Theorem 0nn0 12514

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 2735	. 2 ⊢ 0 = 0
2		elnn0 12501	. . . 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 1540   ∈ wcel 2108  0cc0 11127  ℕcn 12238  ℕ₀cn0 12499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-i2m1 11195

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-n0 12500

This theorem is referenced by:  0xnn0  12578  nn0ind-raph  12691  10nn0  12724  declei  12742  numlti  12743  nummul1c  12755  decaddc2  12762  decrmanc  12763  decrmac  12764  decaddm10  12765  decaddi  12766  decaddci  12767  decaddci2  12768  decmul1  12770  decmulnc  12773  6p5e11  12779  7p4e11  12782  8p3e11  12787  9p2e11  12793  10p10e20  12801  xnn0n0n1ge2b  13146  0elfz  13639  4fvwrd4  13663  fvinim0ffz  13800  ssnn0fi  14001  fsuppmapnn0fiubex  14008  exple1  14193  nn0opth2  14288  faclbnd4lem3  14311  bc0k  14327  bcn1  14329  bccl  14338  hasheq0  14379  hashrabrsn  14388  hashbc  14469  fi1uzind  14523  brfi1ind  14525  opfi1ind  14528  iswrdi  14533  wrdnfi  14564  s1fv  14626  ccat2s1fst  14655  splfv2a  14772  repsw0  14793  0csh0  14809  cshw1  14838  s2fv0  14904  s3fv0  14908  s4fv0  14912  pfx2  14964  ofs1  14987  relexp0g  15039  relexpaddg  15070  rtrclreclem2  15076  fsumnn0cl  15750  binom  15844  bcxmas  15849  isumnn0nn  15856  climcndslem1  15863  geoser  15881  geomulcvg  15890  risefac0  16041  fallfac0  16042  risefac1  16047  fallfac1  16048  binomfallfaclem2  16054  binomfallfac  16055  bpoly0  16064  bpoly2  16071  bpoly3  16072  bpoly4  16073  fsumcube  16074  ef0lem  16092  ege2le3  16104  ef4p  16129  efgt1p2  16130  efgt1p  16131  ruclem11  16256  nthruz  16269  nn0o  16400  ndvdssub  16426  5ndvds3  16430  bits0  16445  0bits  16456  sadcf  16470  sadc0  16471  sadcaddlem  16474  sadcadd  16475  sadadd2lem  16476  sadadd2  16477  smupf  16495  smup0  16496  smumullem  16509  gcdcl  16523  nn0seqcvgd  16587  algcvg  16593  eucalg  16604  lcmcl  16618  lcmfval  16638  lcmfcl  16645  pclem  16856  pcfac  16917  vdwap0  16994  vdwap1  16995  vdwlem6  17004  hashbc0  17023  0ram  17038  0ramcl  17041  ramz2  17042  ramz  17043  ramcl  17047  prmo0  17054  dec5dvds2  17083  2exp11  17107  2exp16  17108  11prm  17132  37prm  17138  43prm  17139  83prm  17140  139prm  17141  163prm  17142  317prm  17143  631prm  17144  1259lem1  17148  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  2503lem1  17154  2503lem2  17155  2503lem3  17156  2503prm  17157  4001lem1  17158  4001lem2  17159  4001lem3  17160  4001lem4  17161  4001prm  17162  plendxnocndx  17396  slotsdifdsndx  17406  slotsdifunifndx  17413  odrngstr  17415  slotsdifplendx2  17428  imasvalstr  17463  ipostr  18537  gsumws1  18814  cycsubm  19183  psgnunilem2  19474  psgnunilem3  19475  odfval  19511  oddvdsnn0  19523  pgp0  19575  sylow1lem1  19577  cyggex2  19876  telgsums  19972  srgbinomlem3  20186  srgbinomlem4  20187  srgbinom  20189  cnfldstr  21315  cnfldstrOLD  21330  nn0subm  21388  expmhm  21402  nn0srg  21403  znf1o  21510  zzngim  21511  cygznlem1  21525  cygznlem2a  21526  cygznlem3  21528  cygth  21530  freshmansdream  21533  snifpsrbag  21878  fczpsrbag  21879  psrbagaddcl  21882  psrlidm  21920  mvrf1  21944  mplcoe3  21994  mplcoe5  21996  ltbwe  22000  psrbag0  22018  psrbagsn  22019  evlslem1  22038  mhpsclcl  22083  mhpmulcl  22085  psdmul  22102  psdmvr  22105  00ply1bas  22173  ply1plusgfvi  22175  coe1sclmul  22217  coe1sclmul2  22219  coe1scl  22222  ply1sclid  22223  ply1idvr1OLD  22231  cply1coe0bi  22238  ply1scleq  22241  cpm2mf  22688  m2cpminvid2lem  22690  m2cpminvid2  22691  m2cpmfo  22692  decpmatid  22706  pmatcollpw3  22720  pmatcollpw3fi1lem1  22722  pmatcollpwscmatlem1  22725  pmatcollpwscmatlem2  22726  idpm2idmp  22737  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  cpmadugsumlemF  22812  dscmet  24509  ehl0base  25366  ehl0  25367  itgcnlem  25741  dvn0  25876  dvn1  25878  cpncn  25888  dveflem  25933  c1lip2  25953  deg1le0  26066  ply1divex  26092  mon1pid  26109  ply1rem  26121  fta1g  26125  plyconst  26161  plypf1  26167  plyco  26196  0dgr  26200  0dgrb  26201  coefv0  26203  dgreq0  26221  vieta1lem2  26269  vieta1  26270  aareccl  26284  aannenlem2  26287  taylthlem1  26331  radcnv0  26375  abelthlem6  26396  abelthlem9  26400  logtayl  26619  cxp0  26629  cxpeq  26717  leibpilem2  26901  leibpi  26902  log2ublem3  26908  log2ub  26909  log2le1  26910  divsqrtsumlem  26940  dmgmn0  26986  lgambdd  26997  sqff1o  27142  ppiublem2  27164  chtublem  27172  bclbnd  27241  bposlem8  27252  lgsval  27262  dchrisum0flblem1  27469  dchrisum0flb  27471  ostth2lem2  27595  usgrexmplef  29184  usgr0edg0rusgr  29501  usgr2pthlem  29691  wwlksn0s  29789  rusgrnumwwlkb0  29899  erclwwlkref  29947  clwwlkf1  29976  0wlkonlem1  30045  upgr4cycl4dv4e  30112  1kp2ke3k  30373  ex-fac  30378  ex-prmo  30386  nn0min  32745  dpmul1000  32819  dp0h  32822  dpexpp1  32828  dpmul4  32834  threehalves  32835  1mhdrd  32836  s1f1  32864  s2f1  32866  cshw1s2  32882  cycpm2tr  33076  deg1le0eq0  33532  ply1unit  33534  evl1deg1  33535  evl1deg2  33536  evl1deg3  33537  ply1dg1rt  33538  m1pmeq  33542  minplyirredlem  33690  rtelextdg2lem  33706  fldext2chn  33708  constraddcl  33742  constrnegcl  33743  constrdircl  33745  constrremulcl  33747  2sqr3minply  33760  lmatcl  33793  lmat22e12  33796  lmat22e21  33797  fsumcvg4  33927  oddpwdc  34332  eulerpartlems  34338  eulerpartlemb  34346  eulerpartlemt  34349  eulerpartgbij  34350  eulerpartlemmf  34353  eulerpartlemgf  34357  eulerpartlemgs2  34358  eulerpartlemn  34359  fib0  34377  fib1  34378  fibp1  34379  ofcs1  34522  signsply0  34529  signsvvf  34557  prodfzo03  34581  repr0  34589  breprexp  34611  hgt750lemd  34626  hgt750lem  34629  hgt750lem2  34630  hgt750leme  34636  tgoldbachgtde  34638  0nn0m1nnn0  35081  f1resfz0f1d  35082  usgrgt2cycl  35098  subfac0  35145  subfacval2  35155  subfaclim  35156  cvmliftlem7  35259  cvmliftlem13  35264  bccolsum  35702  fwddifn0  36128  heiborlem4  37784  heiborlem10  37790  12gcd5e1  41962  60gcd6e6  41963  60gcd7e1  41964  420gcd8e4  41965  12lcm5e60  41967  60lcm7e420  41969  420lcm8e840  41970  lcmineqlem  42011  3exp7  42012  3lexlogpow5ineq1  42013  3lexlogpow5ineq2  42014  3lexlogpow5ineq5  42019  aks4d1p1  42035  aks6d1c2lem4  42086  aks6d1c2  42089  sticksstones11  42115  sticksstones22  42127  aks6d1c7lem1  42139  sqn5i  42282  decpmul  42285  sqdeccom12  42286  sq3deccom12  42287  235t711  42301  ex-decpmul  42302  mhphflem  42566  0prjspn  42598  sum9cubes  42642  nacsfix  42682  diophrw  42729  pell1qr1  42841  monotoddzzfi  42913  jm2.23  42967  hbtlem5  43099  mncn0  43110  aaitgo  43133  brfvrcld  43662  corclrcl  43678  dfrtrcl3  43704  fvrtrcllb0d  43706  fvrtrcllb0da  43707  corcltrcl  43710  cotrclrcl  43713  k0004val0  44125  bccn0  44315  bccn1  44316  binomcxplemradcnv  44324  binomcxplemnotnn0  44328  rexanuz2nf  45467  dvnmul  45920  dvnprodlem3  45925  wallispilem2  46043  wallispi2lem2  46049  stirlinglem5  46055  stirlinglem7  46057  fourierdlem83  46166  fourierdlem112  46195  fouriersw  46208  elaa2lem  46210  elaa2  46211  etransclem48  46259  etransc  46260  iccelpart  47395  fmtno0  47502  fmtnorec2  47505  fmtno5lem1  47515  fmtno5lem2  47516  fmtno5lem4  47518  257prm  47523  fmtnofac2  47531  fmtnofac1  47532  fmtno4prmfac  47534  fmtno4nprmfac193  47536  fmtno5faclem1  47541  fmtno5faclem2  47542  fmtno5faclem3  47543  fmtno5fac  47544  fmtno5nprm  47545  139prmALT  47558  31prm  47559  127prm  47561  m11nprm  47563  bits0ALTV  47641  2exp340mod341  47695  nfermltl2rev  47705  evengpoap3  47761  tgoldbachlt  47778  tgoldbach  47779  stgr0  47920  usgrexmpl1lem  47973  usgrexmpl2lem  47978  gpgprismgr4cycllem6  48047  gpgprismgr4cycllem7  48048  gpgprismgr4cycllem10  48051  nn0mnd  48102  ssnn0ssfz  48272  dig1  48536  0dig2nn0e  48540  0dig2nn0o  48541  0aryfvalel  48562  itcoval0  48590  itcoval1  48591  ackval0  48608  ackval1  48609  ackvalsuc0val  48615  ackval0012  48617  ackval1012  48618  ackval2012  48619  ackval3012  48620  ackval41a  48622