Theorem prmnn 12100

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 12099	. 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 2148   {crab 2459   class class class wbr 4001   2oc2o 6406   ~~ cen 6733   NNcn 8913   || cdvds 11785   Primecprime 12097

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rab 2464  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4002  df-prm 12098

This theorem is referenced by:  prmz  12101  prmssnn  12102  nprmdvds1  12130  isprm5lem  12131  isprm5  12132  coprm  12134  euclemma  12136  prmdvdsexpr  12140  cncongrprm  12147  phiprmpw  12212  fermltl  12224  prmdiv  12225  prmdiveq  12226  prmdivdiv  12227  m1dvdsndvds  12238  vfermltl  12241  powm2modprm  12242  reumodprminv  12243  modprm0  12244  nnnn0modprm0  12245  modprmn0modprm0  12246  oddprm  12249  nnoddn2prm  12250  prm23lt5  12253  pcpremul  12283  pcdvdsb  12309  pcelnn  12310  pcidlem  12312  pcid  12313  pcdvdstr  12316  pcgcd1  12317  pcprmpw2  12322  dvdsprmpweqnn  12325  dvdsprmpweqle  12326  pcaddlem  12328  pcadd  12329  pcmptcl  12330  pcmpt  12331  pcmpt2  12332  pcfaclem  12337  pcfac  12338  pcbc  12339  expnprm  12341  oddprmdvds  12342  prmpwdvds  12343  pockthlem  12344  pockthg  12345  pockthi  12346  1arith  12355  lgslem1  14183  lgslem4  14186  lgsval  14187  lgsval2lem  14193  lgsvalmod  14202  lgsmod  14209  lgsdirprm  14217  lgsne0  14221  lgsprme0  14225  2sqlem3  14235  2sqlem8  14241