Theorem prmnn 12837

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 12836	. 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 2205   {crab 2526   class class class wbr 4115   2oc2o 6655   ~~ cen 6987   NNcn 9258   || cdvds 12503   Primecprime 12834

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rab 2531  df-v 2817  df-un 3218  df-sn 3701  df-pr 3702  df-op 3704  df-br 4116  df-prm 12835

This theorem is referenced by:  prmz  12838  prmssnn  12839  nprmdvds1  12867  isprm5lem  12868  isprm5  12869  coprm  12871  euclemma  12873  prmdvdsexpr  12877  cncongrprm  12884  phiprmpw  12949  fermltl  12961  prmdiv  12962  prmdiveq  12963  prmdivdiv  12964  m1dvdsndvds  12976  vfermltl  12979  powm2modprm  12980  reumodprminv  12981  modprm0  12982  nnnn0modprm0  12983  modprmn0modprm0  12984  oddprm  12987  nnoddn2prm  12988  prm23lt5  12991  pcpremul  13021  pcdvdsb  13048  pcelnn  13049  pcidlem  13051  pcid  13052  pcdvdstr  13055  pcgcd1  13056  pcprmpw2  13061  dvdsprmpweqnn  13064  dvdsprmpweqle  13065  pcaddlem  13067  pcadd  13068  pcmptcl  13070  pcmpt  13071  pcmpt2  13072  pcfaclem  13077  pcfac  13078  pcbc  13079  expnprm  13081  oddprmdvds  13082  prmpwdvds  13083  pockthlem  13084  pockthg  13085  pockthi  13086  1arith  13095  4sqlem11  13129  4sqlem12  13130  4sqlem13m  13131  4sqlem14  13132  4sqlem17  13135  4sqlem18  13136  4sqlem19  13137  znidom  14936  wilthlem1  15979  dvdsppwf1o  15988  sgmppw  15991  0sgmppw  15992  1sgmprm  15993  mersenne  15996  perfect1  15997  perfect  16000  lgslem1  16004  lgslem4  16007  lgsval  16008  lgsval2lem  16014  lgsvalmod  16023  lgsmod  16030  lgsdirprm  16038  lgsne0  16042  lgsprme0  16046  gausslemma2dlem0c  16055  gausslemma2dlem1a  16062  gausslemma2dlem5a  16069  lgseisenlem1  16074  lgseisenlem2  16075  lgseisenlem3  16076  lgseisenlem4  16077  lgsquadlem1  16081  lgsquadlem3  16083  lgsquad2lem2  16086  lgsquad2  16087  m1lgs  16089  2lgslem1a  16092  2lgslem1c  16094  2lgs  16108  2sqlem3  16121  2sqlem8  16127