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

Theorem prmnn 15226
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 15225 . 2 (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧𝑃} ≈ 2𝑜))
21simplbi 475 1 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  {crab 2900   class class class wbr 4583  2𝑜c2o 7441  cen 7838  cn 10897  cdvds 14821  cprime 15223
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-prm 15224
This theorem is referenced by:  prmz  15227  prmssnn  15228  nprmdvds1  15256  isprm5  15257  coprm  15261  prmdvdsexpr  15267  prmndvdsfaclt  15273  cncongrprm  15275  phiprmpw  15319  fermltl  15327  prmdiv  15328  prmdiveq  15329  prmdivdiv  15330  modprm1div  15340  m1dvdsndvds  15341  vfermltl  15344  vfermltlALT  15345  powm2modprm  15346  reumodprminv  15347  modprm0  15348  nnnn0modprm0  15349  modprmn0modprm0  15350  oddprm  15353  nnoddn2prm  15354  prm23lt5  15357  pcpremul  15386  pcdvdsb  15411  pcelnn  15412  pcidlem  15414  pcid  15415  pcdvdstr  15418  pcgcd1  15419  pcprmpw2  15424  dvdsprmpweqnn  15427  dvdsprmpweqle  15428  pcaddlem  15430  pcadd  15431  pcmptcl  15433  pcmpt  15434  pcmpt2  15435  pcfaclem  15440  pcfac  15441  pcbc  15442  expnprm  15444  oddprmdvds  15445  prmpwdvds  15446  pockthlem  15447  pockthg  15448  pockthi  15449  prminf  15457  prmreclem4  15461  prmreclem5  15462  prmreclem6  15463  prmrec  15464  1arith  15469  4sqlem11  15497  4sqlem12  15498  4sqlem13  15499  4sqlem14  15500  4sqlem17  15503  4sqlem18  15504  4sqlem19  15505  prmdvdsprmo  15584  prmgaplem3  15595  prmgaplem4  15596  prmgaplem5  15597  prmgaplem6  15598  prmgaplem8  15600  cshwshashnsame  15648  cshwshash  15649  prmlem1a  15651  pgpfi1  17833  pgp0  17834  sylow1lem1  17836  sylow1lem3  17838  sylow1lem4  17839  sylow1lem5  17840  odcau  17842  pgpfi  17843  fislw  17863  sylow3lem6  17870  gexexlem  18078  prmcyg  18118  ablfac1lem  18290  ablfac1b  18292  ablfac1eu  18295  pgpfac1lem3a  18298  pgpfac1lem3  18299  ablfaclem3  18309  prmirredlem  19660  dfprm2  19661  prmirred  19662  znfld  19728  wilthlem1  24594  wilthlem2  24595  wilthlem3  24596  prmdvdsfi  24633  chtf  24634  efchtcl  24637  vmaval  24639  isppw2  24641  vmappw  24642  vmaprm  24643  vmacl  24644  efvmacl  24646  muval1  24659  chtprm  24679  chtdif  24684  efchtdvds  24685  mumul  24707  sqff1o  24708  dvdsppwf1o  24712  sgmppw  24722  0sgmppw  24723  1sgmprm  24724  vmalelog  24730  chtleppi  24735  chtublem  24736  fsumvma2  24739  vmasum  24741  chpchtsum  24744  chpub  24745  mersenne  24752  perfect1  24753  perfect  24756  pcbcctr  24801  bpos1lem  24807  bposlem1  24809  bposlem2  24810  bposlem6  24814  lgslem1  24822  lgsval2lem  24832  lgsvalmod  24841  lgsmod  24848  lgsdirprm  24856  lgsne0  24860  lgsprme0  24864  lgsqrlem1  24871  lgsqrlem2  24872  lgsqrlem4  24874  lgsqr  24876  lgsqrmod  24877  lgsqrmodndvds  24878  gausslemma2dlem0c  24883  gausslemma2dlem0i  24889  gausslemma2dlem1a  24890  gausslemma2dlem5a  24895  gausslemma2dlem7  24898  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgseisenlem4  24903  lgseisen  24904  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  lgsquad2lem2  24910  lgsquad2  24911  m1lgs  24913  2lgslem1a  24916  2lgslem1c  24918  2lgs  24932  2sqlem3  24945  2sqlem8  24951  2sqlem11  24954  2sqblem  24956  chtppilimlem1  24962  rplogsumlem2  24974  rpvmasumlem  24976  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dirith2  25017  padicabvf  25120  ostth1  25122  ostth3  25127  hashecclwwlkn1  26361  usghashecclwwlk  26362  hashclwwlkn  26363  clwwlkndivn  26364  clwlkfclwwlk  26371  clwlkfoclwwlk  26372  clwlkf1clwwlk  26377  numclwwlk5  26639  numclwwlk6  26640  numclwwlk7  26641  numclwwlk8  26642  2sqmod  28979  nn0prpwlem  31487  nn0prpw  31488  nzprmdif  37540  etransclem41  39168  etransclem44  39171  etransclem47  39174  etransclem48  39175  odz2prm2pw  40013  fmtnoprmfac1lem  40014  fmtnoprmfac1  40015  fmtnoprmfac2  40017  prmdvdsfmtnof1lem2  40035  2pwp1prm  40041  sfprmdvdsmersenne  40058  lighneallem2  40061  lighneallem3  40062  lighneallem4  40065  lighneal  40066  perfectALTV  40166  gbepos  40180  gbopos  40181  sgoldbaltlem1  40201  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  fusgrhashclwwlkn  41263  clwlksfclwwlk  41269  clwlksfoclwwlk  41270  clwlksf1clwwlk  41276  av-numclwwlk5  41542  av-numclwwlk6  41544  av-numclwwlk7  41545  av-numclwwlk8  41546  ztprmneprm  41918
  Copyright terms: Public domain W3C validator