Theorem prmnn 16637

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

Syntax hints:   → wi 4   ∈ wcel 2114  {crab 3390   class class class wbr 5086  2_oc2o 8393   ≈ cen 8884  ℕcn 12168   ∥ cdvds 16215  ℙcprime 16634

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-prm 16635

This theorem is referenced by:  prmz  16638  prmssnn  16639  0nprm  16641  2mulprm  16656  nprmdvds1  16670  isprm5  16671  coprm  16675  prmdvdsexpr  16681  prmndvdsfaclt  16689  prmdvdsbc  16690  prmdvdsncoprmbd  16691  cncongrprm  16693  phiprmpw  16740  fermltl  16748  prmdiv  16749  prmdiveq  16750  prmdivdiv  16751  m1dvdsndvds  16763  vfermltl  16766  vfermltlALT  16767  powm2modprm  16768  reumodprminv  16769  modprm0  16770  nnnn0modprm0  16771  modprmn0modprm0  16772  oddprm  16775  nnoddn2prm  16776  prm23lt5  16779  pcpremul  16808  pcdvdsb  16834  pcelnn  16835  pcidlem  16837  pcid  16838  pcdvdstr  16841  pcgcd1  16842  pcprmpw2  16847  dvdsprmpweqnn  16850  dvdsprmpweqle  16851  pcaddlem  16853  pcadd  16854  pcmptcl  16856  pcmpt  16857  pcmpt2  16858  pcfaclem  16863  pcfac  16864  pcbc  16865  expnprm  16867  oddprmdvds  16868  prmpwdvds  16869  pockthlem  16870  pockthg  16871  pockthi  16872  prmreclem4  16884  prmreclem5  16885  prmreclem6  16886  prmrec  16887  1arith  16892  4sqlem11  16920  4sqlem12  16921  4sqlem13  16922  4sqlem14  16923  4sqlem17  16926  4sqlem18  16927  4sqlem19  16928  prmdvdsprmo  17007  prmgaplem3  17018  prmgaplem4  17019  prmgaplem5  17020  prmgaplem6  17021  prmgaplem8  17023  cshwshashnsame  17068  cshwshash  17069  prmlem1a  17071  pgpfi1  19564  pgp0  19565  sylow1lem1  19567  sylow1lem3  19569  sylow1lem4  19570  sylow1lem5  19571  odcau  19573  pgpfi  19574  fislw  19594  sylow3lem6  19601  gexexlem  19821  prmcyg  19863  ablfac1lem  20039  ablfac1b  20041  ablfac1eu  20044  pgpfac1lem3a  20047  pgpfac1lem3  20048  ablfaclem3  20058  prmgrpsimpgd  20085  prmirredlem  21465  dfprm2  21466  prmirred  21467  fermltlchr  21522  znfld  21553  freshmansdream  21567  frobrhm  21568  ply1fermltlchr  22290  rtprmirr  26740  wilthlem1  27048  wilthlem2  27049  wilthlem3  27050  chtf  27088  efchtcl  27091  isppw2  27095  vmappw  27096  vmaprm  27097  vmacl  27098  efvmacl  27100  muval1  27113  chtprm  27133  chtdif  27138  efchtdvds  27139  dvdsppwf1o  27166  sgmppw  27177  0sgmppw  27178  1sgmprm  27179  vmalelog  27185  chtleppi  27190  chtublem  27191  fsumvma2  27194  vmasum  27196  chpchtsum  27199  chpub  27200  mersenne  27207  perfect1  27208  perfect  27211  pcbcctr  27256  bpos1lem  27262  bposlem1  27264  bposlem2  27265  bposlem6  27269  lgslem1  27277  lgsval2lem  27287  lgsvalmod  27296  lgsmod  27303  lgsdirprm  27311  lgsne0  27315  lgsprme0  27319  lgsqrlem1  27326  lgsqrlem2  27327  lgsqrlem4  27329  lgsqr  27331  lgsqrmod  27332  lgsqrmodndvds  27333  gausslemma2dlem0c  27338  gausslemma2dlem0i  27344  gausslemma2dlem1a  27345  gausslemma2dlem5a  27350  gausslemma2dlem7  27353  gausslemma2d  27354  lgseisenlem1  27355  lgseisenlem2  27356  lgseisenlem3  27357  lgseisenlem4  27358  lgsquadlem1  27360  lgsquadlem3  27362  lgsquad2lem2  27365  lgsquad2  27366  m1lgs  27368  2lgslem1a  27371  2lgslem1c  27373  2lgs  27387  2sqlem3  27400  2sqlem8  27406  2sqlem11  27409  2sqblem  27411  2sqmod  27416  chtppilimlem1  27453  rplogsumlem2  27465  rpvmasumlem  27467  dchrisum0flblem1  27488  dchrisum0flblem2  27489  padicabvf  27611  ostth1  27613  ostth3  27618  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  fusgrhashclwwlkn  30167  clwlksndivn  30174  numclwwlk5  30476  numclwwlk6  30478  numclwwlk7  30479  numclwwlk8  30480  znfermltl  33444  ply1fermltl  33664  cos9thpiminplylem2  33946  nn0prpwlem  36523  nn0prpw  36524  aks4d1p6  42537  aks4d1p8d1  42540  aks4d1p8d2  42541  aks4d1p8d3  42542  aks4d1p8  42543  aks6d1c1p2  42565  aks6d1c1p3  42566  aks6d1c1  42572  aks6d1c2p1  42574  aks6d1c2p2  42575  aks6d1c3  42579  aks6d1c4  42580  aks6d1c2lem4  42583  aks6d1c5lem1  42592  aks6d1c6lem3  42628  aks6d1c6lem4  42629  aks6d1c7lem1  42636  aks6d1c7  42640  aks5lem1  42642  aks5lem2  42643  aks5lem3a  42645  aks5lem8  42657  aks5  42660  nzprmdif  44767  etransclem41  46724  etransclem44  46727  etransclem47  46730  etransclem48  46731  odz2prm2pw  48041  fmtnoprmfac1lem  48042  fmtnoprmfac1  48043  fmtnoprmfac2  48045  prmdvdsfmtnof1lem2  48063  2pwp1prm  48067  sfprmdvdsmersenne  48081  lighneallem2  48084  lighneallem3  48085  lighneallem4  48088  lighneal  48089  perfectALTV  48214  gbepos  48249  gbowpos  48250  sbgoldbaltlem1  48270  ztprmneprm  48838