Theorem prmnn 16379

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

Syntax hints:   → wi 4   ∈ wcel 2106  {crab 3068   class class class wbr 5074  2_oc2o 8291   ≈ cen 8730  ℕcn 11973   ∥ cdvds 15963  ℙcprime 16376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-prm 16377

This theorem is referenced by:  prmz  16380  prmssnn  16381  0nprm  16383  2mulprm  16398  nprmdvds1  16411  isprm5  16412  coprm  16416  prmdvdsexpr  16422  prmndvdsfaclt  16430  prmdvdsncoprmbd  16431  cncongrprm  16433  phiprmpw  16477  fermltl  16485  prmdiv  16486  prmdiveq  16487  prmdivdiv  16488  m1dvdsndvds  16499  vfermltl  16502  vfermltlALT  16503  powm2modprm  16504  reumodprminv  16505  modprm0  16506  nnnn0modprm0  16507  modprmn0modprm0  16508  oddprm  16511  nnoddn2prm  16512  prm23lt5  16515  pcpremul  16544  pcdvdsb  16570  pcelnn  16571  pcidlem  16573  pcid  16574  pcdvdstr  16577  pcgcd1  16578  pcprmpw2  16583  dvdsprmpweqnn  16586  dvdsprmpweqle  16587  pcaddlem  16589  pcadd  16590  pcmptcl  16592  pcmpt  16593  pcmpt2  16594  pcfaclem  16599  pcfac  16600  pcbc  16601  expnprm  16603  oddprmdvds  16604  prmpwdvds  16605  pockthlem  16606  pockthg  16607  pockthi  16608  prmreclem4  16620  prmreclem5  16621  prmreclem6  16622  prmrec  16623  1arith  16628  4sqlem11  16656  4sqlem12  16657  4sqlem13  16658  4sqlem14  16659  4sqlem17  16662  4sqlem18  16663  4sqlem19  16664  prmdvdsprmo  16743  prmgaplem3  16754  prmgaplem4  16755  prmgaplem5  16756  prmgaplem6  16757  prmgaplem8  16759  cshwshashnsame  16805  cshwshash  16806  prmlem1a  16808  pgpfi1  19200  pgp0  19201  sylow1lem1  19203  sylow1lem3  19205  sylow1lem4  19206  sylow1lem5  19207  odcau  19209  pgpfi  19210  fislw  19230  sylow3lem6  19237  gexexlem  19453  prmcyg  19495  ablfac1lem  19671  ablfac1b  19673  ablfac1eu  19676  pgpfac1lem3a  19679  pgpfac1lem3  19680  ablfaclem3  19690  prmgrpsimpgd  19717  prmirredlem  20694  dfprm2  20695  prmirred  20696  znfld  20768  wilthlem1  26217  wilthlem2  26218  wilthlem3  26219  chtf  26257  efchtcl  26260  isppw2  26264  vmappw  26265  vmaprm  26266  vmacl  26267  efvmacl  26269  muval1  26282  chtprm  26302  chtdif  26307  efchtdvds  26308  dvdsppwf1o  26335  sgmppw  26345  0sgmppw  26346  1sgmprm  26347  vmalelog  26353  chtleppi  26358  chtublem  26359  fsumvma2  26362  vmasum  26364  chpchtsum  26367  chpub  26368  mersenne  26375  perfect1  26376  perfect  26379  pcbcctr  26424  bpos1lem  26430  bposlem1  26432  bposlem2  26433  bposlem6  26437  lgslem1  26445  lgsval2lem  26455  lgsvalmod  26464  lgsmod  26471  lgsdirprm  26479  lgsne0  26483  lgsprme0  26487  lgsqrlem1  26494  lgsqrlem2  26495  lgsqrlem4  26497  lgsqr  26499  lgsqrmod  26500  lgsqrmodndvds  26501  gausslemma2dlem0c  26506  gausslemma2dlem0i  26512  gausslemma2dlem1a  26513  gausslemma2dlem5a  26518  gausslemma2dlem7  26521  gausslemma2d  26522  lgseisenlem1  26523  lgseisenlem2  26524  lgseisenlem3  26525  lgseisenlem4  26526  lgsquadlem1  26528  lgsquadlem3  26530  lgsquad2lem2  26533  lgsquad2  26534  m1lgs  26536  2lgslem1a  26539  2lgslem1c  26541  2lgs  26555  2sqlem3  26568  2sqlem8  26574  2sqlem11  26577  2sqblem  26579  2sqmod  26584  chtppilimlem1  26621  rplogsumlem2  26633  rpvmasumlem  26635  dchrisum0flblem1  26656  dchrisum0flblem2  26657  padicabvf  26779  ostth1  26781  ostth3  26786  hashecclwwlkn1  28441  umgrhashecclwwlk  28442  fusgrhashclwwlkn  28443  clwlksndivn  28450  numclwwlk5  28752  numclwwlk6  28754  numclwwlk7  28755  numclwwlk8  28756  prmdvdsbc  31130  freshmansdream  31484  frobrhm  31485  znfermltl  31562  ply1fermltl  31670  nn0prpwlem  34511  nn0prpw  34512  aks4d1p6  40089  aks4d1p8d1  40092  aks4d1p8d2  40093  aks4d1p8d3  40094  aks4d1p8  40095  rtprmirr  40347  nzprmdif  41937  etransclem41  43816  etransclem44  43819  etransclem47  43822  etransclem48  43823  odz2prm2pw  45015  fmtnoprmfac1lem  45016  fmtnoprmfac1  45017  fmtnoprmfac2  45019  prmdvdsfmtnof1lem2  45037  2pwp1prm  45041  sfprmdvdsmersenne  45055  lighneallem2  45058  lighneallem3  45059  lighneallem4  45062  lighneal  45063  perfectALTV  45175  gbepos  45210  gbowpos  45211  sbgoldbaltlem1  45231  ztprmneprm  45683