Theorem prmnn 16731

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

Syntax hints:   → wi 4   ∈ wcel 2149  {crab 3423   class class class wbr 5113  2_oc2o 8446   ≈ cen 8939  ℕcn 12232   ∥ cdvds 16309  ℙcprime 16728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-prm 16729

This theorem is referenced by:  prmz  16732  prmssnn  16733  0nprm  16735  2mulprm  16750  nprmdvds1  16764  isprm5  16765  coprm  16769  prmdvdsexpr  16775  prmndvdsfaclt  16783  prmdvdsbc  16784  prmdvdsncoprmbd  16785  cncongrprm  16787  phiprmpw  16834  fermltl  16842  prmdiv  16843  prmdiveq  16844  prmdivdiv  16845  m1dvdsndvds  16857  vfermltl  16860  vfermltlALT  16861  powm2modprm  16862  reumodprminv  16863  modprm0  16864  nnnn0modprm0  16865  modprmn0modprm0  16866  oddprm  16869  nnoddn2prm  16870  prm23lt5  16873  pcpremul  16902  pcdvdsb  16928  pcelnn  16929  pcidlem  16931  pcid  16932  pcdvdstr  16935  pcgcd1  16936  pcprmpw2  16941  dvdsprmpweqnn  16944  dvdsprmpweqle  16945  pcaddlem  16947  pcadd  16948  pcmptcl  16950  pcmpt  16951  pcmpt2  16952  pcfaclem  16957  pcfac  16958  pcbc  16959  expnprm  16961  oddprmdvds  16962  prmpwdvds  16963  pockthlem  16964  pockthg  16965  pockthi  16966  prmreclem4  16978  prmreclem5  16979  prmreclem6  16980  prmrec  16981  1arith  16986  4sqlem11  17014  4sqlem12  17015  4sqlem13  17016  4sqlem14  17017  4sqlem17  17020  4sqlem18  17021  4sqlem19  17022  prmdvdsprmo  17101  prmgaplem3  17112  prmgaplem4  17113  prmgaplem5  17114  prmgaplem6  17115  prmgaplem8  17117  cshwshashnsame  17162  cshwshash  17163  prmlem1a  17165  pgpfi1  19664  pgp0  19665  sylow1lem1  19667  sylow1lem3  19669  sylow1lem4  19670  sylow1lem5  19671  odcau  19673  pgpfi  19674  fislw  19694  sylow3lem6  19701  gexexlem  19921  prmcyg  19963  ablfac1lem  20139  ablfac1b  20141  ablfac1eu  20144  pgpfac1lem3a  20147  pgpfac1lem3  20148  ablfaclem3  20158  prmgrpsimpgd  20185  prmirredlem  21590  dfprm2  21591  prmirred  21592  fermltlchr  21647  znfld  21678  freshmansdream  21692  frobrhm  21693  ply1fermltlchr  22440  rtprmirr  26890  wilthlem1  27197  wilthlem2  27198  wilthlem3  27199  chtf  27237  efchtcl  27240  isppw2  27244  vmappw  27245  vmaprm  27246  vmacl  27247  efvmacl  27249  muval1  27262  chtprm  27282  chtdif  27287  efchtdvds  27288  dvdsppwf1o  27315  sgmppw  27326  0sgmppw  27327  1sgmprm  27328  vmalelog  27334  chtleppi  27339  chtublem  27340  fsumvma2  27343  vmasum  27345  chpchtsum  27348  chpub  27349  mersenne  27356  perfect1  27357  perfect  27360  pcbcctr  27405  bpos1lem  27411  bposlem1  27413  bposlem2  27414  bposlem6  27418  lgslem1  27426  lgsval2lem  27436  lgsvalmod  27445  lgsmod  27452  lgsdirprm  27460  lgsne0  27464  lgsprme0  27468  lgsqrlem1  27475  lgsqrlem2  27476  lgsqrlem4  27478  lgsqr  27480  lgsqrmod  27481  lgsqrmodndvds  27482  gausslemma2dlem0c  27487  gausslemma2dlem0i  27493  gausslemma2dlem1a  27494  gausslemma2dlem5a  27499  gausslemma2dlem7  27502  gausslemma2d  27503  lgseisenlem1  27504  lgseisenlem2  27505  lgseisenlem3  27506  lgseisenlem4  27507  lgsquadlem1  27509  lgsquadlem3  27511  lgsquad2lem2  27514  lgsquad2  27515  m1lgs  27517  2lgslem1a  27520  2lgslem1c  27522  2lgs  27536  2sqlem3  27549  2sqlem8  27555  2sqlem11  27558  2sqblem  27560  2sqmod  27565  chtppilimlem1  27602  rplogsumlem2  27614  rpvmasumlem  27616  dchrisum0flblem1  27637  dchrisum0flblem2  27638  padicabvf  27760  ostth1  27762  ostth3  27767  hashecclwwlkn1  30368  umgrhashecclwwlk  30369  fusgrhashclwwlkn  30370  clwlksndivn  30377  numclwwlk5  30679  numclwwlk6  30681  numclwwlk7  30682  numclwwlk8  30683  znfermltl  33623  ply1fermltl  33820  cos9thpiminplylem2  34117  nn0prpwlem  36721  nn0prpw  36722  aks4d1p6  42737  aks4d1p8d1  42740  aks4d1p8d2  42741  aks4d1p8d3  42742  aks4d1p8  42743  aks6d1c1p2  42765  aks6d1c1p3  42766  aks6d1c1  42772  aks6d1c2p1  42774  aks6d1c2p2  42775  aks6d1c3  42779  aks6d1c4  42780  aks6d1c2lem4  42783  aks6d1c5lem1  42792  aks6d1c6lem3  42828  aks6d1c6lem4  42829  aks6d1c7lem1  42836  aks6d1c7  42840  aks5lem1  42842  aks5lem2  42843  aks5lem3a  42845  aks5lem8  42857  aks5  42860  nzprmdif  44920  etransclem41  46880  etransclem44  46883  etransclem47  46886  etransclem48  46887  odz2prm2pw  48203  fmtnoprmfac1lem  48204  fmtnoprmfac1  48205  fmtnoprmfac2  48207  prmdvdsfmtnof1lem2  48225  2pwp1prm  48229  sfprmdvdsmersenne  48243  lighneallem2  48246  lighneallem3  48247  lighneallem4  48250  lighneal  48251  perfectALTV  48376  gbepos  48411  gbowpos  48412  sbgoldbaltlem1  48432  ztprmneprm  49011