Theorem prmnn 16618

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

Syntax hints:   → wi 4   ∈ wcel 2105  {crab 3431   class class class wbr 5148  2_oc2o 8466   ≈ cen 8942  ℕcn 12219   ∥ cdvds 16204  ℙcprime 16615

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-prm 16616

This theorem is referenced by:  prmz  16619  prmssnn  16620  0nprm  16622  2mulprm  16637  nprmdvds1  16650  isprm5  16651  coprm  16655  prmdvdsexpr  16661  prmndvdsfaclt  16669  prmdvdsncoprmbd  16670  cncongrprm  16672  phiprmpw  16716  fermltl  16724  prmdiv  16725  prmdiveq  16726  prmdivdiv  16727  m1dvdsndvds  16738  vfermltl  16741  vfermltlALT  16742  powm2modprm  16743  reumodprminv  16744  modprm0  16745  nnnn0modprm0  16746  modprmn0modprm0  16747  oddprm  16750  nnoddn2prm  16751  prm23lt5  16754  pcpremul  16783  pcdvdsb  16809  pcelnn  16810  pcidlem  16812  pcid  16813  pcdvdstr  16816  pcgcd1  16817  pcprmpw2  16822  dvdsprmpweqnn  16825  dvdsprmpweqle  16826  pcaddlem  16828  pcadd  16829  pcmptcl  16831  pcmpt  16832  pcmpt2  16833  pcfaclem  16838  pcfac  16839  pcbc  16840  expnprm  16842  oddprmdvds  16843  prmpwdvds  16844  pockthlem  16845  pockthg  16846  pockthi  16847  prmreclem4  16859  prmreclem5  16860  prmreclem6  16861  prmrec  16862  1arith  16867  4sqlem11  16895  4sqlem12  16896  4sqlem13  16897  4sqlem14  16898  4sqlem17  16901  4sqlem18  16902  4sqlem19  16903  prmdvdsprmo  16982  prmgaplem3  16993  prmgaplem4  16994  prmgaplem5  16995  prmgaplem6  16996  prmgaplem8  16998  cshwshashnsame  17044  cshwshash  17045  prmlem1a  17047  pgpfi1  19511  pgp0  19512  sylow1lem1  19514  sylow1lem3  19516  sylow1lem4  19517  sylow1lem5  19518  odcau  19520  pgpfi  19521  fislw  19541  sylow3lem6  19548  gexexlem  19768  prmcyg  19810  ablfac1lem  19986  ablfac1b  19988  ablfac1eu  19991  pgpfac1lem3a  19994  pgpfac1lem3  19995  ablfaclem3  20005  prmgrpsimpgd  20032  prmirredlem  21331  dfprm2  21332  prmirred  21333  znfld  21425  wilthlem1  26912  wilthlem2  26913  wilthlem3  26914  chtf  26952  efchtcl  26955  isppw2  26959  vmappw  26960  vmaprm  26961  vmacl  26962  efvmacl  26964  muval1  26977  chtprm  26997  chtdif  27002  efchtdvds  27003  dvdsppwf1o  27030  sgmppw  27042  0sgmppw  27043  1sgmprm  27044  vmalelog  27050  chtleppi  27055  chtublem  27056  fsumvma2  27059  vmasum  27061  chpchtsum  27064  chpub  27065  mersenne  27072  perfect1  27073  perfect  27076  pcbcctr  27121  bpos1lem  27127  bposlem1  27129  bposlem2  27130  bposlem6  27134  lgslem1  27142  lgsval2lem  27152  lgsvalmod  27161  lgsmod  27168  lgsdirprm  27176  lgsne0  27180  lgsprme0  27184  lgsqrlem1  27191  lgsqrlem2  27192  lgsqrlem4  27194  lgsqr  27196  lgsqrmod  27197  lgsqrmodndvds  27198  gausslemma2dlem0c  27203  gausslemma2dlem0i  27209  gausslemma2dlem1a  27210  gausslemma2dlem5a  27215  gausslemma2dlem7  27218  gausslemma2d  27219  lgseisenlem1  27220  lgseisenlem2  27221  lgseisenlem3  27222  lgseisenlem4  27223  lgsquadlem1  27225  lgsquadlem3  27227  lgsquad2lem2  27230  lgsquad2  27231  m1lgs  27233  2lgslem1a  27236  2lgslem1c  27238  2lgs  27252  2sqlem3  27265  2sqlem8  27271  2sqlem11  27274  2sqblem  27276  2sqmod  27281  chtppilimlem1  27318  rplogsumlem2  27330  rpvmasumlem  27332  dchrisum0flblem1  27353  dchrisum0flblem2  27354  padicabvf  27476  ostth1  27478  ostth3  27483  hashecclwwlkn1  29762  umgrhashecclwwlk  29763  fusgrhashclwwlkn  29764  clwlksndivn  29771  numclwwlk5  30073  numclwwlk6  30075  numclwwlk7  30076  numclwwlk8  30077  prmdvdsbc  32454  freshmansdream  32816  frobrhm  32817  fermltlchr  32917  znfermltl  32918  ply1fermltlchr  33101  ply1fermltl  33102  nn0prpwlem  35670  nn0prpw  35671  aks4d1p6  41412  aks4d1p8d1  41415  aks4d1p8d2  41416  aks4d1p8d3  41417  aks4d1p8  41418  aks6d1c2p1  41422  aks6d1c2p2  41423  rtprmirr  41699  nzprmdif  43540  etransclem41  45449  etransclem44  45452  etransclem47  45455  etransclem48  45456  odz2prm2pw  46689  fmtnoprmfac1lem  46690  fmtnoprmfac1  46691  fmtnoprmfac2  46693  prmdvdsfmtnof1lem2  46711  2pwp1prm  46715  sfprmdvdsmersenne  46729  lighneallem2  46732  lighneallem3  46733  lighneallem4  46736  lighneal  46737  perfectALTV  46849  gbepos  46884  gbowpos  46885  sbgoldbaltlem1  46905  ztprmneprm  47185