Theorem prmnn 12762

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 12761	. 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 2202   {crab 2515   class class class wbr 4093   2oc2o 6619   ~~ cen 6950   NNcn 9202   || cdvds 12428   Primecprime 12759

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rab 2520  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094  df-prm 12760

This theorem is referenced by:  prmz  12763  prmssnn  12764  nprmdvds1  12792  isprm5lem  12793  isprm5  12794  coprm  12796  euclemma  12798  prmdvdsexpr  12802  cncongrprm  12809  phiprmpw  12874  fermltl  12886  prmdiv  12887  prmdiveq  12888  prmdivdiv  12889  m1dvdsndvds  12901  vfermltl  12904  powm2modprm  12905  reumodprminv  12906  modprm0  12907  nnnn0modprm0  12908  modprmn0modprm0  12909  oddprm  12912  nnoddn2prm  12913  prm23lt5  12916  pcpremul  12946  pcdvdsb  12973  pcelnn  12974  pcidlem  12976  pcid  12977  pcdvdstr  12980  pcgcd1  12981  pcprmpw2  12986  dvdsprmpweqnn  12989  dvdsprmpweqle  12990  pcaddlem  12992  pcadd  12993  pcmptcl  12995  pcmpt  12996  pcmpt2  12997  pcfaclem  13002  pcfac  13003  pcbc  13004  expnprm  13006  oddprmdvds  13007  prmpwdvds  13008  pockthlem  13009  pockthg  13010  pockthi  13011  1arith  13020  4sqlem11  13054  4sqlem12  13055  4sqlem13m  13056  4sqlem14  13057  4sqlem17  13060  4sqlem18  13061  4sqlem19  13062  znidom  14753  wilthlem1  15794  dvdsppwf1o  15803  sgmppw  15806  0sgmppw  15807  1sgmprm  15808  mersenne  15811  perfect1  15812  perfect  15815  lgslem1  15819  lgslem4  15822  lgsval  15823  lgsval2lem  15829  lgsvalmod  15838  lgsmod  15845  lgsdirprm  15853  lgsne0  15857  lgsprme0  15861  gausslemma2dlem0c  15870  gausslemma2dlem1a  15877  gausslemma2dlem5a  15884  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgseisenlem4  15892  lgsquadlem1  15896  lgsquadlem3  15898  lgsquad2lem2  15901  lgsquad2  15902  m1lgs  15904  2lgslem1a  15907  2lgslem1c  15909  2lgs  15923  2sqlem3  15936  2sqlem8  15942