Theorem prmnn 16599

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

Syntax hints:   → wi 4   ∈ wcel 2113  {crab 3397   class class class wbr 5096  2_oc2o 8389   ≈ cen 8878  ℕcn 12143   ∥ cdvds 16177  ℙcprime 16596

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-prm 16597

This theorem is referenced by:  prmz  16600  prmssnn  16601  0nprm  16603  2mulprm  16618  nprmdvds1  16631  isprm5  16632  coprm  16636  prmdvdsexpr  16642  prmndvdsfaclt  16650  prmdvdsbc  16651  prmdvdsncoprmbd  16652  cncongrprm  16654  phiprmpw  16701  fermltl  16709  prmdiv  16710  prmdiveq  16711  prmdivdiv  16712  m1dvdsndvds  16724  vfermltl  16727  vfermltlALT  16728  powm2modprm  16729  reumodprminv  16730  modprm0  16731  nnnn0modprm0  16732  modprmn0modprm0  16733  oddprm  16736  nnoddn2prm  16737  prm23lt5  16740  pcpremul  16769  pcdvdsb  16795  pcelnn  16796  pcidlem  16798  pcid  16799  pcdvdstr  16802  pcgcd1  16803  pcprmpw2  16808  dvdsprmpweqnn  16811  dvdsprmpweqle  16812  pcaddlem  16814  pcadd  16815  pcmptcl  16817  pcmpt  16818  pcmpt2  16819  pcfaclem  16824  pcfac  16825  pcbc  16826  expnprm  16828  oddprmdvds  16829  prmpwdvds  16830  pockthlem  16831  pockthg  16832  pockthi  16833  prmreclem4  16845  prmreclem5  16846  prmreclem6  16847  prmrec  16848  1arith  16853  4sqlem11  16881  4sqlem12  16882  4sqlem13  16883  4sqlem14  16884  4sqlem17  16887  4sqlem18  16888  4sqlem19  16889  prmdvdsprmo  16968  prmgaplem3  16979  prmgaplem4  16980  prmgaplem5  16981  prmgaplem6  16982  prmgaplem8  16984  cshwshashnsame  17029  cshwshash  17030  prmlem1a  17032  pgpfi1  19522  pgp0  19523  sylow1lem1  19525  sylow1lem3  19527  sylow1lem4  19528  sylow1lem5  19529  odcau  19531  pgpfi  19532  fislw  19552  sylow3lem6  19559  gexexlem  19779  prmcyg  19821  ablfac1lem  19997  ablfac1b  19999  ablfac1eu  20002  pgpfac1lem3a  20005  pgpfac1lem3  20006  ablfaclem3  20016  prmgrpsimpgd  20043  prmirredlem  21425  dfprm2  21426  prmirred  21427  fermltlchr  21482  znfld  21513  freshmansdream  21527  frobrhm  21528  ply1fermltlchr  22254  rtprmirr  26724  wilthlem1  27032  wilthlem2  27033  wilthlem3  27034  chtf  27072  efchtcl  27075  isppw2  27079  vmappw  27080  vmaprm  27081  vmacl  27082  efvmacl  27084  muval1  27097  chtprm  27117  chtdif  27122  efchtdvds  27123  dvdsppwf1o  27150  sgmppw  27162  0sgmppw  27163  1sgmprm  27164  vmalelog  27170  chtleppi  27175  chtublem  27176  fsumvma2  27179  vmasum  27181  chpchtsum  27184  chpub  27185  mersenne  27192  perfect1  27193  perfect  27196  pcbcctr  27241  bpos1lem  27247  bposlem1  27249  bposlem2  27250  bposlem6  27254  lgslem1  27262  lgsval2lem  27272  lgsvalmod  27281  lgsmod  27288  lgsdirprm  27296  lgsne0  27300  lgsprme0  27304  lgsqrlem1  27311  lgsqrlem2  27312  lgsqrlem4  27314  lgsqr  27316  lgsqrmod  27317  lgsqrmodndvds  27318  gausslemma2dlem0c  27323  gausslemma2dlem0i  27329  gausslemma2dlem1a  27330  gausslemma2dlem5a  27335  gausslemma2dlem7  27338  gausslemma2d  27339  lgseisenlem1  27340  lgseisenlem2  27341  lgseisenlem3  27342  lgseisenlem4  27343  lgsquadlem1  27345  lgsquadlem3  27347  lgsquad2lem2  27350  lgsquad2  27351  m1lgs  27353  2lgslem1a  27356  2lgslem1c  27358  2lgs  27372  2sqlem3  27385  2sqlem8  27391  2sqlem11  27394  2sqblem  27396  2sqmod  27401  chtppilimlem1  27438  rplogsumlem2  27450  rpvmasumlem  27452  dchrisum0flblem1  27473  dchrisum0flblem2  27474  padicabvf  27596  ostth1  27598  ostth3  27603  hashecclwwlkn1  30101  umgrhashecclwwlk  30102  fusgrhashclwwlkn  30103  clwlksndivn  30110  numclwwlk5  30412  numclwwlk6  30414  numclwwlk7  30415  numclwwlk8  30416  znfermltl  33396  ply1fermltl  33616  cos9thpiminplylem2  33889  nn0prpwlem  36465  nn0prpw  36466  aks4d1p6  42274  aks4d1p8d1  42277  aks4d1p8d2  42278  aks4d1p8d3  42279  aks4d1p8  42280  aks6d1c1p2  42302  aks6d1c1p3  42303  aks6d1c1  42309  aks6d1c2p1  42311  aks6d1c2p2  42312  aks6d1c3  42316  aks6d1c4  42317  aks6d1c2lem4  42320  aks6d1c5lem1  42329  aks6d1c6lem3  42365  aks6d1c6lem4  42366  aks6d1c7lem1  42373  aks6d1c7  42377  aks5lem1  42379  aks5lem2  42380  aks5lem3a  42382  aks5lem8  42394  aks5  42397  nzprmdif  44502  etransclem41  46461  etransclem44  46464  etransclem47  46467  etransclem48  46468  odz2prm2pw  47751  fmtnoprmfac1lem  47752  fmtnoprmfac1  47753  fmtnoprmfac2  47755  prmdvdsfmtnof1lem2  47773  2pwp1prm  47777  sfprmdvdsmersenne  47791  lighneallem2  47794  lighneallem3  47795  lighneallem4  47798  lighneal  47799  perfectALTV  47911  gbepos  47946  gbowpos  47947  sbgoldbaltlem1  47967  ztprmneprm  48535