From 915195971f5c176d4510a2037c4041e48a9f3993 Mon Sep 17 00:00:00 2001
From: Jim Kingdon <kingdon@panix.com>
Date: Mon, 30 Sep 2024 18:01:47 -0700
Subject: [PATCH] Add prmdc to iset.mm

Primality is decidable.  This follows fairly easily from decidability of
divisibility, isprm3 , and other theorems we have.
---
 iset.mm | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/iset.mm b/iset.mm
index 24759ec9d7..7f78963b6e 100644
--- a/iset.mm
+++ b/iset.mm
@@ -133435,6 +133435,22 @@ According to Wikipedia ("Least common multiple", 27-Aug-2020,
   4nprm $p |- -. 4 e. Prime $=
     ( c2 c4 2nn 1lt2 2t2e4 nprmi ) AABCCDDEF $.
 
+  ${
+    $d N x $.
+    $( Primality is decidable.  (Contributed by Jim Kingdon, 30-Sep-2024.) $)
+    prmdc $p |- ( N e. NN -> DECID N e. Prime ) $=
+      ( vx cn wcel c2 cuz wbr wn c1 co wral wa wdc wo cz a1i syl adantl syl2anc
+      cle cfv cv cdvds cmin cfz cprime wceq 1nuz2 mtbiri orim1i orcomd elnn1uz2
+      eleq1 df-dc 3imtr4i cfn 2z nnz peano2zm fzfigd elfzelz 1red 2re zred 1le2
+      cr elfzle1 letrd elnnz1 sylanbrc adantr dvdsdc ralrimiva dcfi dcan isprm3
+      dcn sylc dcbii sylibr ) ACDZAEFUAZDZBUBZAUCGZHZBEAIUDJZUEJZKZLZMZAUFDZMWA
+      WCMZWIMZWKAIUGZWCNZWCWCHZNWAWMWPWQWCWOWQWCWOWCIWBDUHAIWBUMUIUJUKAULWCUNUO
+      WAWHUPDWFMZBWHKWNWAEWGEODWAUQPWAAODZWGODAURZAUSQUTWAWRBWHWAWDWHDZLZWEMZWR
+      XBWDCDZWSXCXBWDODZIWDTGXDXAXEWAWDEWGVARZXBIEWDXBVBEVFDXBVCPXBWDXFVDIETGXB
+      VEPXAEWDTGWAWDEWGVGRVHWDVIVJWAWSXAWTVKWDAVLSWEVQQVMWFBWHVNSWCWIVOVRWLWJBA
+      VPVSVT $.
+  $}
+
   ${
     $d P x $.
     $( A prime number is an integer greater than or equal to 2.  (Contributed