Theorem prmnn 12064

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 12063	. 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 3989   2oc2o 6389   ~~ cen 6716   NNcn 8878   || cdvds 11749   Primecprime 12061

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 3589  df-pr 3590  df-op 3592  df-br 3990  df-prm 12062

This theorem is referenced by:  prmz  12065  prmssnn  12066  nprmdvds1  12094  isprm5lem  12095  isprm5  12096  coprm  12098  euclemma  12100  prmdvdsexpr  12104  cncongrprm  12111  phiprmpw  12176  fermltl  12188  prmdiv  12189  prmdiveq  12190  prmdivdiv  12191  m1dvdsndvds  12202  vfermltl  12205  powm2modprm  12206  reumodprminv  12207  modprm0  12208  nnnn0modprm0  12209  modprmn0modprm0  12210  oddprm  12213  nnoddn2prm  12214  prm23lt5  12217  pcpremul  12247  pcdvdsb  12273  pcelnn  12274  pcidlem  12276  pcid  12277  pcdvdstr  12280  pcgcd1  12281  pcprmpw2  12286  dvdsprmpweqnn  12289  dvdsprmpweqle  12290  pcaddlem  12292  pcadd  12293  pcmptcl  12294  pcmpt  12295  pcmpt2  12296  pcfaclem  12301  pcfac  12302  pcbc  12303  expnprm  12305  oddprmdvds  12306  prmpwdvds  12307  pockthlem  12308  pockthg  12309  pockthi  12310  1arith  12319  lgslem1  13695  lgslem4  13698  lgsval  13699  lgsval2lem  13705  lgsvalmod  13714  lgsmod  13721  lgsdirprm  13729  lgsne0  13733  lgsprme0  13737  2sqlem3  13747  2sqlem8  13753