Theorem 0nn0 12407

Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
0nn0	⊢ 0 ∈ ℕ0

Proof of Theorem 0nn0

Step	Hyp	Ref	Expression
1		eqid 2733	. 2 ⊢ 0 = 0
2		elnn0 12394	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 228	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 876	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 847   = wceq 1541   ∈ wcel 2113  0cc0 11017  ℕcn 12136  ℕ₀cn0 12392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-mulcl 11079  ax-i2m1 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4578  df-n0 12393

This theorem is referenced by:  0xnn0  12471  nn0ind-raph  12583  10nn0  12616  declei  12634  numlti  12635  nummul1c  12647  decaddc2  12654  decrmanc  12655  decrmac  12656  decaddm10  12657  decaddi  12658  decaddci  12659  decaddci2  12660  decmul1  12662  decmulnc  12665  6p5e11  12671  7p4e11  12674  8p3e11  12679  9p2e11  12685  10p10e20  12693  xnn0n0n1ge2b  13037  0elfz  13531  4fvwrd4  13555  fvinim0ffz  13696  ssnn0fi  13899  fsuppmapnn0fiubex  13906  exple1  14091  nn0opth2  14186  faclbnd4lem3  14209  bc0k  14225  bcn1  14227  bccl  14236  hasheq0  14277  hashrabrsn  14286  hashbc  14367  fi1uzind  14421  brfi1ind  14423  opfi1ind  14426  iswrdi  14431  wrdnfi  14462  s1fv  14525  ccat2s1fst  14554  splfv2a  14670  repsw0  14691  0csh0  14707  cshw1  14736  s2fv0  14801  s3fv0  14805  s4fv0  14809  pfx2  14861  ofs1  14884  relexp0g  14936  relexpaddg  14967  rtrclreclem2  14973  fsumnn0cl  15650  binom  15744  bcxmas  15749  isumnn0nn  15756  climcndslem1  15763  geoser  15781  geomulcvg  15790  risefac0  15941  fallfac0  15942  risefac1  15947  fallfac1  15948  binomfallfaclem2  15954  binomfallfac  15955  bpoly0  15964  bpoly2  15971  bpoly3  15972  bpoly4  15973  fsumcube  15974  ef0lem  15992  ege2le3  16004  ef4p  16029  efgt1p2  16030  efgt1p  16031  ruclem11  16156  nthruz  16169  nn0o  16301  ndvdssub  16327  5ndvds3  16331  bits0  16346  0bits  16357  sadcf  16371  sadc0  16372  sadcaddlem  16375  sadcadd  16376  sadadd2lem  16377  sadadd2  16378  smupf  16396  smup0  16397  smumullem  16410  gcdcl  16424  nn0seqcvgd  16488  algcvg  16494  eucalg  16505  lcmcl  16519  lcmfval  16539  lcmfcl  16546  pclem  16757  pcfac  16818  vdwap0  16895  vdwap1  16896  vdwlem6  16905  hashbc0  16924  0ram  16939  0ramcl  16942  ramz2  16943  ramz  16944  ramcl  16948  prmo0  16955  dec5dvds2  16984  2exp11  17008  2exp16  17009  11prm  17033  37prm  17039  43prm  17040  83prm  17041  139prm  17042  163prm  17043  317prm  17044  631prm  17045  1259lem1  17049  1259lem2  17050  1259lem3  17051  1259lem4  17052  1259lem5  17053  2503lem1  17055  2503lem2  17056  2503lem3  17057  2503prm  17058  4001lem1  17059  4001lem2  17060  4001lem3  17061  4001lem4  17062  4001prm  17063  plendxnocndx  17295  slotsdifdsndx  17305  slotsdifunifndx  17312  odrngstr  17314  slotsdifplendx2  17327  imasvalstr  17362  ipostr  18443  gsumws1  18754  cycsubm  19122  psgnunilem2  19415  psgnunilem3  19416  odfval  19452  oddvdsnn0  19464  pgp0  19516  sylow1lem1  19518  cyggex2  19817  telgsums  19913  srgbinomlem3  20154  srgbinomlem4  20155  srgbinom  20157  cnfldstr  21302  cnfldstrOLD  21317  nn0subm  21368  expmhm  21382  nn0srg  21383  znf1o  21497  zzngim  21498  cygznlem1  21512  cygznlem2a  21513  cygznlem3  21515  cygth  21517  freshmansdream  21520  snifpsrbag  21867  fczpsrbag  21868  psrbagaddcl  21871  psrlidm  21908  mvrf1  21932  mplcoe3  21984  mplcoe5  21986  ltbwe  21990  psrbag0  22008  psrbagsn  22009  evlslem1  22028  mhpsclcl  22081  mhpmulcl  22083  psdmul  22100  psdmvr  22103  00ply1bas  22171  ply1plusgfvi  22173  coe1sclmul  22215  coe1sclmul2  22217  coe1scl  22220  ply1sclid  22221  ply1idvr1OLD  22230  cply1coe0bi  22237  ply1scleq  22240  cpm2mf  22687  m2cpminvid2lem  22689  m2cpminvid2  22690  m2cpmfo  22691  decpmatid  22705  pmatcollpw3  22719  pmatcollpw3fi1lem1  22721  pmatcollpwscmatlem1  22724  pmatcollpwscmatlem2  22725  idpm2idmp  22736  chfacfscmulgsum  22795  chfacfpmmulgsum  22799  cpmadugsumlemF  22811  dscmet  24507  ehl0base  25363  ehl0  25364  itgcnlem  25738  dvn0  25873  dvn1  25875  cpncn  25885  dveflem  25930  c1lip2  25950  deg1le0  26063  ply1divex  26089  mon1pid  26106  ply1rem  26118  fta1g  26122  plyconst  26158  plypf1  26164  plyco  26193  0dgr  26197  0dgrb  26198  coefv0  26200  dgreq0  26218  vieta1lem2  26266  vieta1  26267  aareccl  26281  aannenlem2  26284  taylthlem1  26328  radcnv0  26372  abelthlem6  26393  abelthlem9  26397  logtayl  26616  cxp0  26626  cxpeq  26714  leibpilem2  26898  leibpi  26899  log2ublem3  26905  log2ub  26906  log2le1  26907  divsqrtsumlem  26937  dmgmn0  26983  lgambdd  26994  sqff1o  27139  ppiublem2  27161  chtublem  27169  bclbnd  27238  bposlem8  27249  lgsval  27259  dchrisum0flblem1  27466  dchrisum0flb  27468  ostth2lem2  27592  usgrexmplef  29258  usgr0edg0rusgr  29575  usgr2pthlem  29762  wwlksn0s  29860  rusgrnumwwlkb0  29973  erclwwlkref  30021  clwwlkf1  30050  0wlkonlem1  30119  upgr4cycl4dv4e  30186  1kp2ke3k  30447  ex-fac  30452  ex-prmo  30460  nn0min  32829  dpmul1000  32908  dp0h  32911  dpexpp1  32917  dpmul4  32923  threehalves  32924  1mhdrd  32925  s1f1  32953  s2f1  32955  cshw1s2  32970  cycpm2tr  33129  deg1le0eq0  33582  ply1unit  33584  evl1deg1  33585  evl1deg2  33586  evl1deg3  33587  ply1dg1rt  33589  m1pmeq  33594  psrbasfsupp  33621  mplmulmvr  33632  evlextv  33635  mplvrpmlem  33636  mplvrpmfgalem  33637  mplvrpmga  33638  mplvrpmmhm  33639  mplvrpmrhm  33640  esplyfval0  33650  esplylem  33652  esplyfv1  33655  esplyind  33659  vietalem  33663  vieta  33664  minplyirredlem  33795  rtelextdg2lem  33811  fldext2chn  33813  constraddcl  33847  constrnegcl  33848  constrdircl  33850  constrremulcl  33852  2sqr3minply  33865  lmatcl  33901  lmat22e12  33904  lmat22e21  33905  fsumcvg4  34035  oddpwdc  34439  eulerpartlems  34445  eulerpartlemb  34453  eulerpartlemt  34456  eulerpartgbij  34457  eulerpartlemmf  34460  eulerpartlemgf  34464  eulerpartlemgs2  34465  eulerpartlemn  34466  fib0  34484  fib1  34485  fibp1  34486  ofcs1  34629  signsply0  34636  signsvvf  34664  prodfzo03  34688  repr0  34696  breprexp  34718  hgt750lemd  34733  hgt750lem  34736  hgt750lem2  34737  hgt750leme  34743  tgoldbachgtde  34745  0nn0m1nnn0  35229  f1resfz0f1d  35230  usgrgt2cycl  35246  subfac0  35293  subfacval2  35303  subfaclim  35304  cvmliftlem7  35407  cvmliftlem13  35412  bccolsum  35855  fwddifn0  36280  heiborlem4  37927  heiborlem10  37933  12gcd5e1  42169  60gcd6e6  42170  60gcd7e1  42171  420gcd8e4  42172  12lcm5e60  42174  60lcm7e420  42176  420lcm8e840  42177  lcmineqlem  42218  3exp7  42219  3lexlogpow5ineq1  42220  3lexlogpow5ineq2  42221  3lexlogpow5ineq5  42226  aks4d1p1  42242  aks6d1c2lem4  42293  aks6d1c2  42296  sticksstones11  42322  sticksstones22  42334  aks6d1c7lem1  42346  sqn5i  42455  decpmul  42458  sqdeccom12  42459  sq3deccom12  42460  235t711  42475  ex-decpmul  42476  mhphflem  42754  0prjspn  42786  sum9cubes  42830  nacsfix  42869  diophrw  42916  pell1qr1  43028  monotoddzzfi  43099  jm2.23  43153  hbtlem5  43285  mncn0  43296  aaitgo  43319  brfvrcld  43848  corclrcl  43864  dfrtrcl3  43890  fvrtrcllb0d  43892  fvrtrcllb0da  43893  corcltrcl  43896  cotrclrcl  43899  k0004val0  44311  bccn0  44500  bccn1  44501  binomcxplemradcnv  44509  binomcxplemnotnn0  44513  rexanuz2nf  45652  dvnmul  46103  dvnprodlem3  46108  wallispilem2  46226  wallispi2lem2  46232  stirlinglem5  46238  stirlinglem7  46240  fourierdlem83  46349  fourierdlem112  46378  fouriersw  46391  elaa2lem  46393  elaa2  46394  etransclem48  46442  etransc  46443  iccelpart  47595  fmtno0  47702  fmtnorec2  47705  fmtno5lem1  47715  fmtno5lem2  47716  fmtno5lem4  47718  257prm  47723  fmtnofac2  47731  fmtnofac1  47732  fmtno4prmfac  47734  fmtno4nprmfac193  47736  fmtno5faclem1  47741  fmtno5faclem2  47742  fmtno5faclem3  47743  fmtno5fac  47744  fmtno5nprm  47745  139prmALT  47758  31prm  47759  127prm  47761  m11nprm  47763  bits0ALTV  47841  2exp340mod341  47895  nfermltl2rev  47905  evengpoap3  47961  tgoldbachlt  47978  tgoldbach  47979  stgr0  48122  usgrexmpl1lem  48183  usgrexmpl2lem  48188  gpgprismgr4cycllem6  48262  gpgprismgr4cycllem7  48263  gpgprismgr4cycllem10  48266  nn0mnd  48341  ssnn0ssfz  48511  dig1  48770  0dig2nn0e  48774  0dig2nn0o  48775  0aryfvalel  48796  itcoval0  48824  itcoval1  48825  ackval0  48842  ackval1  48843  ackvalsuc0val  48849  ackval0012  48851  ackval1012  48852  ackval2012  48853  ackval3012  48854  ackval41a  48856