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 2111  {crab 3395   class class class wbr 5089  2_oc2o 8379   ≈ cen 8866  ℕcn 12125   ∥ cdvds 16163  ℙcprime 16582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  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  19507  pgp0  19508  sylow1lem1  19510  sylow1lem3  19512  sylow1lem4  19513  sylow1lem5  19514  odcau  19516  pgpfi  19517  fislw  19537  sylow3lem6  19544  gexexlem  19764  prmcyg  19806  ablfac1lem  19982  ablfac1b  19984  ablfac1eu  19987  pgpfac1lem3a  19990  pgpfac1lem3  19991  ablfaclem3  20001  prmgrpsimpgd  20028  prmirredlem  21409  dfprm2  21410  prmirred  21411  fermltlchr  21466  znfld  21497  freshmansdream  21511  frobrhm  21512  ply1fermltlchr  22227  rtprmirr  26697  wilthlem1  27005  wilthlem2  27006  wilthlem3  27007  chtf  27045  efchtcl  27048  isppw2  27052  vmappw  27053  vmaprm  27054  vmacl  27055  efvmacl  27057  muval1  27070  chtprm  27090  chtdif  27095  efchtdvds  27096  dvdsppwf1o  27123  sgmppw  27135  0sgmppw  27136  1sgmprm  27137  vmalelog  27143  chtleppi  27148  chtublem  27149  fsumvma2  27152  vmasum  27154  chpchtsum  27157  chpub  27158  mersenne  27165  perfect1  27166  perfect  27169  pcbcctr  27214  bpos1lem  27220  bposlem1  27222  bposlem2  27223  bposlem6  27227  lgslem1  27235  lgsval2lem  27245  lgsvalmod  27254  lgsmod  27261  lgsdirprm  27269  lgsne0  27273  lgsprme0  27277  lgsqrlem1  27284  lgsqrlem2  27285  lgsqrlem4  27287  lgsqr  27289  lgsqrmod  27290  lgsqrmodndvds  27291  gausslemma2dlem0c  27296  gausslemma2dlem0i  27302  gausslemma2dlem1a  27303  gausslemma2dlem5a  27308  gausslemma2dlem7  27311  gausslemma2d  27312  lgseisenlem1  27313  lgseisenlem2  27314  lgseisenlem3  27315  lgseisenlem4  27316  lgsquadlem1  27318  lgsquadlem3  27320  lgsquad2lem2  27323  lgsquad2  27324  m1lgs  27326  2lgslem1a  27329  2lgslem1c  27331  2lgs  27345  2sqlem3  27358  2sqlem8  27364  2sqlem11  27367  2sqblem  27369  2sqmod  27374  chtppilimlem1  27411  rplogsumlem2  27423  rpvmasumlem  27425  dchrisum0flblem1  27446  dchrisum0flblem2  27447  padicabvf  27569  ostth1  27571  ostth3  27576  hashecclwwlkn1  30057  umgrhashecclwwlk  30058  fusgrhashclwwlkn  30059  clwlksndivn  30066  numclwwlk5  30368  numclwwlk6  30370  numclwwlk7  30371  numclwwlk8  30372  znfermltl  33331  ply1fermltl  33548  cos9thpiminplylem2  33796  nn0prpwlem  36364  nn0prpw  36365  aks4d1p6  42122  aks4d1p8d1  42125  aks4d1p8d2  42126  aks4d1p8d3  42127  aks4d1p8  42128  aks6d1c1p2  42150  aks6d1c1p3  42151  aks6d1c1  42157  aks6d1c2p1  42159  aks6d1c2p2  42160  aks6d1c3  42164  aks6d1c4  42165  aks6d1c2lem4  42168  aks6d1c5lem1  42177  aks6d1c6lem3  42213  aks6d1c6lem4  42214  aks6d1c7lem1  42221  aks6d1c7  42225  aks5lem1  42227  aks5lem2  42228  aks5lem3a  42230  aks5lem8  42242  aks5  42245  nzprmdif  44360  etransclem41  46321  etransclem44  46324  etransclem47  46327  etransclem48  46328  odz2prm2pw  47602  fmtnoprmfac1lem  47603  fmtnoprmfac1  47604  fmtnoprmfac2  47606  prmdvdsfmtnof1lem2  47624  2pwp1prm  47628  sfprmdvdsmersenne  47642  lighneallem2  47645  lighneallem3  47646  lighneallem4  47649  lighneal  47650  perfectALTV  47762  gbepos  47797  gbowpos  47798  sbgoldbaltlem1  47818  ztprmneprm  48386