Theorem prmnn 12832

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 12831	. 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 4114   2oc2o 6654   ~~ cen 6986   NNcn 9254   || cdvds 12498   Primecprime 12829

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 3700  df-pr 3701  df-op 3703  df-br 4115  df-prm 12830

This theorem is referenced by:  prmz  12833  prmssnn  12834  nprmdvds1  12862  isprm5lem  12863  isprm5  12864  coprm  12866  euclemma  12868  prmdvdsexpr  12872  cncongrprm  12879  phiprmpw  12944  fermltl  12956  prmdiv  12957  prmdiveq  12958  prmdivdiv  12959  m1dvdsndvds  12971  vfermltl  12974  powm2modprm  12975  reumodprminv  12976  modprm0  12977  nnnn0modprm0  12978  modprmn0modprm0  12979  oddprm  12982  nnoddn2prm  12983  prm23lt5  12986  pcpremul  13016  pcdvdsb  13043  pcelnn  13044  pcidlem  13046  pcid  13047  pcdvdstr  13050  pcgcd1  13051  pcprmpw2  13056  dvdsprmpweqnn  13059  dvdsprmpweqle  13060  pcaddlem  13062  pcadd  13063  pcmptcl  13065  pcmpt  13066  pcmpt2  13067  pcfaclem  13072  pcfac  13073  pcbc  13074  expnprm  13076  oddprmdvds  13077  prmpwdvds  13078  pockthlem  13079  pockthg  13080  pockthi  13081  1arith  13090  4sqlem11  13124  4sqlem12  13125  4sqlem13m  13126  4sqlem14  13127  4sqlem17  13130  4sqlem18  13131  4sqlem19  13132  znidom  14931  wilthlem1  15974  dvdsppwf1o  15983  sgmppw  15986  0sgmppw  15987  1sgmprm  15988  mersenne  15991  perfect1  15992  perfect  15995  lgslem1  15999  lgslem4  16002  lgsval  16003  lgsval2lem  16009  lgsvalmod  16018  lgsmod  16025  lgsdirprm  16033  lgsne0  16037  lgsprme0  16041  gausslemma2dlem0c  16050  gausslemma2dlem1a  16057  gausslemma2dlem5a  16064  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgsquadlem1  16076  lgsquadlem3  16078  lgsquad2lem2  16081  lgsquad2  16082  m1lgs  16084  2lgslem1a  16087  2lgslem1c  16089  2lgs  16103  2sqlem3  16116  2sqlem8  16122