Theorem prmnn 12648

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 12647	. 2 |- ( P e. Prime <-> ( P e. NN /\ { z e. NN | z || P } ~~ 2o ) )
2	1	simplbi 274	1 |- ( P e. Prime -> P e. NN )

Syntax hints:   -> wi 4   e. wcel 2200   {crab 2512   class class class wbr 4083   2oc2o 6562   ~~ cen 6893   NNcn 9121   || cdvds 12314   Primecprime 12645

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rab 2517  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084  df-prm 12646

This theorem is referenced by:  prmz  12649  prmssnn  12650  nprmdvds1  12678  isprm5lem  12679  isprm5  12680  coprm  12682  euclemma  12684  prmdvdsexpr  12688  cncongrprm  12695  phiprmpw  12760  fermltl  12772  prmdiv  12773  prmdiveq  12774  prmdivdiv  12775  m1dvdsndvds  12787  vfermltl  12790  powm2modprm  12791  reumodprminv  12792  modprm0  12793  nnnn0modprm0  12794  modprmn0modprm0  12795  oddprm  12798  nnoddn2prm  12799  prm23lt5  12802  pcpremul  12832  pcdvdsb  12859  pcelnn  12860  pcidlem  12862  pcid  12863  pcdvdstr  12866  pcgcd1  12867  pcprmpw2  12872  dvdsprmpweqnn  12875  dvdsprmpweqle  12876  pcaddlem  12878  pcadd  12879  pcmptcl  12881  pcmpt  12882  pcmpt2  12883  pcfaclem  12888  pcfac  12889  pcbc  12890  expnprm  12892  oddprmdvds  12893  prmpwdvds  12894  pockthlem  12895  pockthg  12896  pockthi  12897  1arith  12906  4sqlem11  12940  4sqlem12  12941  4sqlem13m  12942  4sqlem14  12943  4sqlem17  12946  4sqlem18  12947  4sqlem19  12948  znidom  14637  wilthlem1  15670  dvdsppwf1o  15679  sgmppw  15682  0sgmppw  15683  1sgmprm  15684  mersenne  15687  perfect1  15688  perfect  15691  lgslem1  15695  lgslem4  15698  lgsval  15699  lgsval2lem  15705  lgsvalmod  15714  lgsmod  15721  lgsdirprm  15729  lgsne0  15733  lgsprme0  15737  gausslemma2dlem0c  15746  gausslemma2dlem1a  15753  gausslemma2dlem5a  15760  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  lgsquadlem1  15772  lgsquadlem3  15774  lgsquad2lem2  15777  lgsquad2  15778  m1lgs  15780  2lgslem1a  15783  2lgslem1c  15785  2lgs  15799  2sqlem3  15812  2sqlem8  15818