Theorem prmnn 16307

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

Syntax hints:   → wi 4   ∈ wcel 2108  {crab 3067   class class class wbr 5070  2_oc2o 8261   ≈ cen 8688  ℕcn 11903   ∥ cdvds 15891  ℙcprime 16304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-prm 16305

This theorem is referenced by:  prmz  16308  prmssnn  16309  0nprm  16311  2mulprm  16326  nprmdvds1  16339  isprm5  16340  coprm  16344  prmdvdsexpr  16350  prmndvdsfaclt  16358  prmdvdsncoprmbd  16359  cncongrprm  16361  phiprmpw  16405  fermltl  16413  prmdiv  16414  prmdiveq  16415  prmdivdiv  16416  m1dvdsndvds  16427  vfermltl  16430  vfermltlALT  16431  powm2modprm  16432  reumodprminv  16433  modprm0  16434  nnnn0modprm0  16435  modprmn0modprm0  16436  oddprm  16439  nnoddn2prm  16440  prm23lt5  16443  pcpremul  16472  pcdvdsb  16498  pcelnn  16499  pcidlem  16501  pcid  16502  pcdvdstr  16505  pcgcd1  16506  pcprmpw2  16511  dvdsprmpweqnn  16514  dvdsprmpweqle  16515  pcaddlem  16517  pcadd  16518  pcmptcl  16520  pcmpt  16521  pcmpt2  16522  pcfaclem  16527  pcfac  16528  pcbc  16529  expnprm  16531  oddprmdvds  16532  prmpwdvds  16533  pockthlem  16534  pockthg  16535  pockthi  16536  prmreclem4  16548  prmreclem5  16549  prmreclem6  16550  prmrec  16551  1arith  16556  4sqlem11  16584  4sqlem12  16585  4sqlem13  16586  4sqlem14  16587  4sqlem17  16590  4sqlem18  16591  4sqlem19  16592  prmdvdsprmo  16671  prmgaplem3  16682  prmgaplem4  16683  prmgaplem5  16684  prmgaplem6  16685  prmgaplem8  16687  cshwshashnsame  16733  cshwshash  16734  prmlem1a  16736  pgpfi1  19115  pgp0  19116  sylow1lem1  19118  sylow1lem3  19120  sylow1lem4  19121  sylow1lem5  19122  odcau  19124  pgpfi  19125  fislw  19145  sylow3lem6  19152  gexexlem  19368  prmcyg  19410  ablfac1lem  19586  ablfac1b  19588  ablfac1eu  19591  pgpfac1lem3a  19594  pgpfac1lem3  19595  ablfaclem3  19605  prmgrpsimpgd  19632  prmirredlem  20606  dfprm2  20607  prmirred  20608  znfld  20680  wilthlem1  26122  wilthlem2  26123  wilthlem3  26124  chtf  26162  efchtcl  26165  isppw2  26169  vmappw  26170  vmaprm  26171  vmacl  26172  efvmacl  26174  muval1  26187  chtprm  26207  chtdif  26212  efchtdvds  26213  dvdsppwf1o  26240  sgmppw  26250  0sgmppw  26251  1sgmprm  26252  vmalelog  26258  chtleppi  26263  chtublem  26264  fsumvma2  26267  vmasum  26269  chpchtsum  26272  chpub  26273  mersenne  26280  perfect1  26281  perfect  26284  pcbcctr  26329  bpos1lem  26335  bposlem1  26337  bposlem2  26338  bposlem6  26342  lgslem1  26350  lgsval2lem  26360  lgsvalmod  26369  lgsmod  26376  lgsdirprm  26384  lgsne0  26388  lgsprme0  26392  lgsqrlem1  26399  lgsqrlem2  26400  lgsqrlem4  26402  lgsqr  26404  lgsqrmod  26405  lgsqrmodndvds  26406  gausslemma2dlem0c  26411  gausslemma2dlem0i  26417  gausslemma2dlem1a  26418  gausslemma2dlem5a  26423  gausslemma2dlem7  26426  gausslemma2d  26427  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgseisenlem4  26431  lgsquadlem1  26433  lgsquadlem3  26435  lgsquad2lem2  26438  lgsquad2  26439  m1lgs  26441  2lgslem1a  26444  2lgslem1c  26446  2lgs  26460  2sqlem3  26473  2sqlem8  26479  2sqlem11  26482  2sqblem  26484  2sqmod  26489  chtppilimlem1  26526  rplogsumlem2  26538  rpvmasumlem  26540  dchrisum0flblem1  26561  dchrisum0flblem2  26562  padicabvf  26684  ostth1  26686  ostth3  26691  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  fusgrhashclwwlkn  28344  clwlksndivn  28351  numclwwlk5  28653  numclwwlk6  28655  numclwwlk7  28656  numclwwlk8  28657  prmdvdsbc  31032  freshmansdream  31386  frobrhm  31387  znfermltl  31464  ply1fermltl  31572  nn0prpwlem  34438  nn0prpw  34439  aks4d1p6  40017  aks4d1p8d1  40020  aks4d1p8d2  40021  aks4d1p8d3  40022  aks4d1p8  40023  rtprmirr  40268  nzprmdif  41826  etransclem41  43706  etransclem44  43709  etransclem47  43712  etransclem48  43713  odz2prm2pw  44903  fmtnoprmfac1lem  44904  fmtnoprmfac1  44905  fmtnoprmfac2  44907  prmdvdsfmtnof1lem2  44925  2pwp1prm  44929  sfprmdvdsmersenne  44943  lighneallem2  44946  lighneallem3  44947  lighneallem4  44950  lighneal  44951  perfectALTV  45063  gbepos  45098  gbowpos  45099  sbgoldbaltlem1  45119  ztprmneprm  45571