Theorem prmnn 16008

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

Syntax hints:   → wi 4   ∈ wcel 2111  {crab 3110   class class class wbr 5030  2_oc2o 8079   ≈ cen 8489  ℕcn 11625   ∥ cdvds 15599  ℙcprime 16005

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-prm 16006

This theorem is referenced by:  prmz  16009  prmssnn  16010  0nprm  16012  2mulprm  16027  nprmdvds1  16040  isprm5  16041  coprm  16045  prmdvdsexpr  16051  prmndvdsfaclt  16057  cncongrprm  16059  phiprmpw  16103  fermltl  16111  prmdiv  16112  prmdiveq  16113  prmdivdiv  16114  m1dvdsndvds  16125  vfermltl  16128  vfermltlALT  16129  powm2modprm  16130  reumodprminv  16131  modprm0  16132  nnnn0modprm0  16133  modprmn0modprm0  16134  oddprm  16137  nnoddn2prm  16138  prm23lt5  16141  pcpremul  16170  pcdvdsb  16195  pcelnn  16196  pcidlem  16198  pcid  16199  pcdvdstr  16202  pcgcd1  16203  pcprmpw2  16208  dvdsprmpweqnn  16211  dvdsprmpweqle  16212  pcaddlem  16214  pcadd  16215  pcmptcl  16217  pcmpt  16218  pcmpt2  16219  pcfaclem  16224  pcfac  16225  pcbc  16226  expnprm  16228  oddprmdvds  16229  prmpwdvds  16230  pockthlem  16231  pockthg  16232  pockthi  16233  prmreclem4  16245  prmreclem5  16246  prmreclem6  16247  prmrec  16248  1arith  16253  4sqlem11  16281  4sqlem12  16282  4sqlem13  16283  4sqlem14  16284  4sqlem17  16287  4sqlem18  16288  4sqlem19  16289  prmdvdsprmo  16368  prmgaplem3  16379  prmgaplem4  16380  prmgaplem5  16381  prmgaplem6  16382  prmgaplem8  16384  cshwshashnsame  16429  cshwshash  16430  prmlem1a  16432  pgpfi1  18712  pgp0  18713  sylow1lem1  18715  sylow1lem3  18717  sylow1lem4  18718  sylow1lem5  18719  odcau  18721  pgpfi  18722  fislw  18742  sylow3lem6  18749  gexexlem  18965  prmcyg  19007  ablfac1lem  19183  ablfac1b  19185  ablfac1eu  19188  pgpfac1lem3a  19191  pgpfac1lem3  19192  ablfaclem3  19202  prmgrpsimpgd  19229  prmirredlem  20186  dfprm2  20187  prmirred  20188  znfld  20252  wilthlem1  25653  wilthlem2  25654  wilthlem3  25655  chtf  25693  efchtcl  25696  isppw2  25700  vmappw  25701  vmaprm  25702  vmacl  25703  efvmacl  25705  muval1  25718  chtprm  25738  chtdif  25743  efchtdvds  25744  dvdsppwf1o  25771  sgmppw  25781  0sgmppw  25782  1sgmprm  25783  vmalelog  25789  chtleppi  25794  chtublem  25795  fsumvma2  25798  vmasum  25800  chpchtsum  25803  chpub  25804  mersenne  25811  perfect1  25812  perfect  25815  pcbcctr  25860  bpos1lem  25866  bposlem1  25868  bposlem2  25869  bposlem6  25873  lgslem1  25881  lgsval2lem  25891  lgsvalmod  25900  lgsmod  25907  lgsdirprm  25915  lgsne0  25919  lgsprme0  25923  lgsqrlem1  25930  lgsqrlem2  25931  lgsqrlem4  25933  lgsqr  25935  lgsqrmod  25936  lgsqrmodndvds  25937  gausslemma2dlem0c  25942  gausslemma2dlem0i  25948  gausslemma2dlem1a  25949  gausslemma2dlem5a  25954  gausslemma2dlem7  25957  gausslemma2d  25958  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem3  25961  lgseisenlem4  25962  lgsquadlem1  25964  lgsquadlem3  25966  lgsquad2lem2  25969  lgsquad2  25970  m1lgs  25972  2lgslem1a  25975  2lgslem1c  25977  2lgs  25991  2sqlem3  26004  2sqlem8  26010  2sqlem11  26013  2sqblem  26015  2sqmod  26020  chtppilimlem1  26057  rplogsumlem2  26069  rpvmasumlem  26071  dchrisum0flblem1  26092  dchrisum0flblem2  26093  padicabvf  26215  ostth1  26217  ostth3  26222  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  fusgrhashclwwlkn  27864  clwlksndivn  27871  numclwwlk5  28173  numclwwlk6  28175  numclwwlk7  28176  numclwwlk8  28177  prmdvdsbc  30558  freshmansdream  30909  frobrhm  30910  nn0prpwlem  33783  nn0prpw  33784  rtprmirr  39502  nzprmdif  41023  etransclem41  42917  etransclem44  42920  etransclem47  42923  etransclem48  42924  odz2prm2pw  44080  fmtnoprmfac1lem  44081  fmtnoprmfac1  44082  fmtnoprmfac2  44084  prmdvdsfmtnof1lem2  44102  2pwp1prm  44106  sfprmdvdsmersenne  44121  lighneallem2  44124  lighneallem3  44125  lighneallem4  44128  lighneal  44129  perfectALTV  44241  gbepos  44276  gbowpos  44277  sbgoldbaltlem1  44297  ztprmneprm  44749