Theorem prmnn 16611

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

Syntax hints:   → wi 4   ∈ wcel 2107  {crab 3433   class class class wbr 5149  2_oc2o 8460   ≈ cen 8936  ℕcn 12212   ∥ cdvds 16197  ℙcprime 16608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-prm 16609

This theorem is referenced by:  prmz  16612  prmssnn  16613  0nprm  16615  2mulprm  16630  nprmdvds1  16643  isprm5  16644  coprm  16648  prmdvdsexpr  16654  prmndvdsfaclt  16662  prmdvdsncoprmbd  16663  cncongrprm  16665  phiprmpw  16709  fermltl  16717  prmdiv  16718  prmdiveq  16719  prmdivdiv  16720  m1dvdsndvds  16731  vfermltl  16734  vfermltlALT  16735  powm2modprm  16736  reumodprminv  16737  modprm0  16738  nnnn0modprm0  16739  modprmn0modprm0  16740  oddprm  16743  nnoddn2prm  16744  prm23lt5  16747  pcpremul  16776  pcdvdsb  16802  pcelnn  16803  pcidlem  16805  pcid  16806  pcdvdstr  16809  pcgcd1  16810  pcprmpw2  16815  dvdsprmpweqnn  16818  dvdsprmpweqle  16819  pcaddlem  16821  pcadd  16822  pcmptcl  16824  pcmpt  16825  pcmpt2  16826  pcfaclem  16831  pcfac  16832  pcbc  16833  expnprm  16835  oddprmdvds  16836  prmpwdvds  16837  pockthlem  16838  pockthg  16839  pockthi  16840  prmreclem4  16852  prmreclem5  16853  prmreclem6  16854  prmrec  16855  1arith  16860  4sqlem11  16888  4sqlem12  16889  4sqlem13  16890  4sqlem14  16891  4sqlem17  16894  4sqlem18  16895  4sqlem19  16896  prmdvdsprmo  16975  prmgaplem3  16986  prmgaplem4  16987  prmgaplem5  16988  prmgaplem6  16989  prmgaplem8  16991  cshwshashnsame  17037  cshwshash  17038  prmlem1a  17040  pgpfi1  19463  pgp0  19464  sylow1lem1  19466  sylow1lem3  19468  sylow1lem4  19469  sylow1lem5  19470  odcau  19472  pgpfi  19473  fislw  19493  sylow3lem6  19500  gexexlem  19720  prmcyg  19762  ablfac1lem  19938  ablfac1b  19940  ablfac1eu  19943  pgpfac1lem3a  19946  pgpfac1lem3  19947  ablfaclem3  19957  prmgrpsimpgd  19984  prmirredlem  21042  dfprm2  21043  prmirred  21044  znfld  21116  wilthlem1  26572  wilthlem2  26573  wilthlem3  26574  chtf  26612  efchtcl  26615  isppw2  26619  vmappw  26620  vmaprm  26621  vmacl  26622  efvmacl  26624  muval1  26637  chtprm  26657  chtdif  26662  efchtdvds  26663  dvdsppwf1o  26690  sgmppw  26700  0sgmppw  26701  1sgmprm  26702  vmalelog  26708  chtleppi  26713  chtublem  26714  fsumvma2  26717  vmasum  26719  chpchtsum  26722  chpub  26723  mersenne  26730  perfect1  26731  perfect  26734  pcbcctr  26779  bpos1lem  26785  bposlem1  26787  bposlem2  26788  bposlem6  26792  lgslem1  26800  lgsval2lem  26810  lgsvalmod  26819  lgsmod  26826  lgsdirprm  26834  lgsne0  26838  lgsprme0  26842  lgsqrlem1  26849  lgsqrlem2  26850  lgsqrlem4  26852  lgsqr  26854  lgsqrmod  26855  lgsqrmodndvds  26856  gausslemma2dlem0c  26861  gausslemma2dlem0i  26867  gausslemma2dlem1a  26868  gausslemma2dlem5a  26873  gausslemma2dlem7  26876  gausslemma2d  26877  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgseisenlem4  26881  lgsquadlem1  26883  lgsquadlem3  26885  lgsquad2lem2  26888  lgsquad2  26889  m1lgs  26891  2lgslem1a  26894  2lgslem1c  26896  2lgs  26910  2sqlem3  26923  2sqlem8  26929  2sqlem11  26932  2sqblem  26934  2sqmod  26939  chtppilimlem1  26976  rplogsumlem2  26988  rpvmasumlem  26990  dchrisum0flblem1  27011  dchrisum0flblem2  27012  padicabvf  27134  ostth1  27136  ostth3  27141  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  fusgrhashclwwlkn  29332  clwlksndivn  29339  numclwwlk5  29641  numclwwlk6  29643  numclwwlk7  29644  numclwwlk8  29645  prmdvdsbc  32022  freshmansdream  32381  frobrhm  32382  fermltlchr  32478  znfermltl  32479  ply1fermltlchr  32662  ply1fermltl  32663  nn0prpwlem  35207  nn0prpw  35208  aks4d1p6  40946  aks4d1p8d1  40949  aks4d1p8d2  40950  aks4d1p8d3  40951  aks4d1p8  40952  aks6d1c2p1  40956  aks6d1c2p2  40957  rtprmirr  41237  nzprmdif  43078  etransclem41  44991  etransclem44  44994  etransclem47  44997  etransclem48  44998  odz2prm2pw  46231  fmtnoprmfac1lem  46232  fmtnoprmfac1  46233  fmtnoprmfac2  46235  prmdvdsfmtnof1lem2  46253  2pwp1prm  46257  sfprmdvdsmersenne  46271  lighneallem2  46274  lighneallem3  46275  lighneallem4  46278  lighneal  46279  perfectALTV  46391  gbepos  46426  gbowpos  46427  sbgoldbaltlem1  46447  ztprmneprm  47023