Theorem prmnn 16689

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

Syntax hints:   → wi 4   ∈ wcel 2141  {crab 3413   class class class wbr 5099  2_oc2o 8424   ≈ cen 8918  ℕcn 12205   ∥ cdvds 16267  ℙcprime 16686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-prm 16687

This theorem is referenced by:  prmz  16690  prmssnn  16691  0nprm  16693  2mulprm  16708  nprmdvds1  16722  isprm5  16723  coprm  16727  prmdvdsexpr  16733  prmndvdsfaclt  16741  prmdvdsbc  16742  prmdvdsncoprmbd  16743  cncongrprm  16745  phiprmpw  16792  fermltl  16800  prmdiv  16801  prmdiveq  16802  prmdivdiv  16803  m1dvdsndvds  16815  vfermltl  16818  vfermltlALT  16819  powm2modprm  16820  reumodprminv  16821  modprm0  16822  nnnn0modprm0  16823  modprmn0modprm0  16824  oddprm  16827  nnoddn2prm  16828  prm23lt5  16831  pcpremul  16860  pcdvdsb  16886  pcelnn  16887  pcidlem  16889  pcid  16890  pcdvdstr  16893  pcgcd1  16894  pcprmpw2  16899  dvdsprmpweqnn  16902  dvdsprmpweqle  16903  pcaddlem  16905  pcadd  16906  pcmptcl  16908  pcmpt  16909  pcmpt2  16910  pcfaclem  16915  pcfac  16916  pcbc  16917  expnprm  16919  oddprmdvds  16920  prmpwdvds  16921  pockthlem  16922  pockthg  16923  pockthi  16924  prmreclem4  16936  prmreclem5  16937  prmreclem6  16938  prmrec  16939  1arith  16944  4sqlem11  16972  4sqlem12  16973  4sqlem13  16974  4sqlem14  16975  4sqlem17  16978  4sqlem18  16979  4sqlem19  16980  prmdvdsprmo  17059  prmgaplem3  17070  prmgaplem4  17071  prmgaplem5  17072  prmgaplem6  17073  prmgaplem8  17075  cshwshashnsame  17120  cshwshash  17121  prmlem1a  17123  pgpfi1  19616  pgp0  19617  sylow1lem1  19619  sylow1lem3  19621  sylow1lem4  19622  sylow1lem5  19623  odcau  19625  pgpfi  19626  fislw  19646  sylow3lem6  19653  gexexlem  19873  prmcyg  19915  ablfac1lem  20091  ablfac1b  20093  ablfac1eu  20096  pgpfac1lem3a  20099  pgpfac1lem3  20100  ablfaclem3  20110  prmgrpsimpgd  20137  prmirredlem  21502  dfprm2  21503  prmirred  21504  fermltlchr  21559  znfld  21590  freshmansdream  21604  frobrhm  21605  ply1fermltlchr  22353  rtprmirr  26800  wilthlem1  27107  wilthlem2  27108  wilthlem3  27109  chtf  27147  efchtcl  27150  isppw2  27154  vmappw  27155  vmaprm  27156  vmacl  27157  efvmacl  27159  muval1  27172  chtprm  27192  chtdif  27197  efchtdvds  27198  dvdsppwf1o  27225  sgmppw  27236  0sgmppw  27237  1sgmprm  27238  vmalelog  27244  chtleppi  27249  chtublem  27250  fsumvma2  27253  vmasum  27255  chpchtsum  27258  chpub  27259  mersenne  27266  perfect1  27267  perfect  27270  pcbcctr  27315  bpos1lem  27321  bposlem1  27323  bposlem2  27324  bposlem6  27328  lgslem1  27336  lgsval2lem  27346  lgsvalmod  27355  lgsmod  27362  lgsdirprm  27370  lgsne0  27374  lgsprme0  27378  lgsqrlem1  27385  lgsqrlem2  27386  lgsqrlem4  27388  lgsqr  27390  lgsqrmod  27391  lgsqrmodndvds  27392  gausslemma2dlem0c  27397  gausslemma2dlem0i  27403  gausslemma2dlem1a  27404  gausslemma2dlem5a  27409  gausslemma2dlem7  27412  gausslemma2d  27413  lgseisenlem1  27414  lgseisenlem2  27415  lgseisenlem3  27416  lgseisenlem4  27417  lgsquadlem1  27419  lgsquadlem3  27421  lgsquad2lem2  27424  lgsquad2  27425  m1lgs  27427  2lgslem1a  27430  2lgslem1c  27432  2lgs  27446  2sqlem3  27459  2sqlem8  27465  2sqlem11  27468  2sqblem  27470  2sqmod  27475  chtppilimlem1  27512  rplogsumlem2  27524  rpvmasumlem  27526  dchrisum0flblem1  27547  dchrisum0flblem2  27548  padicabvf  27670  ostth1  27672  ostth3  27677  hashecclwwlkn1  30223  umgrhashecclwwlk  30224  fusgrhashclwwlkn  30225  clwlksndivn  30232  numclwwlk5  30534  numclwwlk6  30536  numclwwlk7  30537  numclwwlk8  30538  znfermltl  33511  ply1fermltl  33741  cos9thpiminplylem2  34039  nn0prpwlem  36635  nn0prpw  36636  aks4d1p6  42651  aks4d1p8d1  42654  aks4d1p8d2  42655  aks4d1p8d3  42656  aks4d1p8  42657  aks6d1c1p2  42679  aks6d1c1p3  42680  aks6d1c1  42686  aks6d1c2p1  42688  aks6d1c2p2  42689  aks6d1c3  42693  aks6d1c4  42694  aks6d1c2lem4  42697  aks6d1c5lem1  42706  aks6d1c6lem3  42742  aks6d1c6lem4  42743  aks6d1c7lem1  42750  aks6d1c7  42754  aks5lem1  42756  aks5lem2  42757  aks5lem3a  42759  aks5lem8  42771  aks5  42774  nzprmdif  44848  etransclem41  46802  etransclem44  46805  etransclem47  46808  etransclem48  46809  odz2prm2pw  48125  fmtnoprmfac1lem  48126  fmtnoprmfac1  48127  fmtnoprmfac2  48129  prmdvdsfmtnof1lem2  48147  2pwp1prm  48151  sfprmdvdsmersenne  48165  lighneallem2  48168  lighneallem3  48169  lighneallem4  48172  lighneal  48173  perfectALTV  48298  gbepos  48333  gbowpos  48334  sbgoldbaltlem1  48354  ztprmneprm  48922