Theorem prmnn 16585

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 16584	. 2 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧 ∥ 𝑃} ≈ 2o))
2	1	simplbi 497	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3394   class class class wbr 5092  2_oc2o 8382   ≈ cen 8869  ℕcn 12128   ∥ cdvds 16163  ℙcprime 16582

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-prm 16583

This theorem is referenced by:  prmz  16586  prmssnn  16587  0nprm  16589  2mulprm  16604  nprmdvds1  16617  isprm5  16618  coprm  16622  prmdvdsexpr  16628  prmndvdsfaclt  16636  prmdvdsbc  16637  prmdvdsncoprmbd  16638  cncongrprm  16640  phiprmpw  16687  fermltl  16695  prmdiv  16696  prmdiveq  16697  prmdivdiv  16698  m1dvdsndvds  16710  vfermltl  16713  vfermltlALT  16714  powm2modprm  16715  reumodprminv  16716  modprm0  16717  nnnn0modprm0  16718  modprmn0modprm0  16719  oddprm  16722  nnoddn2prm  16723  prm23lt5  16726  pcpremul  16755  pcdvdsb  16781  pcelnn  16782  pcidlem  16784  pcid  16785  pcdvdstr  16788  pcgcd1  16789  pcprmpw2  16794  dvdsprmpweqnn  16797  dvdsprmpweqle  16798  pcaddlem  16800  pcadd  16801  pcmptcl  16803  pcmpt  16804  pcmpt2  16805  pcfaclem  16810  pcfac  16811  pcbc  16812  expnprm  16814  oddprmdvds  16815  prmpwdvds  16816  pockthlem  16817  pockthg  16818  pockthi  16819  prmreclem4  16831  prmreclem5  16832  prmreclem6  16833  prmrec  16834  1arith  16839  4sqlem11  16867  4sqlem12  16868  4sqlem13  16869  4sqlem14  16870  4sqlem17  16873  4sqlem18  16874  4sqlem19  16875  prmdvdsprmo  16954  prmgaplem3  16965  prmgaplem4  16966  prmgaplem5  16967  prmgaplem6  16968  prmgaplem8  16970  cshwshashnsame  17015  cshwshash  17016  prmlem1a  17018  pgpfi1  19474  pgp0  19475  sylow1lem1  19477  sylow1lem3  19479  sylow1lem4  19480  sylow1lem5  19481  odcau  19483  pgpfi  19484  fislw  19504  sylow3lem6  19511  gexexlem  19731  prmcyg  19773  ablfac1lem  19949  ablfac1b  19951  ablfac1eu  19954  pgpfac1lem3a  19957  pgpfac1lem3  19958  ablfaclem3  19968  prmgrpsimpgd  19995  prmirredlem  21379  dfprm2  21380  prmirred  21381  fermltlchr  21436  znfld  21467  freshmansdream  21481  frobrhm  21482  ply1fermltlchr  22197  rtprmirr  26668  wilthlem1  26976  wilthlem2  26977  wilthlem3  26978  chtf  27016  efchtcl  27019  isppw2  27023  vmappw  27024  vmaprm  27025  vmacl  27026  efvmacl  27028  muval1  27041  chtprm  27061  chtdif  27066  efchtdvds  27067  dvdsppwf1o  27094  sgmppw  27106  0sgmppw  27107  1sgmprm  27108  vmalelog  27114  chtleppi  27119  chtublem  27120  fsumvma2  27123  vmasum  27125  chpchtsum  27128  chpub  27129  mersenne  27136  perfect1  27137  perfect  27140  pcbcctr  27185  bpos1lem  27191  bposlem1  27193  bposlem2  27194  bposlem6  27198  lgslem1  27206  lgsval2lem  27216  lgsvalmod  27225  lgsmod  27232  lgsdirprm  27240  lgsne0  27244  lgsprme0  27248  lgsqrlem1  27255  lgsqrlem2  27256  lgsqrlem4  27258  lgsqr  27260  lgsqrmod  27261  lgsqrmodndvds  27262  gausslemma2dlem0c  27267  gausslemma2dlem0i  27273  gausslemma2dlem1a  27274  gausslemma2dlem5a  27279  gausslemma2dlem7  27282  gausslemma2d  27283  lgseisenlem1  27284  lgseisenlem2  27285  lgseisenlem3  27286  lgseisenlem4  27287  lgsquadlem1  27289  lgsquadlem3  27291  lgsquad2lem2  27294  lgsquad2  27295  m1lgs  27297  2lgslem1a  27300  2lgslem1c  27302  2lgs  27316  2sqlem3  27329  2sqlem8  27335  2sqlem11  27338  2sqblem  27340  2sqmod  27345  chtppilimlem1  27382  rplogsumlem2  27394  rpvmasumlem  27396  dchrisum0flblem1  27417  dchrisum0flblem2  27418  padicabvf  27540  ostth1  27542  ostth3  27547  hashecclwwlkn1  30021  umgrhashecclwwlk  30022  fusgrhashclwwlkn  30023  clwlksndivn  30030  numclwwlk5  30332  numclwwlk6  30334  numclwwlk7  30335  numclwwlk8  30336  znfermltl  33303  ply1fermltl  33520  cos9thpiminplylem2  33750  nn0prpwlem  36296  nn0prpw  36297  aks4d1p6  42054  aks4d1p8d1  42057  aks4d1p8d2  42058  aks4d1p8d3  42059  aks4d1p8  42060  aks6d1c1p2  42082  aks6d1c1p3  42083  aks6d1c1  42089  aks6d1c2p1  42091  aks6d1c2p2  42092  aks6d1c3  42096  aks6d1c4  42097  aks6d1c2lem4  42100  aks6d1c5lem1  42109  aks6d1c6lem3  42145  aks6d1c6lem4  42146  aks6d1c7lem1  42153  aks6d1c7  42157  aks5lem1  42159  aks5lem2  42160  aks5lem3a  42162  aks5lem8  42174  aks5  42177  nzprmdif  44292  etransclem41  46256  etransclem44  46259  etransclem47  46262  etransclem48  46263  odz2prm2pw  47547  fmtnoprmfac1lem  47548  fmtnoprmfac1  47549  fmtnoprmfac2  47551  prmdvdsfmtnof1lem2  47569  2pwp1prm  47573  sfprmdvdsmersenne  47587  lighneallem2  47590  lighneallem3  47591  lighneallem4  47594  lighneal  47595  perfectALTV  47707  gbepos  47742  gbowpos  47743  sbgoldbaltlem1  47763  ztprmneprm  48331