Theorem 0nn0 12070

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 2736	. 2 ⊢ 0 = 0
2		elnn0 12057	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 231	. . 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 1543   ∈ wcel 2112  0cc0 10694  ℕcn 11795  ℕ₀cn0 12055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-mulcl 10756  ax-i2m1 10762

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-sn 4528  df-n0 12056

This theorem is referenced by:  0xnn0  12133  nn0ind-raph  12242  10nn0  12276  declei  12294  numlti  12295  nummul1c  12307  decaddc2  12314  decrmanc  12315  decrmac  12316  decaddm10  12317  decaddi  12318  decaddci  12319  decaddci2  12320  decmul1  12322  decmulnc  12325  6p5e11  12331  7p4e11  12334  8p3e11  12339  9p2e11  12345  10p10e20  12353  xnn0n0n1ge2b  12688  0elfz  13174  4fvwrd4  13197  fvinim0ffz  13326  ssnn0fi  13523  fsuppmapnn0fiubex  13530  exple1  13711  nn0opth2  13803  faclbnd4lem3  13826  bc0k  13842  bcn1  13844  bccl  13853  hasheq0  13895  hashrabrsn  13904  hashbc  13982  fi1uzind  14028  brfi1ind  14030  opfi1ind  14033  iswrdi  14038  wrdnfi  14068  s1fv  14132  ccat2s1fst  14168  ccat2s1fstOLD  14169  splfv2a  14286  repsw0  14307  0csh0  14323  cshw1  14352  s2fv0  14417  s3fv0  14421  s4fv0  14425  pfx2  14477  ofs1  14498  relexp0g  14550  relexpaddg  14581  rtrclreclem2  14587  fsumnn0cl  15265  binom  15357  bcxmas  15362  isumnn0nn  15369  climcndslem1  15376  geoser  15394  geomulcvg  15403  risefac0  15552  fallfac0  15553  risefac1  15558  fallfac1  15559  binomfallfaclem2  15565  binomfallfac  15566  bpoly0  15575  bpoly2  15582  bpoly3  15583  bpoly4  15584  fsumcube  15585  ef0lem  15603  ege2le3  15614  ef4p  15637  efgt1p2  15638  efgt1p  15639  ruclem11  15764  nthruz  15777  nn0o  15907  ndvdssub  15933  bits0  15950  0bits  15961  sadcf  15975  sadc0  15976  sadcaddlem  15979  sadcadd  15980  sadadd2lem  15981  sadadd2  15982  smupf  16000  smup0  16001  smumullem  16014  gcdcl  16028  nn0seqcvgd  16090  algcvg  16096  eucalg  16107  lcmcl  16121  lcmfval  16141  lcmfcl  16148  pclem  16354  pcfac  16415  vdwap0  16492  vdwap1  16493  vdwlem6  16502  hashbc0  16521  0ram  16536  0ramcl  16539  ramz2  16540  ramz  16541  ramcl  16545  prmo0  16552  dec5dvds2  16581  2exp11  16606  2exp16  16607  11prm  16631  37prm  16637  43prm  16638  83prm  16639  139prm  16640  163prm  16641  317prm  16642  631prm  16643  1259lem1  16647  1259lem2  16648  1259lem3  16649  1259lem4  16650  1259lem5  16651  2503lem1  16653  2503lem2  16654  2503lem3  16655  2503prm  16656  4001lem1  16657  4001lem2  16658  4001lem3  16659  4001lem4  16660  4001prm  16661  odrngstr  16864  imasvalstr  16910  ipostr  17989  gsumws1  18218  cycsubm  18563  psgnunilem2  18841  psgnunilem3  18842  odfval  18878  oddvdsnn0  18890  pgp0  18939  sylow1lem1  18941  cyggex2  19236  telgsums  19332  srgbinomlem3  19511  srgbinomlem4  19512  srgbinom  19514  cnfldstr  20319  cnfldfun  20329  nn0subm  20372  expmhm  20386  nn0srg  20387  znf1o  20470  zzngim  20471  cygznlem1  20485  cygznlem2a  20486  cygznlem3  20488  cygth  20490  thlle  20613  snifpsrbag  20835  fczpsrbag  20836  psrbagaddcl  20841  psrlidm  20882  mvrf1  20904  mplcoe3  20949  mplcoe5  20951  ltbwe  20955  psrbag0  20974  psrbagsn  20975  evlslem1  20996  mhpsclcl  21041  mhpmulcl  21043  00ply1bas  21115  ply1plusgfvi  21117  coe1sclmul  21157  coe1sclmul2  21159  coe1scl  21162  ply1sclid  21163  ply1idvr1  21168  cply1coe0bi  21175  cpm2mf  21603  m2cpminvid2lem  21605  m2cpminvid2  21606  m2cpmfo  21607  decpmatid  21621  pmatcollpw3  21635  pmatcollpw3fi1lem1  21637  pmatcollpwscmatlem1  21640  pmatcollpwscmatlem2  21641  idpm2idmp  21652  chfacfscmulgsum  21711  chfacfpmmulgsum  21715  cpmadugsumlemF  21727  dscmet  23424  ehl0base  24267  ehl0  24268  itgcnlem  24641  dvn0  24775  dvn1  24777  cpncn  24787  dveflem  24830  c1lip2  24849  tdeglem4OLD  24912  deg1le0  24963  ply1divex  24988  ply1rem  25015  fta1g  25019  plyconst  25054  plypf1  25060  plyco  25089  0dgr  25093  0dgrb  25094  coefv0  25096  dgreq0  25113  vieta1lem2  25158  vieta1  25159  aareccl  25173  aannenlem2  25176  taylthlem1  25219  radcnv0  25262  abelthlem6  25282  abelthlem9  25286  logtayl  25502  cxp0  25512  cxpeq  25597  leibpilem2  25778  leibpi  25779  log2ublem3  25785  log2ub  25786  log2le1  25787  divsqrtsumlem  25816  dmgmn0  25862  lgambdd  25873  sqff1o  26018  ppiublem2  26038  chtublem  26046  bclbnd  26115  bposlem8  26126  lgsval  26136  dchrisum0flblem1  26343  dchrisum0flb  26345  ostth2lem2  26469  usgrexmplef  27301  usgr0edg0rusgr  27617  usgr2pthlem  27804  wwlksn0s  27899  rusgrnumwwlkb0  28009  erclwwlkref  28057  clwwlkf1  28086  0wlkonlem1  28155  upgr4cycl4dv4e  28222  1kp2ke3k  28483  ex-fac  28488  ex-prmo  28496  nn0min  30808  dpmul1000  30847  dp0h  30850  dpexpp1  30856  dpmul4  30862  threehalves  30863  1mhdrd  30864  s1f1  30891  s2f1  30893  cshw1s2  30906  cycpm2tr  31059  freshmansdream  31157  ply1scleq  31336  lmatcl  31434  lmat22e12  31437  lmat22e21  31438  fsumcvg4  31568  oddpwdc  31987  eulerpartlems  31993  eulerpartlemb  32001  eulerpartlemt  32004  eulerpartgbij  32005  eulerpartlemmf  32008  eulerpartlemgf  32012  eulerpartlemgs2  32013  eulerpartlemn  32014  fib0  32032  fib1  32033  fibp1  32034  ofcs1  32189  signsply0  32196  signsvvf  32224  prodfzo03  32249  repr0  32257  breprexp  32279  hgt750lemd  32294  hgt750lem  32297  hgt750lem2  32298  hgt750leme  32304  tgoldbachgtde  32306  0nn0m1nnn0  32738  f1resfz0f1d  32739  usgrgt2cycl  32759  subfac0  32806  subfacval2  32816  subfaclim  32817  cvmliftlem7  32920  cvmliftlem13  32925  bccolsum  33374  fwddifn0  34152  heiborlem4  35658  heiborlem10  35664  12gcd5e1  39694  60gcd6e6  39695  60gcd7e1  39696  420gcd8e4  39697  12lcm5e60  39699  60lcm7e420  39701  420lcm8e840  39702  lcmineqlem  39743  3exp7  39744  3lexlogpow5ineq1  39745  3lexlogpow5ineq2  39746  3lexlogpow5ineq5  39751  aks4d1p1  39766  sticksstones11  39781  mhphflem  39935  sqn5i  39961  decpmul  39964  sqdeccom12  39965  sq3deccom12  39966  235t711  39967  ex-decpmul  39968  0prjspn  40114  nacsfix  40178  diophrw  40225  pell1qr1  40337  monotoddzzfi  40408  jm2.23  40462  hbtlem5  40597  mncn0  40608  aaitgo  40631  mon1pid  40674  brfvrcld  40917  corclrcl  40933  dfrtrcl3  40959  fvrtrcllb0d  40961  fvrtrcllb0da  40962  corcltrcl  40965  cotrclrcl  40968  k0004val0  41382  bccn0  41575  bccn1  41576  binomcxplemradcnv  41584  binomcxplemnotnn0  41588  dvnmul  43102  dvnprodlem3  43107  wallispilem2  43225  wallispi2lem2  43231  stirlinglem5  43237  stirlinglem7  43239  fourierdlem83  43348  fourierdlem112  43377  fouriersw  43390  elaa2lem  43392  elaa2  43393  etransclem48  43441  etransc  43442  iccelpart  44501  fmtno0  44608  fmtnorec2  44611  fmtno5lem1  44621  fmtno5lem2  44622  fmtno5lem4  44624  257prm  44629  fmtnofac2  44637  fmtnofac1  44638  fmtno4prmfac  44640  fmtno4nprmfac193  44642  fmtno5faclem1  44647  fmtno5faclem2  44648  fmtno5faclem3  44649  fmtno5fac  44650  fmtno5nprm  44651  139prmALT  44664  31prm  44665  127prm  44667  m11nprm  44669  bits0ALTV  44747  2exp340mod341  44801  nfermltl2rev  44811  evengpoap3  44867  tgoldbachlt  44884  tgoldbach  44885  nn0mnd  44989  ssnn0ssfz  45301  dig1  45570  0dig2nn0e  45574  0dig2nn0o  45575  0aryfvalel  45596  itcoval0  45624  itcoval1  45625  ackval0  45642  ackval1  45643  ackvalsuc0val  45649  ackval0012  45651  ackval1012  45652  ackval2012  45653  ackval3012  45654  ackval41a  45656  prstcleval  45965