MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmnn Structured version   Visualization version   GIF version

Theorem prmnn 16017
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.
StepHypRef Expression
1 isprm 16016 . 2 (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧𝑃} ≈ 2o))
21simplbi 500 1 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  {crab 3142   class class class wbr 5065  2oc2o 8095  cen 8505  cn 11637  cdvds 15606  cprime 16014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-br 5066  df-prm 16015
This theorem is referenced by:  prmz  16018  prmssnn  16019  0nprm  16021  2mulprm  16036  nprmdvds1  16049  isprm5  16050  coprm  16054  prmdvdsexpr  16060  prmndvdsfaclt  16066  cncongrprm  16068  phiprmpw  16112  fermltl  16120  prmdiv  16121  prmdiveq  16122  prmdivdiv  16123  m1dvdsndvds  16134  vfermltl  16137  vfermltlALT  16138  powm2modprm  16139  reumodprminv  16140  modprm0  16141  nnnn0modprm0  16142  modprmn0modprm0  16143  oddprm  16146  nnoddn2prm  16147  prm23lt5  16150  pcpremul  16179  pcdvdsb  16204  pcelnn  16205  pcidlem  16207  pcid  16208  pcdvdstr  16211  pcgcd1  16212  pcprmpw2  16217  dvdsprmpweqnn  16220  dvdsprmpweqle  16221  pcaddlem  16223  pcadd  16224  pcmptcl  16226  pcmpt  16227  pcmpt2  16228  pcfaclem  16233  pcfac  16234  pcbc  16235  expnprm  16237  oddprmdvds  16238  prmpwdvds  16239  pockthlem  16240  pockthg  16241  pockthi  16242  prmreclem4  16254  prmreclem5  16255  prmreclem6  16256  prmrec  16257  1arith  16262  4sqlem11  16290  4sqlem12  16291  4sqlem13  16292  4sqlem14  16293  4sqlem17  16296  4sqlem18  16297  4sqlem19  16298  prmdvdsprmo  16377  prmgaplem3  16388  prmgaplem4  16389  prmgaplem5  16390  prmgaplem6  16391  prmgaplem8  16393  cshwshashnsame  16436  cshwshash  16437  prmlem1a  16439  pgpfi1  18719  pgp0  18720  sylow1lem1  18722  sylow1lem3  18724  sylow1lem4  18725  sylow1lem5  18726  odcau  18728  pgpfi  18729  fislw  18749  sylow3lem6  18756  gexexlem  18971  prmcyg  19013  ablfac1lem  19189  ablfac1b  19191  ablfac1eu  19194  pgpfac1lem3a  19197  pgpfac1lem3  19198  ablfaclem3  19208  prmgrpsimpgd  19235  prmirredlem  20639  dfprm2  20640  prmirred  20641  znfld  20706  wilthlem1  25644  wilthlem2  25645  wilthlem3  25646  chtf  25684  efchtcl  25687  isppw2  25691  vmappw  25692  vmaprm  25693  vmacl  25694  efvmacl  25696  muval1  25709  chtprm  25729  chtdif  25734  efchtdvds  25735  dvdsppwf1o  25762  sgmppw  25772  0sgmppw  25773  1sgmprm  25774  vmalelog  25780  chtleppi  25785  chtublem  25786  fsumvma2  25789  vmasum  25791  chpchtsum  25794  chpub  25795  mersenne  25802  perfect1  25803  perfect  25806  pcbcctr  25851  bpos1lem  25857  bposlem1  25859  bposlem2  25860  bposlem6  25864  lgslem1  25872  lgsval2lem  25882  lgsvalmod  25891  lgsmod  25898  lgsdirprm  25906  lgsne0  25910  lgsprme0  25914  lgsqrlem1  25921  lgsqrlem2  25922  lgsqrlem4  25924  lgsqr  25926  lgsqrmod  25927  lgsqrmodndvds  25928  gausslemma2dlem0c  25933  gausslemma2dlem0i  25939  gausslemma2dlem1a  25940  gausslemma2dlem5a  25945  gausslemma2dlem7  25948  gausslemma2d  25949  lgseisenlem1  25950  lgseisenlem2  25951  lgseisenlem3  25952  lgseisenlem4  25953  lgsquadlem1  25955  lgsquadlem3  25957  lgsquad2lem2  25960  lgsquad2  25961  m1lgs  25963  2lgslem1a  25966  2lgslem1c  25968  2lgs  25982  2sqlem3  25995  2sqlem8  26001  2sqlem11  26004  2sqblem  26006  2sqmod  26011  chtppilimlem1  26048  rplogsumlem2  26060  rpvmasumlem  26062  dchrisum0flblem1  26083  dchrisum0flblem2  26084  padicabvf  26206  ostth1  26208  ostth3  26213  hashecclwwlkn1  27855  umgrhashecclwwlk  27856  fusgrhashclwwlkn  27857  clwlksndivn  27864  numclwwlk5  28166  numclwwlk6  28168  numclwwlk7  28169  numclwwlk8  28170  prmdvdsbc  30531  freshmansdream  30859  nn0prpwlem  33670  nn0prpw  33671  rtprmirr  39192  nzprmdif  40649  etransclem41  42559  etransclem44  42562  etransclem47  42565  etransclem48  42566  odz2prm2pw  43724  fmtnoprmfac1lem  43725  fmtnoprmfac1  43726  fmtnoprmfac2  43728  prmdvdsfmtnof1lem2  43746  2pwp1prm  43750  sfprmdvdsmersenne  43767  lighneallem2  43770  lighneallem3  43771  lighneallem4  43774  lighneal  43775  perfectALTV  43887  gbepos  43922  gbowpos  43923  sbgoldbaltlem1  43943  ztprmneprm  44394
  Copyright terms: Public domain W3C validator