Theorem prmnn 16764

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {crab 3412   class class class wbr 5103  2_oc2o 8449   ≈ cen 8949  ℕcn 12257   ∥ cdvds 16342  ℙcprime 16761

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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 16762

This theorem is used by:  prmz  16765  prmssnn  16766  0nprm  16768  2mulprm  16783  nprmdvds1  16797  isprm5  16798  coprm  16802  prmdvdsexpr  16808  prmndvdsfaclt  16816  prmdvdsbc  16817  prmdvdsncoprmbd  16818  cncongrprm  16820  phiprmpw  16867  fermltl  16875  prmdiv  16876  prmdiveq  16877  prmdivdiv  16878  m1dvdsndvds  16890  vfermltl  16893  vfermltlALT  16894  powm2modprm  16895  reumodprminv  16896  modprm0  16897  nnnn0modprm0  16898  modprmn0modprm0  16899  oddprm  16902  nnoddn2prm  16903  prm23lt5  16906  pcpremul  16935  pcdvdsb  16961  pcelnn  16962  pcidlem  16964  pcid  16965  pcdvdstr  16968  pcgcd1  16969  pcprmpw2  16974  dvdsprmpweqnn  16977  dvdsprmpweqle  16978  pcaddlem  16980  pcadd  16981  pcmptcl  16983  pcmpt  16984  pcmpt2  16985  pcfaclem  16990  pcfac  16991  pcbc  16992  expnprm  16994  oddprmdvds  16995  prmpwdvds  16996  pockthlem  16997  pockthg  16998  pockthi  16999  prmreclem4  17011  prmreclem5  17012  prmreclem6  17013  prmrec  17014  1arith  17019  4sqlem11  17047  4sqlem12  17048  4sqlem13  17049  4sqlem14  17050  4sqlem17  17053  4sqlem18  17054  4sqlem19  17055  prmdvdsprmo  17134  prmgaplem3  17145  prmgaplem4  17146  prmgaplem5  17147  prmgaplem6  17148  prmgaplem8  17150  cshwshashnsame  17195  cshwshash  17196  prmlem1a  17198  pgpfi1  19722  pgp0  19723  sylow1lem1  19725  sylow1lem3  19727  sylow1lem4  19728  sylow1lem5  19729  odcau  19731  pgpfi  19732  fislw  19752  sylow3lem6  19759  gexexlem  19979  prmcyg  20021  ablfac1lem  20197  ablfac1b  20199  ablfac1eu  20202  pgpfac1lem3a  20205  pgpfac1lem3  20206  ablfaclem3  20216  prmgrpsimpgd  20243  prmirredlem  21685  dfprm2  21686  prmirred  21687  fermltlchr  21742  znfld  21773  freshmansdream  21787  frobrhm  21788  ply1fermltlchr  22537  rtprmirr  26997  wilthlem1  27304  wilthlem2  27305  wilthlem3  27306  chtf  27344  efchtcl  27347  isppw2  27351  vmappw  27352  vmaprm  27353  vmacl  27354  efvmacl  27356  muval1  27369  chtprm  27389  chtdif  27394  efchtdvds  27395  dvdsppwf1o  27422  sgmppw  27433  0sgmppw  27434  1sgmprm  27435  vmalelog  27441  chtleppi  27446  chtublem  27447  fsumvma2  27450  vmasum  27452  chpchtsum  27455  chpub  27456  mersenne  27463  perfect1  27464  perfect  27467  pcbcctr  27512  bpos1lem  27518  bposlem1  27520  bposlem2  27521  bposlem6  27525  lgslem1  27533  lgsval2lem  27543  lgsvalmod  27552  lgsmod  27559  lgsdirprm  27567  lgsne0  27571  lgsprme0  27575  lgsqrlem1  27582  lgsqrlem2  27583  lgsqrlem4  27585  lgsqr  27587  lgsqrmod  27588  lgsqrmodndvds  27589  gausslemma2dlem0c  27594  gausslemma2dlem0i  27600  gausslemma2dlem1a  27601  gausslemma2dlem5a  27606  gausslemma2dlem7  27609  gausslemma2d  27610  lgseisenlem1  27611  lgseisenlem2  27612  lgseisenlem3  27613  lgseisenlem4  27614  lgsquadlem1  27616  lgsquadlem3  27618  lgsquad2lem2  27621  lgsquad2  27622  m1lgs  27624  2lgslem1a  27627  2lgslem1c  27629  2lgs  27643  2sqlem3  27656  2sqlem8  27662  2sqlem11  27665  2sqblem  27667  2sqmod  27672  chtppilimlem1  27709  rplogsumlem2  27721  rpvmasumlem  27723  dchrisum0flblem1  27744  dchrisum0flblem2  27745  padicabvf  27867  ostth1  27869  ostth3  27874  hashecclwwlkn1  30547  umgrhashecclwwlk  30548  fusgrhashclwwlkn  30549  clwlksndivn  30556  numclwwlk5  30868  numclwwlk6  30870  numclwwlk7  30871  numclwwlk8  30872  znfermltl  33801  ply1fermltl  33996  cos9thpiminplylem2  34293  nn0prpwlem  36941  nn0prpw  36942  aks4d1p6  42947  aks4d1p8d1  42950  aks4d1p8d2  42951  aks4d1p8d3  42952  aks4d1p8  42953  aks6d1c1p2  42975  aks6d1c1p3  42976  aks6d1c1  42982  aks6d1c2p1  42984  aks6d1c2p2  42985  aks6d1c3  42989  aks6d1c4  42990  aks6d1c2lem4  42993  aks6d1c5lem1  43002  aks6d1c6lem3  43038  aks6d1c6lem4  43039  aks6d1c7lem1  43046  aks6d1c7  43050  aks5lem1  43052  aks5lem2  43053  aks5lem3a  43055  aks5lem8  43067  aks5  43070  nzprmdif  45143  etransclem41  47103  etransclem44  47106  etransclem47  47109  etransclem48  47110  odz2prm2pw  48466  fmtnoprmfac1lem  48467  fmtnoprmfac1  48468  fmtnoprmfac2  48470  prmdvdsfmtnof1lem2  48488  2pwp1prm  48492  sfprmdvdsmersenne  48506  lighneallem2  48509  lighneallem3  48510  lighneallem4  48513  lighneal  48514  perfectALTV  48639  gbepos  48674  gbowpos  48675  sbgoldbaltlem1  48695  ztprmneprm  49277