Theorem prmnn 12110

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 12109	. 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 4004   2oc2o 6411   ~~ cen 6738   NNcn 8919   || cdvds 11794   Primecprime 12107

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 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005  df-prm 12108

This theorem is referenced by:  prmz  12111  prmssnn  12112  nprmdvds1  12140  isprm5lem  12141  isprm5  12142  coprm  12144  euclemma  12146  prmdvdsexpr  12150  cncongrprm  12157  phiprmpw  12222  fermltl  12234  prmdiv  12235  prmdiveq  12236  prmdivdiv  12237  m1dvdsndvds  12248  vfermltl  12251  powm2modprm  12252  reumodprminv  12253  modprm0  12254  nnnn0modprm0  12255  modprmn0modprm0  12256  oddprm  12259  nnoddn2prm  12260  prm23lt5  12263  pcpremul  12293  pcdvdsb  12319  pcelnn  12320  pcidlem  12322  pcid  12323  pcdvdstr  12326  pcgcd1  12327  pcprmpw2  12332  dvdsprmpweqnn  12335  dvdsprmpweqle  12336  pcaddlem  12338  pcadd  12339  pcmptcl  12340  pcmpt  12341  pcmpt2  12342  pcfaclem  12347  pcfac  12348  pcbc  12349  expnprm  12351  oddprmdvds  12352  prmpwdvds  12353  pockthlem  12354  pockthg  12355  pockthi  12356  1arith  12365  lgslem1  14404  lgslem4  14407  lgsval  14408  lgsval2lem  14414  lgsvalmod  14423  lgsmod  14430  lgsdirprm  14438  lgsne0  14442  lgsprme0  14446  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2sqlem3  14467  2sqlem8  14473