Theorem prmnn 16721

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

Syntax hints:   → wi 4   ∈ wcel 2108  {crab 3443   class class class wbr 5166  2_oc2o 8516   ≈ cen 9000  ℕcn 12293   ∥ cdvds 16302  ℙcprime 16718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-prm 16719

This theorem is referenced by:  prmz  16722  prmssnn  16723  0nprm  16725  2mulprm  16740  nprmdvds1  16753  isprm5  16754  coprm  16758  prmdvdsexpr  16764  prmndvdsfaclt  16772  prmdvdsbc  16773  prmdvdsncoprmbd  16774  cncongrprm  16776  phiprmpw  16823  fermltl  16831  prmdiv  16832  prmdiveq  16833  prmdivdiv  16834  m1dvdsndvds  16845  vfermltl  16848  vfermltlALT  16849  powm2modprm  16850  reumodprminv  16851  modprm0  16852  nnnn0modprm0  16853  modprmn0modprm0  16854  oddprm  16857  nnoddn2prm  16858  prm23lt5  16861  pcpremul  16890  pcdvdsb  16916  pcelnn  16917  pcidlem  16919  pcid  16920  pcdvdstr  16923  pcgcd1  16924  pcprmpw2  16929  dvdsprmpweqnn  16932  dvdsprmpweqle  16933  pcaddlem  16935  pcadd  16936  pcmptcl  16938  pcmpt  16939  pcmpt2  16940  pcfaclem  16945  pcfac  16946  pcbc  16947  expnprm  16949  oddprmdvds  16950  prmpwdvds  16951  pockthlem  16952  pockthg  16953  pockthi  16954  prmreclem4  16966  prmreclem5  16967  prmreclem6  16968  prmrec  16969  1arith  16974  4sqlem11  17002  4sqlem12  17003  4sqlem13  17004  4sqlem14  17005  4sqlem17  17008  4sqlem18  17009  4sqlem19  17010  prmdvdsprmo  17089  prmgaplem3  17100  prmgaplem4  17101  prmgaplem5  17102  prmgaplem6  17103  prmgaplem8  17105  cshwshashnsame  17151  cshwshash  17152  prmlem1a  17154  pgpfi1  19637  pgp0  19638  sylow1lem1  19640  sylow1lem3  19642  sylow1lem4  19643  sylow1lem5  19644  odcau  19646  pgpfi  19647  fislw  19667  sylow3lem6  19674  gexexlem  19894  prmcyg  19936  ablfac1lem  20112  ablfac1b  20114  ablfac1eu  20117  pgpfac1lem3a  20120  pgpfac1lem3  20121  ablfaclem3  20131  prmgrpsimpgd  20158  prmirredlem  21506  dfprm2  21507  prmirred  21508  fermltlchr  21567  znfld  21602  freshmansdream  21616  frobrhm  21617  ply1fermltlchr  22337  rtprmirr  26821  wilthlem1  27129  wilthlem2  27130  wilthlem3  27131  chtf  27169  efchtcl  27172  isppw2  27176  vmappw  27177  vmaprm  27178  vmacl  27179  efvmacl  27181  muval1  27194  chtprm  27214  chtdif  27219  efchtdvds  27220  dvdsppwf1o  27247  sgmppw  27259  0sgmppw  27260  1sgmprm  27261  vmalelog  27267  chtleppi  27272  chtublem  27273  fsumvma2  27276  vmasum  27278  chpchtsum  27281  chpub  27282  mersenne  27289  perfect1  27290  perfect  27293  pcbcctr  27338  bpos1lem  27344  bposlem1  27346  bposlem2  27347  bposlem6  27351  lgslem1  27359  lgsval2lem  27369  lgsvalmod  27378  lgsmod  27385  lgsdirprm  27393  lgsne0  27397  lgsprme0  27401  lgsqrlem1  27408  lgsqrlem2  27409  lgsqrlem4  27411  lgsqr  27413  lgsqrmod  27414  lgsqrmodndvds  27415  gausslemma2dlem0c  27420  gausslemma2dlem0i  27426  gausslemma2dlem1a  27427  gausslemma2dlem5a  27432  gausslemma2dlem7  27435  gausslemma2d  27436  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisenlem4  27440  lgsquadlem1  27442  lgsquadlem3  27444  lgsquad2lem2  27447  lgsquad2  27448  m1lgs  27450  2lgslem1a  27453  2lgslem1c  27455  2lgs  27469  2sqlem3  27482  2sqlem8  27488  2sqlem11  27491  2sqblem  27493  2sqmod  27498  chtppilimlem1  27535  rplogsumlem2  27547  rpvmasumlem  27549  dchrisum0flblem1  27570  dchrisum0flblem2  27571  padicabvf  27693  ostth1  27695  ostth3  27700  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  fusgrhashclwwlkn  30111  clwlksndivn  30118  numclwwlk5  30420  numclwwlk6  30422  numclwwlk7  30423  numclwwlk8  30424  znfermltl  33359  ply1fermltl  33574  nn0prpwlem  36288  nn0prpw  36289  aks4d1p6  42038  aks4d1p8d1  42041  aks4d1p8d2  42042  aks4d1p8d3  42043  aks4d1p8  42044  aks6d1c1p2  42066  aks6d1c1p3  42067  aks6d1c1  42073  aks6d1c2p1  42075  aks6d1c2p2  42076  aks6d1c3  42080  aks6d1c4  42081  aks6d1c2lem4  42084  aks6d1c5lem1  42093  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c7lem1  42137  aks6d1c7  42141  aks5lem1  42143  aks5lem2  42144  aks5lem3a  42146  aks5lem8  42158  aks5  42161  nzprmdif  44288  etransclem41  46196  etransclem44  46199  etransclem47  46202  etransclem48  46203  odz2prm2pw  47437  fmtnoprmfac1lem  47438  fmtnoprmfac1  47439  fmtnoprmfac2  47441  prmdvdsfmtnof1lem2  47459  2pwp1prm  47463  sfprmdvdsmersenne  47477  lighneallem2  47480  lighneallem3  47481  lighneallem4  47484  lighneal  47485  perfectALTV  47597  gbepos  47632  gbowpos  47633  sbgoldbaltlem1  47653  ztprmneprm  48072