Theorem prmnn 16842

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {crab 3413   class class class wbr 5103  2_oc2o 8463   ≈ cen 8963  ℕcn 12328   ∥ cdvds 16415  ℙcprime 16839

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-prm 16840

This theorem is used by:  prmz  16843  prmssnn  16844  0nprm  16846  2mulprm  16861  nprmdvds1  16875  isprm5  16876  coprm  16880  prmdvdsexpr  16886  prmndvdsfaclt  16894  prmdvdsbc  16895  prmdvdsncoprmbd  16896  cncongrprm  16898  phiprmpw  16946  fermltl  16954  prmdiv  16955  prmdiveq  16956  prmdivdiv  16957  m1dvdsndvds  16969  vfermltl  16972  vfermltlALT  16973  powm2modprm  16974  reumodprminv  16975  modprm0  16976  nnnn0modprm0  16977  modprmn0modprm0  16978  oddprm  16981  nnoddn2prm  16982  prm23lt5  16985  pcpremul  17014  pcdvdsb  17040  pcelnn  17041  pcidlem  17043  pcid  17044  pcdvdstr  17047  pcgcd1  17048  pcprmpw2  17053  dvdsprmpweqnn  17056  dvdsprmpweqle  17057  pcaddlem  17059  pcadd  17060  pcmptcl  17062  pcmpt  17063  pcmpt2  17064  pcfaclem  17069  pcfac  17070  pcbc  17071  expnprm  17073  oddprmdvds  17074  prmpwdvds  17075  pockthlem  17076  pockthg  17077  pockthi  17078  prmreclem4  17090  prmreclem5  17091  prmreclem6  17092  prmrec  17093  1arith  17098  4sqlem11  17126  4sqlem12  17127  4sqlem13  17128  4sqlem14  17129  4sqlem17  17132  4sqlem18  17133  4sqlem19  17134  prmdvdsprmo  17213  prmgaplem3  17224  prmgaplem4  17225  prmgaplem5  17226  prmgaplem6  17227  prmgaplem8  17229  cshwshashnsame  17274  cshwshash  17275  prmlem1a  17277  pgpfi1  19802  pgp0  19803  sylow1lem1  19805  sylow1lem3  19807  sylow1lem4  19808  sylow1lem5  19809  odcau  19811  pgpfi  19812  fislw  19832  sylow3lem6  19839  gexexlem  20059  prmcyg  20101  ablfac1lem  20277  ablfac1b  20279  ablfac1eu  20282  pgpfac1lem3a  20285  pgpfac1lem3  20286  ablfaclem3  20296  prmgrpsimpgd  20323  prmirredlem  21771  dfprm2  21772  prmirred  21773  fermltlchr  21828  znfld  21859  freshmansdream  21873  frobrhm  21874  ply1fermltlchr  22623  rtprmirr  27081  wilthlem1  27388  wilthlem2  27389  wilthlem3  27390  chtf  27428  efchtcl  27431  isppw2  27435  vmappw  27436  vmaprm  27437  vmacl  27438  efvmacl  27440  muval1  27453  chtprm  27473  chtdif  27478  efchtdvds  27479  dvdsppwf1o  27506  sgmppw  27517  0sgmppw  27518  1sgmprm  27519  vmalelog  27525  chtleppi  27530  chtublem  27531  fsumvma2  27534  vmasum  27536  chpchtsum  27539  chpub  27540  mersenne  27547  perfect1  27548  perfect  27551  pcbcctr  27596  bpos1lem  27602  bposlem1  27604  bposlem2  27605  bposlem6  27609  lgslem1  27617  lgsval2lem  27627  lgsvalmod  27636  lgsmod  27643  lgsdirprm  27651  lgsne0  27655  lgsprme0  27659  lgsqrlem1  27666  lgsqrlem2  27667  lgsqrlem4  27669  lgsqr  27671  lgsqrmod  27672  lgsqrmodndvds  27673  gausslemma2dlem0c  27678  gausslemma2dlem0i  27684  gausslemma2dlem1a  27685  gausslemma2dlem5a  27690  gausslemma2dlem7  27693  gausslemma2d  27694  lgseisenlem1  27695  lgseisenlem2  27696  lgseisenlem3  27697  lgseisenlem4  27698  lgsquadlem1  27700  lgsquadlem3  27702  lgsquad2lem2  27705  lgsquad2  27706  m1lgs  27708  2lgslem1a  27711  2lgslem1c  27713  2lgs  27727  2sqlem3  27740  2sqlem8  27746  2sqlem11  27749  2sqblem  27751  2sqmod  27756  chtppilimlem1  27793  rplogsumlem2  27805  rpvmasumlem  27807  dchrisum0flblem1  27828  dchrisum0flblem2  27829  padicabvf  27951  ostth1  27953  ostth3  27958  fltoprm  27988  hashecclwwlkn1  30661  umgrhashecclwwlk  30662  fusgrhashclwwlkn  30663  clwlksndivn  30670  numclwwlk5  30982  numclwwlk6  30984  numclwwlk7  30985  numclwwlk8  30986  znfermltl  33915  ply1fermltl  34111  cos9thpiminplylem2  34408  nn0prpwlem  37090  nn0prpw  37091  aks4d1p6  43111  aks4d1p8d1  43114  aks4d1p8d2  43115  aks4d1p8d3  43116  aks4d1p8  43117  aks6d1c1p2  43139  aks6d1c1p3  43140  aks6d1c1  43146  aks6d1c2p1  43148  aks6d1c2p2  43149  aks6d1c3  43153  aks6d1c4  43154  aks6d1c2lem4  43157  aks6d1c5lem1  43166  aks6d1c6lem3  43202  aks6d1c6lem4  43203  aks6d1c7lem1  43210  aks6d1c7  43214  aks5lem1  43216  aks5lem2  43217  aks5lem3a  43219  aks5lem8  43231  aks5  43234  nzprmdif  45288  etransclem41  47254  etransclem44  47257  etransclem47  47260  etransclem48  47261  odz2prm2pw  48617  fmtnoprmfac1lem  48618  fmtnoprmfac1  48619  fmtnoprmfac2  48621  prmdvdsfmtnof1lem2  48639  2pwp1prm  48643  sfprmdvdsmersenne  48657  lighneallem2  48660  lighneallem3  48661  lighneallem4  48664  lighneal  48665  perfectALTV  48790  gbepos  48825  gbowpos  48826  sbgoldbaltlem1  48846  ztprmneprm  49428