Theorem prmnn 16650

Description: A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.)

Assertion

Ref	Expression
prmnn	⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)

Proof of Theorem prmnn

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isprm 16649	. 2 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧 ∥ 𝑃} ≈ 2o))
2	1	simplbi 497	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3408   class class class wbr 5109  2_oc2o 8430   ≈ cen 8917  ℕcn 12187   ∥ cdvds 16228  ℙcprime 16647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-br 5110  df-prm 16648

This theorem is referenced by:  prmz  16651  prmssnn  16652  0nprm  16654  2mulprm  16669  nprmdvds1  16682  isprm5  16683  coprm  16687  prmdvdsexpr  16693  prmndvdsfaclt  16701  prmdvdsbc  16702  prmdvdsncoprmbd  16703  cncongrprm  16705  phiprmpw  16752  fermltl  16760  prmdiv  16761  prmdiveq  16762  prmdivdiv  16763  m1dvdsndvds  16775  vfermltl  16778  vfermltlALT  16779  powm2modprm  16780  reumodprminv  16781  modprm0  16782  nnnn0modprm0  16783  modprmn0modprm0  16784  oddprm  16787  nnoddn2prm  16788  prm23lt5  16791  pcpremul  16820  pcdvdsb  16846  pcelnn  16847  pcidlem  16849  pcid  16850  pcdvdstr  16853  pcgcd1  16854  pcprmpw2  16859  dvdsprmpweqnn  16862  dvdsprmpweqle  16863  pcaddlem  16865  pcadd  16866  pcmptcl  16868  pcmpt  16869  pcmpt2  16870  pcfaclem  16875  pcfac  16876  pcbc  16877  expnprm  16879  oddprmdvds  16880  prmpwdvds  16881  pockthlem  16882  pockthg  16883  pockthi  16884  prmreclem4  16896  prmreclem5  16897  prmreclem6  16898  prmrec  16899  1arith  16904  4sqlem11  16932  4sqlem12  16933  4sqlem13  16934  4sqlem14  16935  4sqlem17  16938  4sqlem18  16939  4sqlem19  16940  prmdvdsprmo  17019  prmgaplem3  17030  prmgaplem4  17031  prmgaplem5  17032  prmgaplem6  17033  prmgaplem8  17035  cshwshashnsame  17080  cshwshash  17081  prmlem1a  17083  pgpfi1  19531  pgp0  19532  sylow1lem1  19534  sylow1lem3  19536  sylow1lem4  19537  sylow1lem5  19538  odcau  19540  pgpfi  19541  fislw  19561  sylow3lem6  19568  gexexlem  19788  prmcyg  19830  ablfac1lem  20006  ablfac1b  20008  ablfac1eu  20011  pgpfac1lem3a  20014  pgpfac1lem3  20015  ablfaclem3  20025  prmgrpsimpgd  20052  prmirredlem  21388  dfprm2  21389  prmirred  21390  fermltlchr  21445  znfld  21476  freshmansdream  21490  frobrhm  21491  ply1fermltlchr  22205  rtprmirr  26676  wilthlem1  26984  wilthlem2  26985  wilthlem3  26986  chtf  27024  efchtcl  27027  isppw2  27031  vmappw  27032  vmaprm  27033  vmacl  27034  efvmacl  27036  muval1  27049  chtprm  27069  chtdif  27074  efchtdvds  27075  dvdsppwf1o  27102  sgmppw  27114  0sgmppw  27115  1sgmprm  27116  vmalelog  27122  chtleppi  27127  chtublem  27128  fsumvma2  27131  vmasum  27133  chpchtsum  27136  chpub  27137  mersenne  27144  perfect1  27145  perfect  27148  pcbcctr  27193  bpos1lem  27199  bposlem1  27201  bposlem2  27202  bposlem6  27206  lgslem1  27214  lgsval2lem  27224  lgsvalmod  27233  lgsmod  27240  lgsdirprm  27248  lgsne0  27252  lgsprme0  27256  lgsqrlem1  27263  lgsqrlem2  27264  lgsqrlem4  27266  lgsqr  27268  lgsqrmod  27269  lgsqrmodndvds  27270  gausslemma2dlem0c  27275  gausslemma2dlem0i  27281  gausslemma2dlem1a  27282  gausslemma2dlem5a  27287  gausslemma2dlem7  27290  gausslemma2d  27291  lgseisenlem1  27292  lgseisenlem2  27293  lgseisenlem3  27294  lgseisenlem4  27295  lgsquadlem1  27297  lgsquadlem3  27299  lgsquad2lem2  27302  lgsquad2  27303  m1lgs  27305  2lgslem1a  27308  2lgslem1c  27310  2lgs  27324  2sqlem3  27337  2sqlem8  27343  2sqlem11  27346  2sqblem  27348  2sqmod  27353  chtppilimlem1  27390  rplogsumlem2  27402  rpvmasumlem  27404  dchrisum0flblem1  27425  dchrisum0flblem2  27426  padicabvf  27548  ostth1  27550  ostth3  27555  hashecclwwlkn1  30012  umgrhashecclwwlk  30013  fusgrhashclwwlkn  30014  clwlksndivn  30021  numclwwlk5  30323  numclwwlk6  30325  numclwwlk7  30326  numclwwlk8  30327  znfermltl  33343  ply1fermltl  33559  cos9thpiminplylem2  33779  nn0prpwlem  36305  nn0prpw  36306  aks4d1p6  42064  aks4d1p8d1  42067  aks4d1p8d2  42068  aks4d1p8d3  42069  aks4d1p8  42070  aks6d1c1p2  42092  aks6d1c1p3  42093  aks6d1c1  42099  aks6d1c2p1  42101  aks6d1c2p2  42102  aks6d1c3  42106  aks6d1c4  42107  aks6d1c2lem4  42110  aks6d1c5lem1  42119  aks6d1c6lem3  42155  aks6d1c6lem4  42156  aks6d1c7lem1  42163  aks6d1c7  42167  aks5lem1  42169  aks5lem2  42170  aks5lem3a  42172  aks5lem8  42184  aks5  42187  nzprmdif  44301  etransclem41  46266  etransclem44  46269  etransclem47  46272  etransclem48  46273  odz2prm2pw  47554  fmtnoprmfac1lem  47555  fmtnoprmfac1  47556  fmtnoprmfac2  47558  prmdvdsfmtnof1lem2  47576  2pwp1prm  47580  sfprmdvdsmersenne  47594  lighneallem2  47597  lighneallem3  47598  lighneallem4  47601  lighneal  47602  perfectALTV  47714  gbepos  47749  gbowpos  47750  sbgoldbaltlem1  47770  ztprmneprm  48325