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

Theorem prmnn 15323
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 15322 . 2 (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧𝑃} ≈ 2𝑜))
21simplbi 476 1 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  {crab 2911   class class class wbr 4618  2𝑜c2o 7506  cen 7904  cn 10972  cdvds 14918  cprime 15320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-br 4619  df-prm 15321
This theorem is referenced by:  prmz  15324  prmssnn  15325  nprmdvds1  15353  isprm5  15354  coprm  15358  prmdvdsexpr  15364  prmndvdsfaclt  15370  cncongrprm  15372  phiprmpw  15416  fermltl  15424  prmdiv  15425  prmdiveq  15426  prmdivdiv  15427  modprm1div  15437  m1dvdsndvds  15438  vfermltl  15441  vfermltlALT  15442  powm2modprm  15443  reumodprminv  15444  modprm0  15445  nnnn0modprm0  15446  modprmn0modprm0  15447  oddprm  15450  nnoddn2prm  15451  prm23lt5  15454  pcpremul  15483  pcdvdsb  15508  pcelnn  15509  pcidlem  15511  pcid  15512  pcdvdstr  15515  pcgcd1  15516  pcprmpw2  15521  dvdsprmpweqnn  15524  dvdsprmpweqle  15525  pcaddlem  15527  pcadd  15528  pcmptcl  15530  pcmpt  15531  pcmpt2  15532  pcfaclem  15537  pcfac  15538  pcbc  15539  expnprm  15541  oddprmdvds  15542  prmpwdvds  15543  pockthlem  15544  pockthg  15545  pockthi  15546  prminf  15554  prmreclem4  15558  prmreclem5  15559  prmreclem6  15560  prmrec  15561  1arith  15566  4sqlem11  15594  4sqlem12  15595  4sqlem13  15596  4sqlem14  15597  4sqlem17  15600  4sqlem18  15601  4sqlem19  15602  prmdvdsprmo  15681  prmgaplem3  15692  prmgaplem4  15693  prmgaplem5  15694  prmgaplem6  15695  prmgaplem8  15697  cshwshashnsame  15745  cshwshash  15746  prmlem1a  15748  pgpfi1  17942  pgp0  17943  sylow1lem1  17945  sylow1lem3  17947  sylow1lem4  17948  sylow1lem5  17949  odcau  17951  pgpfi  17952  fislw  17972  sylow3lem6  17979  gexexlem  18187  prmcyg  18227  ablfac1lem  18399  ablfac1b  18401  ablfac1eu  18404  pgpfac1lem3a  18407  pgpfac1lem3  18408  ablfaclem3  18418  prmirredlem  19773  dfprm2  19774  prmirred  19775  znfld  19841  wilthlem1  24711  wilthlem2  24712  wilthlem3  24713  prmdvdsfi  24750  chtf  24751  efchtcl  24754  vmaval  24756  isppw2  24758  vmappw  24759  vmaprm  24760  vmacl  24761  efvmacl  24763  muval1  24776  chtprm  24796  chtdif  24801  efchtdvds  24802  mumul  24824  sqff1o  24825  dvdsppwf1o  24829  sgmppw  24839  0sgmppw  24840  1sgmprm  24841  vmalelog  24847  chtleppi  24852  chtublem  24853  fsumvma2  24856  vmasum  24858  chpchtsum  24861  chpub  24862  mersenne  24869  perfect1  24870  perfect  24873  pcbcctr  24918  bpos1lem  24924  bposlem1  24926  bposlem2  24927  bposlem6  24931  lgslem1  24939  lgsval2lem  24949  lgsvalmod  24958  lgsmod  24965  lgsdirprm  24973  lgsne0  24977  lgsprme0  24981  lgsqrlem1  24988  lgsqrlem2  24989  lgsqrlem4  24991  lgsqr  24993  lgsqrmod  24994  lgsqrmodndvds  24995  gausslemma2dlem0c  25000  gausslemma2dlem0i  25006  gausslemma2dlem1a  25007  gausslemma2dlem5a  25012  gausslemma2dlem7  25015  gausslemma2d  25016  lgseisenlem1  25017  lgseisenlem2  25018  lgseisenlem3  25019  lgseisenlem4  25020  lgseisen  25021  lgsquadlem1  25022  lgsquadlem2  25023  lgsquadlem3  25024  lgsquad2lem2  25027  lgsquad2  25028  m1lgs  25030  2lgslem1a  25033  2lgslem1c  25035  2lgs  25049  2sqlem3  25062  2sqlem8  25068  2sqlem11  25071  2sqblem  25073  chtppilimlem1  25079  rplogsumlem2  25091  rpvmasumlem  25093  dchrisum0flblem1  25114  dchrisum0flblem2  25115  dirith2  25134  padicabvf  25237  ostth1  25239  ostth3  25244  hashecclwwlksn1  26837  umgrhashecclwwlk  26838  fusgrhashclwwlkn  26839  clwlksfclwwlk  26845  clwlksfoclwwlk  26846  clwlksf1clwwlk  26852  numclwwlk5  27117  numclwwlk6  27119  numclwwlk7  27120  numclwwlk8  27121  2sqmod  29457  nn0prpwlem  31994  nn0prpw  31995  nzprmdif  38035  etransclem41  39825  etransclem44  39828  etransclem47  39831  etransclem48  39832  odz2prm2pw  40800  fmtnoprmfac1lem  40801  fmtnoprmfac1  40802  fmtnoprmfac2  40804  prmdvdsfmtnof1lem2  40822  2pwp1prm  40828  sfprmdvdsmersenne  40845  lighneallem2  40848  lighneallem3  40849  lighneallem4  40852  lighneal  40853  perfectALTV  40953  gbepos  40967  gbopos  40968  sgoldbaltlem1  40988  ztprmneprm  41439
  Copyright terms: Public domain W3C validator