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

Theorem prmnn 15609
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 15608 . 2 (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑧 ∈ ℕ ∣ 𝑧𝑃} ≈ 2𝑜))
21simplbi 487 1 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  {crab 3107   class class class wbr 4851  2𝑜c2o 7793  cen 8192  cn 11308  cdvds 15206  cprime 15606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rab 3112  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-br 4852  df-prm 15607
This theorem is referenced by:  prmz  15610  prmssnn  15611  nprmdvds1  15638  isprm5  15639  coprm  15643  prmdvdsexpr  15649  prmndvdsfaclt  15655  cncongrprm  15657  phiprmpw  15701  fermltl  15709  prmdiv  15710  prmdiveq  15711  prmdivdiv  15712  modprm1div  15722  m1dvdsndvds  15723  vfermltl  15726  vfermltlALT  15727  powm2modprm  15728  reumodprminv  15729  modprm0  15730  nnnn0modprm0  15731  modprmn0modprm0  15732  oddprm  15735  nnoddn2prm  15736  prm23lt5  15739  pcpremul  15768  pcdvdsb  15793  pcelnn  15794  pcidlem  15796  pcid  15797  pcdvdstr  15800  pcgcd1  15801  pcprmpw2  15806  dvdsprmpweqnn  15809  dvdsprmpweqle  15810  pcaddlem  15812  pcadd  15813  pcmptcl  15815  pcmpt  15816  pcmpt2  15817  pcfaclem  15822  pcfac  15823  pcbc  15824  expnprm  15826  oddprmdvds  15827  prmpwdvds  15828  pockthlem  15829  pockthg  15830  pockthi  15831  prminf  15839  prmreclem4  15843  prmreclem5  15844  prmreclem6  15845  prmrec  15846  1arith  15851  4sqlem11  15879  4sqlem12  15880  4sqlem13  15881  4sqlem14  15882  4sqlem17  15885  4sqlem18  15886  4sqlem19  15887  prmdvdsprmo  15966  prmgaplem3  15977  prmgaplem4  15978  prmgaplem5  15979  prmgaplem6  15980  prmgaplem8  15982  cshwshashnsame  16025  cshwshash  16026  prmlem1a  16028  pgpfi1  18214  pgp0  18215  sylow1lem1  18217  sylow1lem3  18219  sylow1lem4  18220  sylow1lem5  18221  odcau  18223  pgpfi  18224  fislw  18244  sylow3lem6  18251  gexexlem  18459  prmcyg  18499  ablfac1lem  18672  ablfac1b  18674  ablfac1eu  18677  pgpfac1lem3a  18680  pgpfac1lem3  18681  ablfaclem3  18691  prmirredlem  20052  dfprm2  20053  prmirred  20054  znfld  20119  wilthlem1  25014  wilthlem2  25015  wilthlem3  25016  prmdvdsfi  25053  chtf  25054  efchtcl  25057  vmaval  25059  isppw2  25061  vmappw  25062  vmaprm  25063  vmacl  25064  efvmacl  25066  muval1  25079  chtprm  25099  chtdif  25104  efchtdvds  25105  mumul  25127  sqff1o  25128  dvdsppwf1o  25132  sgmppw  25142  0sgmppw  25143  1sgmprm  25144  vmalelog  25150  chtleppi  25155  chtublem  25156  fsumvma2  25159  vmasum  25161  chpchtsum  25164  chpub  25165  mersenne  25172  perfect1  25173  perfect  25176  pcbcctr  25221  bpos1lem  25227  bposlem1  25229  bposlem2  25230  bposlem6  25234  lgslem1  25242  lgsval2lem  25252  lgsvalmod  25261  lgsmod  25268  lgsdirprm  25276  lgsne0  25280  lgsprme0  25284  lgsqrlem1  25291  lgsqrlem2  25292  lgsqrlem4  25294  lgsqr  25296  lgsqrmod  25297  lgsqrmodndvds  25298  gausslemma2dlem0c  25303  gausslemma2dlem0i  25309  gausslemma2dlem1a  25310  gausslemma2dlem5a  25315  gausslemma2dlem7  25318  gausslemma2d  25319  lgseisenlem1  25320  lgseisenlem2  25321  lgseisenlem3  25322  lgseisenlem4  25323  lgseisen  25324  lgsquadlem1  25325  lgsquadlem2  25326  lgsquadlem3  25327  lgsquad2lem2  25330  lgsquad2  25331  m1lgs  25333  2lgslem1a  25336  2lgslem1c  25338  2lgs  25352  2sqlem3  25365  2sqlem8  25371  2sqlem11  25374  2sqblem  25376  chtppilimlem1  25382  rplogsumlem2  25394  rpvmasumlem  25396  dchrisum0flblem1  25417  dchrisum0flblem2  25418  dirith2  25437  padicabvf  25540  ostth1  25542  ostth3  25547  hashecclwwlkn1  27234  umgrhashecclwwlk  27235  fusgrhashclwwlkn  27236  clwlksfclwwlkOLD  27242  clwlksfoclwwlkOLD  27243  clwlksf1clwwlkOLD  27249  clwlksndivn  27257  numclwwlk5  27582  numclwwlk6  27584  numclwwlk7  27585  numclwwlk8  27586  2sqmod  29979  nn0prpwlem  32643  nn0prpw  32644  nzprmdif  39019  etransclem41  40972  etransclem44  40975  etransclem47  40978  etransclem48  40979  odz2prm2pw  42051  fmtnoprmfac1lem  42052  fmtnoprmfac1  42053  fmtnoprmfac2  42055  prmdvdsfmtnof1lem2  42073  2pwp1prm  42079  sfprmdvdsmersenne  42096  lighneallem2  42099  lighneallem3  42100  lighneallem4  42103  lighneal  42104  perfectALTV  42208  gbepos  42222  gbowpos  42223  sbgoldbaltlem1  42243  ztprmneprm  42694
  Copyright terms: Public domain W3C validator