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

Theorem 0nn0 11577
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 2813 . 2 0 = 0
2 elnn0 11564 . . . 4 (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
32biimpri 219 . . 3 ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
43olcs 894 . 2 (0 = 0 → 0 ∈ ℕ0)
51, 4ax-mp 5 1 0 ∈ ℕ0
Colors of variables: wff setvar class
Syntax hints:  wo 865   = wceq 1637  wcel 2157  0cc0 10224  cn 11308  0cn0 11562
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  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-mulcl 10286  ax-i2m1 10292
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  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-v 3400  df-un 3781  df-sn 4378  df-n0 11563
This theorem is referenced by:  0xnn0  11638  nn0ind-raph  11746  10nn0  11780  declei  11798  numlti  11799  nummul1c  11811  decaddc2  11818  decrmanc  11819  decrmac  11820  decaddm10  11821  decaddi  11822  decaddci  11823  decaddci2  11824  decmul1  11826  decmulnc  11829  6p5e11  11835  7p4e11  11838  8p3e11  11843  9p2e11  11849  10p10e20  11857  xnn0n0n1ge2b  12184  0elfz  12663  4fvwrd4  12686  fvinim0ffz  12814  ssnn0fi  13011  fsuppmapnn0fiubex  13018  exple1  13146  sq10  13274  nn0opth2  13282  faclbnd4lem3  13305  bc0k  13321  bcn1  13323  bccl  13332  hasheq0  13375  hashrabrsn  13382  hashbc  13457  fi1uzind  13499  brfi1ind  13501  opfi1ind  13504  iswrdi  13523  s1fv  13608  ccat2s1fst  13642  2swrdeqwrdeq  13680  wrdeqs1cat  13701  splfv2a  13734  repsw0  13751  0csh0  13766  repswcshw  13785  cshw1  13795  s2fv0  13859  s3fv0  13863  s4fv0  13867  ofs1  13937  relexp0g  13988  relexpaddg  14019  rtrclreclem1  14024  fsumnn0cl  14693  binom  14787  bcxmas  14792  isumnn0nn  14799  climcndslem1  14806  geoser  14824  geomulcvg  14832  risefac0  14981  fallfac0  14982  risefac1  14987  fallfac1  14988  binomfallfaclem2  14994  binomfallfac  14995  bpoly0  15004  bpoly2  15011  bpoly3  15012  bpoly4  15013  fsumcube  15014  ef0lem  15032  ege2le3  15043  ef4p  15066  efgt1p2  15067  efgt1p  15068  ruclem11  15192  nthruz  15205  nn0o  15322  ndvdssub  15355  bits0  15372  0bits  15383  sadcf  15397  sadc0  15398  sadcaddlem  15401  sadcadd  15402  sadadd2lem  15403  sadadd2  15404  smupf  15422  smup0  15423  smumullem  15436  gcdcl  15450  nn0seqcvgd  15505  algcvg  15511  eucalg  15522  lcmcl  15536  lcmfval  15556  lcmfcl  15563  pclem  15763  pcfac  15823  vdwap0  15900  vdwap1  15901  vdwlem6  15910  hashbc0  15929  0ram  15944  0ramcl  15947  ramz2  15948  ramz  15949  ramcl  15953  prmo0  15960  dec5dvds2  15989  2exp16  16012  11prm  16036  37prm  16042  43prm  16043  83prm  16044  139prm  16045  163prm  16046  317prm  16047  631prm  16048  1259lem1  16052  1259lem2  16053  1259lem3  16054  1259lem4  16055  1259lem5  16056  2503lem1  16058  2503lem2  16059  2503lem3  16060  2503prm  16061  4001lem1  16062  4001lem2  16063  4001lem3  16064  4001lem4  16065  4001prm  16066  odrngstr  16274  imasvalstr  16320  ipostr  17361  gsumws1  17584  psgnunilem2  18119  psgnunilem3  18120  oddvdsnn0  18167  pgp0  18215  sylow1lem1  18217  cyggex2  18502  telgsums  18595  srgbinomlem3  18747  srgbinomlem4  18748  srgbinom  18750  snifpsrbag  19578  fczpsrbag  19579  psrlidm  19615  mvrf1  19637  mplcoe3  19678  mplcoe5  19680  ltbwe  19684  psrbag0  19705  psrbagsn  19706  evlslem1  19726  00ply1bas  19821  ply1plusgfvi  19823  coe1sclmul  19863  coe1sclmul2  19865  coe1scl  19868  ply1sclid  19869  ply1idvr1  19874  cply1coe0bi  19881  cnfldstr  19959  cnfldfun  19969  nn0subm  20012  expmhm  20026  nn0srg  20027  znf1o  20110  zzngim  20111  cygznlem1  20125  cygznlem2a  20126  cygznlem3  20128  cygth  20130  thlle  20255  cpm2mf  20774  m2cpminvid2lem  20776  m2cpminvid2  20777  m2cpmfo  20778  decpmatid  20792  pmatcollpw3  20806  pmatcollpw3fi1lem1  20808  pmatcollpwscmatlem1  20811  pmatcollpwscmatlem2  20812  idpm2idmp  20823  chfacfscmulgsum  20882  chfacfpmmulgsum  20886  cpmadugsumlemF  20898  dscmet  22594  itgcnlem  23776  dvn0  23907  dvn1  23909  cpncn  23919  dveflem  23962  c1lip2  23981  tdeglem4  24040  deg1le0  24091  ply1divex  24116  ply1rem  24143  fta1g  24147  plyconst  24182  plypf1  24188  plyco  24217  0dgr  24221  0dgrb  24222  coefv0  24224  dgreq0  24241  vieta1lem2  24286  vieta1  24287  aareccl  24301  aannenlem2  24304  taylthlem1  24347  radcnv0  24390  abelthlem6  24410  abelthlem9  24414  logtayl  24626  cxp0  24636  cxpeq  24718  leibpilem2  24888  leibpi  24889  log2ublem3  24895  log2ub  24896  log2le1  24897  birthday  24901  divsqrtsumlem  24926  dmgmn0  24972  lgambdd  24983  sqff1o  25128  ppiublem2  25148  chtublem  25156  bclbnd  25225  bposlem8  25236  lgsval  25246  dchrisum0flblem1  25417  dchrisum0flb  25419  ostth2lem2  25543  usgrexmplef  26373  usgr0edg0rusgr  26705  usgr2pthlem  26893  wwlksn0s  26994  rusgrnumwwlkb0  27119  erclwwlkref  27169  clwwlkf1  27204  0wlkonlem1  27297  upgr4cycl4dv4e  27364  1kp2ke3k  27640  ex-fac  27645  ex-prmo  27653  nn0min  29900  dpmul1000  29938  dp0h  29941  dpexpp1  29947  dpmul4  29953  threehalves  29954  1mhdrd  29955  lmatcl  30213  lmat22e12  30216  lmat22e21  30217  fsumcvg4  30327  oddpwdc  30747  eulerpartlems  30753  eulerpartlemb  30761  eulerpartlemt  30764  eulerpartgbij  30765  eulerpartlemmf  30768  eulerpartlemgf  30772  eulerpartlemgs2  30773  eulerpartlemn  30774  fib0  30792  fib1  30793  fibp1  30794  ofcs1  30952  signsply0  30959  signsvvf  30987  prodfzo03  31012  repr0  31020  breprexp  31042  hgt750lemd  31057  hgt750lem  31060  hgt750lem2  31061  hgt750leme  31067  tgoldbachgtde  31069  subfac0  31487  subfacval2  31497  subfaclim  31498  cvmliftlem7  31601  cvmliftlem13  31606  bccolsum  31952  fwddifn0  32597  heiborlem4  33926  heiborlem10  33932  sqn5i  37747  nacsfix  37778  diophrw  37825  pell1qr1  37938  monotoddzzfi  38009  jm2.23  38065  hbtlem5  38200  mncn0  38211  aaitgo  38234  mon1pid  38285  brfvrcld  38484  corclrcl  38500  dfrtrcl3  38526  fvrtrcllb0d  38528  fvrtrcllb0da  38529  corcltrcl  38532  cotrclrcl  38535  k0004val0  38953  bccn0  39043  bccn1  39044  binomcxplemradcnv  39052  binomcxplemnotnn0  39056  dvnmul  40639  dvnprodlem3  40644  wallispilem2  40763  wallispi2lem2  40769  stirlinglem5  40775  stirlinglem7  40777  fourierdlem83  40886  fourierdlem112  40915  fouriersw  40928  elaa2lem  40930  elaa2  40931  etransclem48  40979  etransc  40980  iccelpart  41945  pfx2  41988  fmtno0  42028  fmtnorec2  42031  fmtno5lem1  42041  fmtno5lem2  42042  fmtno5lem4  42044  257prm  42049  fmtnofac2  42057  fmtnofac1  42058  fmtno4prmfac  42060  fmtno4nprmfac193  42062  fmtno5faclem1  42067  fmtno5faclem2  42068  fmtno5faclem3  42069  fmtno5fac  42070  fmtno5nprm  42071  139prmALT  42087  31prm  42088  127prm  42091  2exp11  42093  m11nprm  42094  bits0ALTV  42166  evengpoap3  42263  tgoldbachlt  42280  tgoldbach  42281  ssnn0ssfz  42696  dig1  42971  0dig2nn0e  42975  0dig2nn0o  42976
  Copyright terms: Public domain W3C validator