Theorem prmnn 12057

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

Syntax hints:   -> wi 4   e. wcel 2141   {crab 2452   class class class wbr 3987   2oc2o 6387   ~~ cen 6714   NNcn 8871   || cdvds 11742   Primecprime 12054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rab 2457  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-br 3988  df-prm 12055

This theorem is referenced by:  prmz  12058  prmssnn  12059  nprmdvds1  12087  isprm5lem  12088  isprm5  12089  coprm  12091  euclemma  12093  prmdvdsexpr  12097  cncongrprm  12104  phiprmpw  12169  fermltl  12181  prmdiv  12182  prmdiveq  12183  prmdivdiv  12184  m1dvdsndvds  12195  vfermltl  12198  powm2modprm  12199  reumodprminv  12200  modprm0  12201  nnnn0modprm0  12202  modprmn0modprm0  12203  oddprm  12206  nnoddn2prm  12207  prm23lt5  12210  pcpremul  12240  pcdvdsb  12266  pcelnn  12267  pcidlem  12269  pcid  12270  pcdvdstr  12273  pcgcd1  12274  pcprmpw2  12279  dvdsprmpweqnn  12282  dvdsprmpweqle  12283  pcaddlem  12285  pcadd  12286  pcmptcl  12287  pcmpt  12288  pcmpt2  12289  pcfaclem  12294  pcfac  12295  pcbc  12296  expnprm  12298  oddprmdvds  12299  prmpwdvds  12300  pockthlem  12301  pockthg  12302  pockthi  12303  1arith  12312  lgslem1  13660  lgslem4  13663  lgsval  13664  lgsval2lem  13670  lgsvalmod  13679  lgsmod  13686  lgsdirprm  13694  lgsne0  13698  lgsprme0  13702  2sqlem3  13712  2sqlem8  13718