Theorem prmnn 12904

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.

Step	Hyp	Ref	Expression
1		isprm 12903	. 2 |- ( P e. Prime <-> ( P e. NN /\ { z e. NN | z || P } ~~ 2o ) )
2	1	simplbi 274	1 |- ( P e. Prime -> P e. NN )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   {crab 2532   class class class wbr 4130   2oc2o 6681   ~~ cen 7020   NNcn 9306   || cdvds 12570   Primecprime 12901

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rab 2537  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131  df-prm 12902

This theorem is used by:  prmz  12905  prmssnn  12906  prmdcz  12925  nprmdvds1  12935  isprm5lem  12936  isprm5  12937  coprm  12939  euclemma  12941  prmdvdsexpr  12945  cncongrprm  12952  phiprmpw  13020  fermltl  13032  prmdiv  13033  prmdiveq  13034  prmdivdiv  13035  m1dvdsndvds  13047  vfermltl  13050  powm2modprm  13051  reumodprminv  13052  modprm0  13053  nnnn0modprm0  13054  modprmn0modprm0  13055  oddprm  13058  nnoddn2prm  13059  prm23lt5  13062  pcpremul  13092  pcdvdsb  13119  pcelnn  13120  pcidlem  13122  pcid  13123  pcdvdstr  13126  pcgcd1  13127  pcprmpw2  13132  dvdsprmpweqnn  13135  dvdsprmpweqle  13136  pcaddlem  13138  pcadd  13139  pcmptcl  13141  pcmpt  13142  pcmpt2  13143  pcfaclem  13148  pcfac  13149  pcbc  13150  expnprm  13152  oddprmdvds  13153  prmpwdvds  13154  pockthlem  13155  pockthg  13156  pockthi  13157  1arith  13166  4sqlem11  13200  4sqlem12  13201  4sqlem13m  13202  4sqlem14  13203  4sqlem17  13206  4sqlem18  13207  4sqlem19  13208  prmlem1a  13241  znidom  15041  zprmlogbaplem1  16134  zprmlogbaplem2  16135  zprmlogbaplem3  16136  wilthlem1  16151  dvdsppwf1o  16184  sgmppw  16187  0sgmppw  16188  1sgmprm  16189  mersenne  16195  perfect1  16196  perfect  16199  pcbcctr  16201  prmefexple  16206  bpos1lem  16207  bposlem1  16209  bposlem2  16210  lgslem1  16217  lgslem4  16220  lgsval  16221  lgsval2lem  16227  lgsvalmod  16236  lgsmod  16243  lgsdirprm  16251  lgsne0  16255  lgsprme0  16259  gausslemma2dlem0c  16268  gausslemma2dlem1a  16275  gausslemma2dlem5a  16282  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgsquadlem1  16294  lgsquadlem3  16296  lgsquad2lem2  16299  lgsquad2  16300  m1lgs  16302  2lgslem1a  16305  2lgslem1c  16307  2lgs  16321  2sqlem3  16334  2sqlem8  16340