Theorem 0nn0 12568

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 2740	. 2 ⊢ 0 = 0
2		elnn0 12555	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 228	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 875	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 846   = wceq 1537   ∈ wcel 2108  0cc0 11184  ℕcn 12293  ℕ₀cn0 12553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-i2m1 11252

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-n0 12554

This theorem is referenced by:  0xnn0  12631  nn0ind-raph  12743  10nn0  12776  declei  12794  numlti  12795  nummul1c  12807  decaddc2  12814  decrmanc  12815  decrmac  12816  decaddm10  12817  decaddi  12818  decaddci  12819  decaddci2  12820  decmul1  12822  decmulnc  12825  6p5e11  12831  7p4e11  12834  8p3e11  12839  9p2e11  12845  10p10e20  12853  xnn0n0n1ge2b  13194  0elfz  13681  4fvwrd4  13705  fvinim0ffz  13836  ssnn0fi  14036  fsuppmapnn0fiubex  14043  exple1  14226  nn0opth2  14321  faclbnd4lem3  14344  bc0k  14360  bcn1  14362  bccl  14371  hasheq0  14412  hashrabrsn  14421  hashbc  14502  fi1uzind  14556  brfi1ind  14558  opfi1ind  14561  iswrdi  14566  wrdnfi  14596  s1fv  14658  ccat2s1fst  14687  splfv2a  14804  repsw0  14825  0csh0  14841  cshw1  14870  s2fv0  14936  s3fv0  14940  s4fv0  14944  pfx2  14996  ofs1  15019  relexp0g  15071  relexpaddg  15102  rtrclreclem2  15108  fsumnn0cl  15784  binom  15878  bcxmas  15883  isumnn0nn  15890  climcndslem1  15897  geoser  15915  geomulcvg  15924  risefac0  16075  fallfac0  16076  risefac1  16081  fallfac1  16082  binomfallfaclem2  16088  binomfallfac  16089  bpoly0  16098  bpoly2  16105  bpoly3  16106  bpoly4  16107  fsumcube  16108  ef0lem  16126  ege2le3  16138  ef4p  16161  efgt1p2  16162  efgt1p  16163  ruclem11  16288  nthruz  16301  nn0o  16431  ndvdssub  16457  bits0  16474  0bits  16485  sadcf  16499  sadc0  16500  sadcaddlem  16503  sadcadd  16504  sadadd2lem  16505  sadadd2  16506  smupf  16524  smup0  16525  smumullem  16538  gcdcl  16552  nn0seqcvgd  16617  algcvg  16623  eucalg  16634  lcmcl  16648  lcmfval  16668  lcmfcl  16675  pclem  16885  pcfac  16946  vdwap0  17023  vdwap1  17024  vdwlem6  17033  hashbc0  17052  0ram  17067  0ramcl  17070  ramz2  17071  ramz  17072  ramcl  17076  prmo0  17083  dec5dvds2  17112  2exp11  17137  2exp16  17138  11prm  17162  37prm  17168  43prm  17169  83prm  17170  139prm  17171  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  4001prm  17192  plendxnocndx  17443  slotsdifdsndx  17453  slotsdifunifndx  17460  odrngstr  17462  slotsdifplendx2  17476  imasvalstr  17511  ipostr  18599  gsumws1  18873  cycsubm  19242  psgnunilem2  19537  psgnunilem3  19538  odfval  19574  oddvdsnn0  19586  pgp0  19638  sylow1lem1  19640  cyggex2  19939  telgsums  20035  srgbinomlem3  20255  srgbinomlem4  20256  srgbinom  20258  cnfldstr  21389  cnfldstrOLD  21404  cnfldfunALTOLDOLD  21416  nn0subm  21463  expmhm  21477  nn0srg  21478  znf1o  21593  zzngim  21594  cygznlem1  21608  cygznlem2a  21609  cygznlem3  21611  cygth  21613  freshmansdream  21616  thlleOLD  21740  snifpsrbag  21963  fczpsrbag  21964  psrbagaddcl  21967  psrlidm  22005  mvrf1  22029  mplcoe3  22079  mplcoe5  22081  ltbwe  22085  psrbag0  22109  psrbagsn  22110  evlslem1  22129  mhpsclcl  22174  mhpmulcl  22176  psdmul  22193  00ply1bas  22262  ply1plusgfvi  22264  coe1sclmul  22306  coe1sclmul2  22308  coe1scl  22311  ply1sclid  22312  ply1idvr1OLD  22320  cply1coe0bi  22327  ply1scleq  22330  cpm2mf  22779  m2cpminvid2lem  22781  m2cpminvid2  22782  m2cpmfo  22783  decpmatid  22797  pmatcollpw3  22811  pmatcollpw3fi1lem1  22813  pmatcollpwscmatlem1  22816  pmatcollpwscmatlem2  22817  idpm2idmp  22828  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  cpmadugsumlemF  22903  dscmet  24606  ehl0base  25469  ehl0  25470  itgcnlem  25845  dvn0  25980  dvn1  25982  cpncn  25992  dveflem  26037  c1lip2  26057  deg1le0  26170  ply1divex  26196  mon1pid  26213  ply1rem  26225  fta1g  26229  plyconst  26265  plypf1  26271  plyco  26300  0dgr  26304  0dgrb  26305  coefv0  26307  dgreq0  26325  vieta1lem2  26371  vieta1  26372  aareccl  26386  aannenlem2  26389  taylthlem1  26433  radcnv0  26477  abelthlem6  26498  abelthlem9  26502  logtayl  26720  cxp0  26730  cxpeq  26818  leibpilem2  27002  leibpi  27003  log2ublem3  27009  log2ub  27010  log2le1  27011  divsqrtsumlem  27041  dmgmn0  27087  lgambdd  27098  sqff1o  27243  ppiublem2  27265  chtublem  27273  bclbnd  27342  bposlem8  27353  lgsval  27363  dchrisum0flblem1  27570  dchrisum0flb  27572  ostth2lem2  27696  usgrexmplef  29294  usgr0edg0rusgr  29611  usgr2pthlem  29799  wwlksn0s  29894  rusgrnumwwlkb0  30004  erclwwlkref  30052  clwwlkf1  30081  0wlkonlem1  30150  upgr4cycl4dv4e  30217  1kp2ke3k  30478  ex-fac  30483  ex-prmo  30491  nn0min  32824  dpmul1000  32863  dp0h  32866  dpexpp1  32872  dpmul4  32878  threehalves  32879  1mhdrd  32880  s1f1  32909  s2f1  32911  cshw1s2  32927  cycpm2tr  33112  deg1le0eq0  33563  ply1unit  33565  evl1deg1  33566  evl1deg2  33567  evl1deg3  33568  ply1dg1rt  33569  m1pmeq  33573  minplyirredlem  33703  rtelextdg2lem  33717  fldext2chn  33719  2sqr3minply  33738  lmatcl  33762  lmat22e12  33765  lmat22e21  33766  fsumcvg4  33896  oddpwdc  34319  eulerpartlems  34325  eulerpartlemb  34333  eulerpartlemt  34336  eulerpartgbij  34337  eulerpartlemmf  34340  eulerpartlemgf  34344  eulerpartlemgs2  34345  eulerpartlemn  34346  fib0  34364  fib1  34365  fibp1  34366  ofcs1  34521  signsply0  34528  signsvvf  34556  prodfzo03  34580  repr0  34588  breprexp  34610  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  hgt750leme  34635  tgoldbachgtde  34637  0nn0m1nnn0  35080  f1resfz0f1d  35081  usgrgt2cycl  35098  subfac0  35145  subfacval2  35155  subfaclim  35156  cvmliftlem7  35259  cvmliftlem13  35264  bccolsum  35701  fwddifn0  36128  heiborlem4  37774  heiborlem10  37780  12gcd5e1  41960  60gcd6e6  41961  60gcd7e1  41962  420gcd8e4  41963  12lcm5e60  41965  60lcm7e420  41967  420lcm8e840  41968  lcmineqlem  42009  3exp7  42010  3lexlogpow5ineq1  42011  3lexlogpow5ineq2  42012  3lexlogpow5ineq5  42017  aks4d1p1  42033  aks6d1c2lem4  42084  aks6d1c2  42087  sticksstones11  42113  sticksstones22  42125  aks6d1c7lem1  42137  sqn5i  42274  decpmul  42277  sqdeccom12  42278  sq3deccom12  42279  235t711  42293  ex-decpmul  42294  mhphflem  42551  0prjspn  42583  sum9cubes  42627  nacsfix  42668  diophrw  42715  pell1qr1  42827  monotoddzzfi  42899  jm2.23  42953  hbtlem5  43085  mncn0  43096  aaitgo  43119  brfvrcld  43653  corclrcl  43669  dfrtrcl3  43695  fvrtrcllb0d  43697  fvrtrcllb0da  43698  corcltrcl  43701  cotrclrcl  43704  k0004val0  44116  bccn0  44312  bccn1  44313  binomcxplemradcnv  44321  binomcxplemnotnn0  44325  rexanuz2nf  45408  dvnmul  45864  dvnprodlem3  45869  wallispilem2  45987  wallispi2lem2  45993  stirlinglem5  45999  stirlinglem7  46001  fourierdlem83  46110  fourierdlem112  46139  fouriersw  46152  elaa2lem  46154  elaa2  46155  etransclem48  46203  etransc  46204  iccelpart  47307  fmtno0  47414  fmtnorec2  47417  fmtno5lem1  47427  fmtno5lem2  47428  fmtno5lem4  47430  257prm  47435  fmtnofac2  47443  fmtnofac1  47444  fmtno4prmfac  47446  fmtno4nprmfac193  47448  fmtno5faclem1  47453  fmtno5faclem2  47454  fmtno5faclem3  47455  fmtno5fac  47456  fmtno5nprm  47457  139prmALT  47470  31prm  47471  127prm  47473  m11nprm  47475  bits0ALTV  47553  2exp340mod341  47607  nfermltl2rev  47617  evengpoap3  47673  tgoldbachlt  47690  tgoldbach  47691  usgrexmpl1lem  47836  usgrexmpl2lem  47841  nn0mnd  47902  ssnn0ssfz  48074  dig1  48342  0dig2nn0e  48346  0dig2nn0o  48347  0aryfvalel  48368  itcoval0  48396  itcoval1  48397  ackval0  48414  ackval1  48415  ackvalsuc0val  48421  ackval0012  48423  ackval1012  48424  ackval2012  48425  ackval3012  48426  ackval41a  48428  prstclevalOLD  48736