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

Theorem nnnn0d 11198
Description: A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnnn0d.1 (𝜑𝐴 ∈ ℕ)
Assertion
Ref Expression
nnnn0d (𝜑𝐴 ∈ ℕ0)

Proof of Theorem nnnn0d
StepHypRef Expression
1 nnssnn0 11142 . 2 ℕ ⊆ ℕ0
2 nnnn0d.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3565 1 (𝜑𝐴 ∈ ℕ0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cn 10867  0cn0 11139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-in 3546  df-ss 3553  df-n0 11140
This theorem is referenced by:  nn0ge2m1nn0  11208  nnzd  11313  eluzge2nn0  11559  expgt1  12715  expaddzlem  12720  expaddz  12721  expmulz  12723  expmulnbnd  12813  facwordi  12893  faclbnd  12894  facavg  12905  bcm1k  12919  wrdeqs1cat  13272  cshwcsh2id  13371  relexpsucnnr  13559  isercolllem2  14190  bcxmas  14352  climcndslem1  14366  climcndslem2  14367  climcnds  14368  geo2sum  14389  mertenslem1  14401  prodmolem3  14448  prodmolem2a  14449  bpolydiflem  14570  eftabs  14591  efcllem  14593  eftlub  14624  eirrlem  14717  rpnnen2lem9  14736  rpnnen2lem11  14738  dvdsfac  14832  oddpwp1fsum  14899  bitsfzo  14941  bitsfi  14943  sadcaddlem  14963  smumullem  14998  gcdcl  15012  mulgcd  15049  rplpwr  15060  rppwr  15061  lcmcl  15098  lcmgcdnn  15108  lcmfcl  15125  nprmdvds1  15202  rpexp  15216  zsqrtelqelz  15250  phiprmpw  15265  eulerthlem2  15271  eulerth  15272  fermltl  15273  odzcllem  15281  odzdvds  15284  odzphi  15285  prm23lt5  15303  pythagtriplem6  15310  pythagtriplem7  15311  pcprmpw2  15370  dvdsprmpweqle  15374  pcprod  15383  pcfac  15387  pcbc  15388  expnprm  15390  pockthlem  15393  pockthg  15394  prmunb  15402  prmreclem2  15405  prmreclem3  15406  prmreclem4  15407  prmreclem5  15408  prmreclem6  15409  mul4sqlem  15441  4sqlem11  15443  4sqlem17  15449  vdwlem1  15469  vdwlem5  15473  vdwlem6  15474  vdwlem8  15476  vdwlem9  15477  vdwlem11  15479  vdwlem12  15480  vdwnnlem3  15485  ramz2  15512  ramub1lem1  15514  ramub1lem2  15515  ramub1  15516  prmgaplem3  15541  2expltfac  15583  psgnunilem3  17685  mndodconglem  17729  gexcl3  17771  pgpfi1  17779  sylow1lem1  17782  gexexlem  18024  prmcyg  18064  gsumval3  18077  ablfacrplem  18233  ablfacrp  18234  ablfacrp2  18235  ablfac1eu  18241  srgbinomlem3  18311  srgbinomlem4  18312  chfacfscmulgsum  20426  chfacfpmmulgsum  20430  cpmadugsumlemF  20442  ovoliunlem1  22994  mbfi1fseqlem1  23205  mbfi1fseqlem3  23207  mbfi1fseqlem5  23209  itg2cnlem2  23252  dvply1  23760  aalioulem2  23809  aalioulem5  23812  aaliou3lem1  23818  aaliou3lem2  23819  aaliou3lem8  23821  aaliou3lem6  23824  taylthlem1  23848  taylthlem2  23849  pserdvlem2  23903  cxpeq  24215  dmgmdivn0  24471  lgamgulmlem5  24476  lgamcvg2  24498  wilthlem1  24511  ftalem1  24516  ftalem2  24517  ftalem4  24519  ftalem5  24520  basellem2  24525  basellem3  24526  basellem4  24527  basellem5  24528  isppw2  24558  dvdsmulf1o  24637  sgmmul  24643  chpchtsum  24661  logfacubnd  24663  mersenne  24669  perfect1  24670  perfectlem1  24671  perfectlem2  24672  perfect  24673  dchrelbas3  24680  dchrelbasd  24681  dchrzrh1  24686  dchrzrhmul  24688  dchrmulcl  24691  dchrn0  24692  dchrfi  24697  dchrghm  24698  dchrabs  24702  dchrinv  24703  dchrptlem1  24706  dchrptlem2  24707  dchrptlem3  24708  dchrpt  24709  dchrsum2  24710  sum2dchr  24716  pcbcctr  24718  bcmono  24719  bclbnd  24722  bposlem1  24726  bposlem3  24728  bposlem5  24730  bposlem6  24731  lgslem1  24739  lgslem4  24742  lgsval2lem  24749  lgsvalmod  24758  lgsmod  24765  lgsdirprm  24773  lgsne0  24777  lgsqrlem1  24788  lgsqrlem2  24789  lgsqrlem3  24790  lgsqrlem4  24791  gausslemma2dlem0b  24799  gausslemma2dlem0c  24800  gausslemma2dlem1  24808  gausslemma2dlem7  24815  gausslemma2d  24816  lgseisenlem1  24817  lgseisenlem2  24818  lgseisenlem3  24819  lgseisenlem4  24820  lgseisen  24821  lgsquadlem2  24823  lgsquadlem3  24824  m1lgs  24830  2lgslem1a  24833  2sqlem3  24862  2sqblem  24873  chebbnd1lem1  24875  chebbnd1lem3  24877  rplogsumlem2  24891  rpvmasumlem  24893  dchrisumlem1  24895  dchrisumlem2  24896  dchrmusum2  24900  dchrvmasumlem3  24905  dchrisum0ff  24913  dchrisum0flblem1  24914  rpvmasum2  24918  dchrisum0re  24919  dchrisum0lem2a  24923  dirith  24935  mudivsum  24936  pntpbnd1a  24991  pntlemq  25007  pntlemr  25008  pntlemj  25009  ostth2lem2  25040  ostth2lem3  25041  ostth2  25043  hashecclwwlkn1  26127  usghashecclwwlk  26128  hashclwwlkn  26129  clwwlkndivn  26130  clwlkfclwwlk  26137  numclwwlk3  26402  numclwwlk6  26406  numclwwlk7  26407  dipcl  26755  dipcn  26763  sspival  26781  bcm1n  28747  isarchi2  28876  submarchi  28877  psgnfzto1st  28992  submateqlem1  29007  madjusmdetlem2  29028  madjusmdetlem4  29030  mdetlap  29032  nexple  29205  oddpwdc  29549  eulerpartlemsv2  29553  eulerpartlemsf  29554  eulerpartlems  29555  eulerpartlemv  29559  eulerpartlemb  29563  plymulx0  29756  signsvtn0  29779  subfacp1lem1  30221  subfacp1lem6  30227  subfaclim  30230  erdszelem8  30240  erdszelem10  30242  cvmliftlem10  30336  faclim2  30693  poimirlem7  32382  poimirlem17  32392  poimirlem18  32393  poimirlem20  32395  poimirlem21  32396  poimirlem22  32397  poimirlem25  32400  poimirlem26  32401  poimirlem27  32402  poimirlem28  32403  poimirlem32  32407  nninfnub  32513  bfplem1  32587  3rexfrabdioph  36175  4rexfrabdioph  36176  6rexfrabdioph  36177  7rexfrabdioph  36178  irrapxlem5  36204  pellexlem2  36208  pellexlem6  36212  pell14qrgt0  36237  pell1qrge1  36248  pellfundgt1  36261  ltrmxnn0  36330  jm2.26lem3  36382  jm2.27a  36386  jm2.27c  36388  rmxdiophlem  36396  jm3.1lem1  36398  jm3.1lem2  36399  jm3.1lem3  36400  jm3.1  36401  dgrsub2  36520  mpaaeu  36535  idomsubgmo  36591  relexpxpmin  36824  nzprmdif  37336  binomcxplemwb  37365  fperiodmul  38255  xralrple4  38327  fsumnncl  38435  dvsinexp  38595  dvxpaek  38627  itgsinexplem1  38642  stoweidlem1  38691  stoweidlem17  38707  stoweidlem25  38715  stoweidlem34  38724  stoweidlem38  38728  stoweidlem40  38730  stoweidlem42  38732  stoweidlem45  38735  stirlinglem4  38767  stirlinglem5  38768  stirlinglem10  38773  stirlinglem13  38776  dirkertrigeq  38791  fourierdlem21  38818  fourierdlem25  38822  fourierdlem48  38844  fourierdlem54  38850  fourierdlem64  38860  fourierdlem65  38861  fourierdlem73  38869  fourierdlem81  38877  fourierdlem83  38879  fourierdlem92  38888  fourierdlem103  38899  fourierdlem104  38900  fourierdlem112  38908  fourierdlem113  38909  etransclem1  38925  etransclem4  38928  etransclem8  38932  etransclem15  38939  etransclem17  38941  etransclem18  38942  etransclem19  38943  etransclem20  38944  etransclem21  38945  etransclem22  38946  etransclem23  38947  etransclem24  38948  etransclem25  38949  etransclem27  38951  etransclem32  38956  etransclem35  38959  etransclem41  38965  etransclem44  38968  etransclem46  38970  iccpartigtl  39759  iccpartgt  39763  iccpartgel  39765  iccelpart  39769  odz2prm2pw  39811  fmtnoprmfac1  39813  fmtnoprmfac2  39815  pwdif  39837  2pwp1prm  39839  sfprmdvdsmersenne  39856  lighneallem4a  39861  proththdlem  39866  proththd  39867  perfectALTVlem1  39962  perfectALTVlem2  39963  perfectALTV  39964  crctcsh1wlkn0lem6  41013  hashecclwwlksn1  41256  umgrhashecclwwlk  41257  clwlksfclwwlk  41264  eucrctshift  41406  logbpw2m1  42154  nnpw2blenfzo  42168  nnolog2flm1  42177  dignn0fr  42188  nn0sumshdiglemA  42206  nn0sumshdiglemB  42207
  Copyright terms: Public domain W3C validator