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

Theorem 0nn0 11345
Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)
Assertion
Ref Expression
0nn0 0 ∈ ℕ0

Proof of Theorem 0nn0
StepHypRef Expression
1 eqid 2651 . 2 0 = 0
2 elnn0 11332 . . . 4 (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
32biimpri 218 . . 3 ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
43olcs 409 . 2 (0 = 0 → 0 ∈ ℕ0)
51, 4ax-mp 5 1 0 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wo 382   = wceq 1523  wcel 2030  0cc0 9974  cn 11058  0cn0 11330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-mulcl 10036  ax-i2m1 10042
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-sn 4211  df-n0 11331
This theorem is referenced by:  0xnn0  11407  nn0ind-raph  11515  10nn0  11554  declei  11580  numlti  11583  nummul1c  11600  decaddc2OLD  11612  decaddc2  11613  decrmanc  11614  decrmac  11615  decaddm10  11616  decaddi  11617  decaddci  11618  decaddci2  11619  decaddci2OLD  11620  decmul1  11623  decmul1OLD  11624  decmulnc  11629  6p5e11  11638  6p5e11OLD  11639  7p4e11  11643  7p4e11OLD  11644  8p3e11  11650  8p3e11OLD  11651  9p2e11  11657  9p2e11OLD  11658  10p10e20  11666  10p10e20OLD  11667  xnn0n0n1ge2b  12003  0elfz  12475  4fvwrd4  12498  fvinim0ffz  12627  ssnn0fi  12824  fsuppmapnn0fiubex  12832  exple1  12960  sq10  13088  nn0opth2  13099  faclbnd4lem3  13122  bc0k  13138  bcn1  13140  bccl  13149  hasheq0  13192  hashrabrsn  13199  hashbc  13275  fi1uzind  13317  brfi1ind  13319  opfi1ind  13322  iswrdi  13341  s1fv  13427  ccat2s1fst  13461  2swrdeqwrdeq  13499  wrdeqs1cat  13520  splfv2a  13553  repsw0  13570  0csh0  13585  repswcshw  13604  cshw1  13614  s2fv0  13678  s3fv0  13682  s4fv0  13686  ofs1  13755  relexp0g  13806  relexpaddg  13837  rtrclreclem1  13842  fsumnn0cl  14511  binom  14606  bcxmas  14611  isumnn0nn  14618  climcndslem1  14625  geoser  14643  geomulcvg  14651  risefac0  14802  fallfac0  14803  risefac1  14808  fallfac1  14809  binomfallfaclem2  14815  binomfallfac  14816  bpoly0  14825  bpoly2  14832  bpoly3  14833  bpoly4  14834  fsumcube  14835  ef0lem  14853  ege2le3  14864  ef4p  14887  efgt1p2  14888  efgt1p  14889  ruclem11  15013  nthruz  15026  nn0o  15146  ndvdssub  15180  bits0  15197  0bits  15208  sadcf  15222  sadc0  15223  sadcaddlem  15226  sadcadd  15227  sadadd2lem  15228  sadadd2  15229  smupf  15247  smup0  15248  smumullem  15261  gcdcl  15275  nn0seqcvgd  15330  algcvg  15336  eucalg  15347  lcmcl  15361  lcmfval  15381  lcmfcl  15388  pclem  15590  pcfac  15650  vdwap0  15727  vdwap1  15728  vdwlem6  15737  hashbc0  15756  0ram  15771  0ramcl  15774  ramz2  15775  ramz  15776  ramcl  15780  prmo0  15787  dec5dvds2  15816  2exp16  15844  11prm  15869  37prm  15875  43prm  15876  83prm  15877  139prm  15878  163prm  15879  317prm  15880  631prm  15881  1259lem1  15885  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  2503lem1  15891  2503lem2  15892  2503lem3  15893  2503prm  15894  4001lem1  15895  4001lem2  15896  4001lem3  15897  4001lem4  15898  4001prm  15899  odrngstr  16113  imasvalstr  16159  ipostr  17200  gsumws1  17423  psgnunilem2  17961  psgnunilem3  17962  oddvdsnn0  18009  pgp0  18057  sylow1lem1  18059  cyggex2  18344  telgsums  18436  srgbinomlem3  18588  srgbinomlem4  18589  srgbinom  18591  snifpsrbag  19414  fczpsrbag  19415  psrlidm  19451  mvrf1  19473  mplcoe3  19514  mplcoe5  19516  ltbwe  19520  psrbag0  19542  psrbagsn  19543  evlslem1  19563  00ply1bas  19658  ply1plusgfvi  19660  coe1sclmul  19700  coe1sclmul2  19702  coe1scl  19705  ply1sclid  19706  ply1idvr1  19711  cply1coe0bi  19718  cnfldstr  19796  cnfldfun  19806  nn0subm  19849  expmhm  19863  nn0srg  19864  znf1o  19948  zzngim  19949  cygznlem1  19963  cygznlem2a  19964  cygznlem3  19966  cygth  19968  thlle  20089  cpm2mf  20605  m2cpminvid2lem  20607  m2cpminvid2  20608  m2cpmfo  20609  decpmatid  20623  pmatcollpw3  20637  pmatcollpw3fi1lem1  20639  pmatcollpwscmatlem1  20642  pmatcollpwscmatlem2  20643  idpm2idmp  20654  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  cpmadugsumlemF  20729  dscmet  22424  itgcnlem  23601  dvn0  23732  dvn1  23734  cpncn  23744  dveflem  23787  c1lip2  23806  tdeglem4  23865  deg1le0  23916  ply1divex  23941  ply1rem  23968  fta1g  23972  plyconst  24007  plypf1  24013  plyco  24042  0dgr  24046  0dgrb  24047  coefv0  24049  dgreq0  24066  vieta1lem2  24111  vieta1  24112  aareccl  24126  aannenlem2  24129  taylthlem1  24172  radcnv0  24215  abelthlem6  24235  abelthlem9  24239  logtayl  24451  cxp0  24461  cxpeq  24543  leibpilem2  24713  leibpi  24714  log2ublem3  24720  log2ub  24721  log2le1  24722  birthday  24726  divsqrtsumlem  24751  dmgmn0  24797  lgambdd  24808  sqff1o  24953  ppiublem2  24973  chtublem  24981  bclbnd  25050  bposlem8  25061  lgsval  25071  dchrisum0flblem1  25242  dchrisum0flb  25244  ostth2lem2  25368  usgrexmplef  26196  usgr0edg0rusgr  26527  usgr2pthlem  26715  wwlksn0s  26815  rusgrnumwwlkb0  26938  erclwwlkref  26977  clwwlkf1  27012  0wlkonlem1  27096  upgr4cycl4dv4e  27163  1kp2ke3k  27433  ex-fac  27438  ex-prmo  27446  nn0min  29695  dpmul1000  29735  dp0h  29738  dpexpp1  29744  dpmul4  29750  threehalves  29751  1mhdrd  29752  lmatcl  30010  lmat22e12  30013  lmat22e21  30014  fsumcvg4  30124  oddpwdc  30544  eulerpartlems  30550  eulerpartlemb  30558  eulerpartlemt  30561  eulerpartgbij  30562  eulerpartlemmf  30565  eulerpartlemgf  30569  eulerpartlemgs2  30570  eulerpartlemn  30571  fib0  30589  fib1  30590  fibp1  30591  ofcs1  30749  signsply0  30756  signsvvf  30784  prodfzo03  30809  repr0  30817  breprexp  30839  hgt750lemd  30854  hgt750lem  30857  hgt750lem2  30858  hgt750leme  30864  tgoldbachgtde  30866  subfac0  31285  subfacval2  31295  subfaclim  31296  cvmliftlem7  31399  cvmliftlem13  31404  bccolsum  31751  fwddifn0  32396  heiborlem4  33743  heiborlem10  33749  nacsfix  37592  diophrw  37639  pell1qr1  37752  monotoddzzfi  37824  jm2.23  37880  hbtlem5  38015  mncn0  38026  aaitgo  38049  mon1pid  38100  brfvrcld  38300  corclrcl  38316  dfrtrcl3  38342  fvrtrcllb0d  38344  fvrtrcllb0da  38345  corcltrcl  38348  cotrclrcl  38351  k0004val0  38769  bccn0  38859  bccn1  38860  binomcxplemradcnv  38868  binomcxplemnotnn0  38872  dvnmul  40476  dvnprodlem3  40481  wallispilem2  40601  wallispi2lem2  40607  stirlinglem5  40613  stirlinglem7  40615  fourierdlem83  40724  fourierdlem112  40753  fouriersw  40766  elaa2lem  40768  elaa2  40769  etransclem48  40817  etransc  40818  iccelpart  41694  pfx2  41737  fmtno0  41777  fmtnorec2  41780  fmtno5lem1  41790  fmtno5lem2  41791  fmtno5lem4  41793  257prm  41798  fmtnofac2  41806  fmtnofac1  41807  fmtno4prmfac  41809  fmtno4nprmfac193  41811  fmtno5faclem1  41816  fmtno5faclem2  41817  fmtno5faclem3  41818  fmtno5fac  41819  fmtno5nprm  41820  139prmALT  41836  31prm  41837  127prm  41840  2exp11  41842  m11nprm  41843  bits0ALTV  41915  evengpoap3  42012  tgoldbachlt  42029  tgoldbach  42030  tgoldbachltOLD  42035  tgoldbachOLD  42037  ssnn0ssfz  42452  dig1  42727  0dig2nn0e  42731  0dig2nn0o  42732
  Copyright terms: Public domain W3C validator