Theorem prmnn 16613

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

Syntax hints:   → wi 4   ∈ wcel 2114  {crab 3401   class class class wbr 5100  2_oc2o 8401   ≈ cen 8892  ℕcn 12157   ∥ cdvds 16191  ℙcprime 16610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-prm 16611

This theorem is referenced by:  prmz  16614  prmssnn  16615  0nprm  16617  2mulprm  16632  nprmdvds1  16645  isprm5  16646  coprm  16650  prmdvdsexpr  16656  prmndvdsfaclt  16664  prmdvdsbc  16665  prmdvdsncoprmbd  16666  cncongrprm  16668  phiprmpw  16715  fermltl  16723  prmdiv  16724  prmdiveq  16725  prmdivdiv  16726  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  17043  cshwshash  17044  prmlem1a  17046  pgpfi1  19536  pgp0  19537  sylow1lem1  19539  sylow1lem3  19541  sylow1lem4  19542  sylow1lem5  19543  odcau  19545  pgpfi  19546  fislw  19566  sylow3lem6  19573  gexexlem  19793  prmcyg  19835  ablfac1lem  20011  ablfac1b  20013  ablfac1eu  20016  pgpfac1lem3a  20019  pgpfac1lem3  20020  ablfaclem3  20030  prmgrpsimpgd  20057  prmirredlem  21439  dfprm2  21440  prmirred  21441  fermltlchr  21496  znfld  21527  freshmansdream  21541  frobrhm  21542  ply1fermltlchr  22268  rtprmirr  26738  wilthlem1  27046  wilthlem2  27047  wilthlem3  27048  chtf  27086  efchtcl  27089  isppw2  27093  vmappw  27094  vmaprm  27095  vmacl  27096  efvmacl  27098  muval1  27111  chtprm  27131  chtdif  27136  efchtdvds  27137  dvdsppwf1o  27164  sgmppw  27176  0sgmppw  27177  1sgmprm  27178  vmalelog  27184  chtleppi  27189  chtublem  27190  fsumvma2  27193  vmasum  27195  chpchtsum  27198  chpub  27199  mersenne  27206  perfect1  27207  perfect  27210  pcbcctr  27255  bpos1lem  27261  bposlem1  27263  bposlem2  27264  bposlem6  27268  lgslem1  27276  lgsval2lem  27286  lgsvalmod  27295  lgsmod  27302  lgsdirprm  27310  lgsne0  27314  lgsprme0  27318  lgsqrlem1  27325  lgsqrlem2  27326  lgsqrlem4  27328  lgsqr  27330  lgsqrmod  27331  lgsqrmodndvds  27332  gausslemma2dlem0c  27337  gausslemma2dlem0i  27343  gausslemma2dlem1a  27344  gausslemma2dlem5a  27349  gausslemma2dlem7  27352  gausslemma2d  27353  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisenlem4  27357  lgsquadlem1  27359  lgsquadlem3  27361  lgsquad2lem2  27364  lgsquad2  27365  m1lgs  27367  2lgslem1a  27370  2lgslem1c  27372  2lgs  27386  2sqlem3  27399  2sqlem8  27405  2sqlem11  27408  2sqblem  27410  2sqmod  27415  chtppilimlem1  27452  rplogsumlem2  27464  rpvmasumlem  27466  dchrisum0flblem1  27487  dchrisum0flblem2  27488  padicabvf  27610  ostth1  27612  ostth3  27617  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  fusgrhashclwwlkn  30166  clwlksndivn  30173  numclwwlk5  30475  numclwwlk6  30477  numclwwlk7  30478  numclwwlk8  30479  znfermltl  33459  ply1fermltl  33679  cos9thpiminplylem2  33961  nn0prpwlem  36538  nn0prpw  36539  aks4d1p6  42451  aks4d1p8d1  42454  aks4d1p8d2  42455  aks4d1p8d3  42456  aks4d1p8  42457  aks6d1c1p2  42479  aks6d1c1p3  42480  aks6d1c1  42486  aks6d1c2p1  42488  aks6d1c2p2  42489  aks6d1c3  42493  aks6d1c4  42494  aks6d1c2lem4  42497  aks6d1c5lem1  42506  aks6d1c6lem3  42542  aks6d1c6lem4  42543  aks6d1c7lem1  42550  aks6d1c7  42554  aks5lem1  42556  aks5lem2  42557  aks5lem3a  42559  aks5lem8  42571  aks5  42574  nzprmdif  44675  etransclem41  46633  etransclem44  46636  etransclem47  46639  etransclem48  46640  odz2prm2pw  47923  fmtnoprmfac1lem  47924  fmtnoprmfac1  47925  fmtnoprmfac2  47927  prmdvdsfmtnof1lem2  47945  2pwp1prm  47949  sfprmdvdsmersenne  47963  lighneallem2  47966  lighneallem3  47967  lighneallem4  47970  lighneal  47971  perfectALTV  48083  gbepos  48118  gbowpos  48119  sbgoldbaltlem1  48139  ztprmneprm  48707