Add prmdc to iset.mm

Primality is decidable.  This follows fairly easily from decidability of
divisibility, isprm3 , and other theorems we have.

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