ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  prmnn Unicode version

Theorem prmnn 12251
Description: A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.)
Assertion
Ref Expression
prmnn  |-  ( P  e.  Prime  ->  P  e.  NN )

Proof of Theorem prmnn
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 isprm 12250 . 2  |-  ( P  e.  Prime  <->  ( P  e.  NN  /\  { z  e.  NN  |  z 
||  P }  ~~  2o ) )
21simplbi 274 1  |-  ( P  e.  Prime  ->  P  e.  NN )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2164   {crab 2476   class class class wbr 4030   2oc2o 6465    ~~ cen 6794   NNcn 8984    || cdvds 11933   Primecprime 12248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rab 2481  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-br 4031  df-prm 12249
This theorem is referenced by:  prmz  12252  prmssnn  12253  nprmdvds1  12281  isprm5lem  12282  isprm5  12283  coprm  12285  euclemma  12287  prmdvdsexpr  12291  cncongrprm  12298  phiprmpw  12363  fermltl  12375  prmdiv  12376  prmdiveq  12377  prmdivdiv  12378  m1dvdsndvds  12389  vfermltl  12392  powm2modprm  12393  reumodprminv  12394  modprm0  12395  nnnn0modprm0  12396  modprmn0modprm0  12397  oddprm  12400  nnoddn2prm  12401  prm23lt5  12404  pcpremul  12434  pcdvdsb  12461  pcelnn  12462  pcidlem  12464  pcid  12465  pcdvdstr  12468  pcgcd1  12469  pcprmpw2  12474  dvdsprmpweqnn  12477  dvdsprmpweqle  12478  pcaddlem  12480  pcadd  12481  pcmptcl  12483  pcmpt  12484  pcmpt2  12485  pcfaclem  12490  pcfac  12491  pcbc  12492  expnprm  12494  oddprmdvds  12495  prmpwdvds  12496  pockthlem  12497  pockthg  12498  pockthi  12499  1arith  12508  4sqlem11  12542  4sqlem12  12543  4sqlem13m  12544  4sqlem14  12545  4sqlem17  12548  4sqlem18  12549  4sqlem19  12550  znidom  14156  wilthlem1  15153  lgslem1  15157  lgslem4  15160  lgsval  15161  lgsval2lem  15167  lgsvalmod  15176  lgsmod  15183  lgsdirprm  15191  lgsne0  15195  lgsprme0  15199  gausslemma2dlem0c  15208  gausslemma2dlem1a  15215  gausslemma2dlem5a  15222  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgsquadlem1  15234  lgsquadlem3  15236  lgsquad2lem2  15239  lgsquad2  15240  m1lgs  15242  2lgslem1a  15245  2lgslem1c  15247  2lgs  15261  2sqlem3  15274  2sqlem8  15280
  Copyright terms: Public domain W3C validator