Theorem 0nn0 12433

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 2729	. 2 ⊢ 0 = 0
2		elnn0 12420	. . . 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 2109  0cc0 11044  ℕcn 12162  ℕ₀cn0 12418

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-mulcl 11106  ax-i2m1 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-sn 4586  df-n0 12419

This theorem is referenced by:  0xnn0  12497  nn0ind-raph  12610  10nn0  12643  declei  12661  numlti  12662  nummul1c  12674  decaddc2  12681  decrmanc  12682  decrmac  12683  decaddm10  12684  decaddi  12685  decaddci  12686  decaddci2  12687  decmul1  12689  decmulnc  12692  6p5e11  12698  7p4e11  12701  8p3e11  12706  9p2e11  12712  10p10e20  12720  xnn0n0n1ge2b  13068  0elfz  13561  4fvwrd4  13585  fvinim0ffz  13723  ssnn0fi  13926  fsuppmapnn0fiubex  13933  exple1  14118  nn0opth2  14213  faclbnd4lem3  14236  bc0k  14252  bcn1  14254  bccl  14263  hasheq0  14304  hashrabrsn  14313  hashbc  14394  fi1uzind  14448  brfi1ind  14450  opfi1ind  14453  iswrdi  14458  wrdnfi  14489  s1fv  14551  ccat2s1fst  14580  splfv2a  14697  repsw0  14718  0csh0  14734  cshw1  14763  s2fv0  14829  s3fv0  14833  s4fv0  14837  pfx2  14889  ofs1  14912  relexp0g  14964  relexpaddg  14995  rtrclreclem2  15001  fsumnn0cl  15678  binom  15772  bcxmas  15777  isumnn0nn  15784  climcndslem1  15791  geoser  15809  geomulcvg  15818  risefac0  15969  fallfac0  15970  risefac1  15975  fallfac1  15976  binomfallfaclem2  15982  binomfallfac  15983  bpoly0  15992  bpoly2  15999  bpoly3  16000  bpoly4  16001  fsumcube  16002  ef0lem  16020  ege2le3  16032  ef4p  16057  efgt1p2  16058  efgt1p  16059  ruclem11  16184  nthruz  16197  nn0o  16329  ndvdssub  16355  5ndvds3  16359  bits0  16374  0bits  16385  sadcf  16399  sadc0  16400  sadcaddlem  16403  sadcadd  16404  sadadd2lem  16405  sadadd2  16406  smupf  16424  smup0  16425  smumullem  16438  gcdcl  16452  nn0seqcvgd  16516  algcvg  16522  eucalg  16533  lcmcl  16547  lcmfval  16567  lcmfcl  16574  pclem  16785  pcfac  16846  vdwap0  16923  vdwap1  16924  vdwlem6  16933  hashbc0  16952  0ram  16967  0ramcl  16970  ramz2  16971  ramz  16972  ramcl  16976  prmo0  16983  dec5dvds2  17012  2exp11  17036  2exp16  17037  11prm  17061  37prm  17067  43prm  17068  83prm  17069  139prm  17070  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  4001prm  17091  plendxnocndx  17323  slotsdifdsndx  17333  slotsdifunifndx  17340  odrngstr  17342  slotsdifplendx2  17355  imasvalstr  17390  ipostr  18464  gsumws1  18741  cycsubm  19110  psgnunilem2  19401  psgnunilem3  19402  odfval  19438  oddvdsnn0  19450  pgp0  19502  sylow1lem1  19504  cyggex2  19803  telgsums  19899  srgbinomlem3  20113  srgbinomlem4  20114  srgbinom  20116  cnfldstr  21242  cnfldstrOLD  21257  nn0subm  21315  expmhm  21329  nn0srg  21330  znf1o  21437  zzngim  21438  cygznlem1  21452  cygznlem2a  21453  cygznlem3  21455  cygth  21457  freshmansdream  21460  snifpsrbag  21805  fczpsrbag  21806  psrbagaddcl  21809  psrlidm  21847  mvrf1  21871  mplcoe3  21921  mplcoe5  21923  ltbwe  21927  psrbag0  21945  psrbagsn  21946  evlslem1  21965  mhpsclcl  22010  mhpmulcl  22012  psdmul  22029  psdmvr  22032  00ply1bas  22100  ply1plusgfvi  22102  coe1sclmul  22144  coe1sclmul2  22146  coe1scl  22149  ply1sclid  22150  ply1idvr1OLD  22158  cply1coe0bi  22165  ply1scleq  22168  cpm2mf  22615  m2cpminvid2lem  22617  m2cpminvid2  22618  m2cpmfo  22619  decpmatid  22633  pmatcollpw3  22647  pmatcollpw3fi1lem1  22649  pmatcollpwscmatlem1  22652  pmatcollpwscmatlem2  22653  idpm2idmp  22664  chfacfscmulgsum  22723  chfacfpmmulgsum  22727  cpmadugsumlemF  22739  dscmet  24436  ehl0base  25292  ehl0  25293  itgcnlem  25667  dvn0  25802  dvn1  25804  cpncn  25814  dveflem  25859  c1lip2  25879  deg1le0  25992  ply1divex  26018  mon1pid  26035  ply1rem  26047  fta1g  26051  plyconst  26087  plypf1  26093  plyco  26122  0dgr  26126  0dgrb  26127  coefv0  26129  dgreq0  26147  vieta1lem2  26195  vieta1  26196  aareccl  26210  aannenlem2  26213  taylthlem1  26257  radcnv0  26301  abelthlem6  26322  abelthlem9  26326  logtayl  26545  cxp0  26555  cxpeq  26643  leibpilem2  26827  leibpi  26828  log2ublem3  26834  log2ub  26835  log2le1  26836  divsqrtsumlem  26866  dmgmn0  26912  lgambdd  26923  sqff1o  27068  ppiublem2  27090  chtublem  27098  bclbnd  27167  bposlem8  27178  lgsval  27188  dchrisum0flblem1  27395  dchrisum0flb  27397  ostth2lem2  27521  usgrexmplef  29162  usgr0edg0rusgr  29479  usgr2pthlem  29666  wwlksn0s  29764  rusgrnumwwlkb0  29874  erclwwlkref  29922  clwwlkf1  29951  0wlkonlem1  30020  upgr4cycl4dv4e  30087  1kp2ke3k  30348  ex-fac  30353  ex-prmo  30361  nn0min  32718  dpmul1000  32792  dp0h  32795  dpexpp1  32801  dpmul4  32807  threehalves  32808  1mhdrd  32809  s1f1  32837  s2f1  32839  cshw1s2  32855  cycpm2tr  33049  deg1le0eq0  33515  ply1unit  33517  evl1deg1  33518  evl1deg2  33519  evl1deg3  33520  ply1dg1rt  33521  m1pmeq  33525  minplyirredlem  33673  rtelextdg2lem  33689  fldext2chn  33691  constraddcl  33725  constrnegcl  33726  constrdircl  33728  constrremulcl  33730  2sqr3minply  33743  lmatcl  33779  lmat22e12  33782  lmat22e21  33783  fsumcvg4  33913  oddpwdc  34318  eulerpartlems  34324  eulerpartlemb  34332  eulerpartlemt  34335  eulerpartgbij  34336  eulerpartlemmf  34339  eulerpartlemgf  34343  eulerpartlemgs2  34344  eulerpartlemn  34345  fib0  34363  fib1  34364  fibp1  34365  ofcs1  34508  signsply0  34515  signsvvf  34543  prodfzo03  34567  repr0  34575  breprexp  34597  hgt750lemd  34612  hgt750lem  34615  hgt750lem2  34616  hgt750leme  34622  tgoldbachgtde  34624  0nn0m1nnn0  35073  f1resfz0f1d  35074  usgrgt2cycl  35090  subfac0  35137  subfacval2  35147  subfaclim  35148  cvmliftlem7  35251  cvmliftlem13  35256  bccolsum  35699  fwddifn0  36125  heiborlem4  37781  heiborlem10  37787  12gcd5e1  41964  60gcd6e6  41965  60gcd7e1  41966  420gcd8e4  41967  12lcm5e60  41969  60lcm7e420  41971  420lcm8e840  41972  lcmineqlem  42013  3exp7  42014  3lexlogpow5ineq1  42015  3lexlogpow5ineq2  42016  3lexlogpow5ineq5  42021  aks4d1p1  42037  aks6d1c2lem4  42088  aks6d1c2  42091  sticksstones11  42117  sticksstones22  42129  aks6d1c7lem1  42141  sqn5i  42246  decpmul  42249  sqdeccom12  42250  sq3deccom12  42251  235t711  42266  ex-decpmul  42267  mhphflem  42557  0prjspn  42589  sum9cubes  42633  nacsfix  42673  diophrw  42720  pell1qr1  42832  monotoddzzfi  42904  jm2.23  42958  hbtlem5  43090  mncn0  43101  aaitgo  43124  brfvrcld  43653  corclrcl  43669  dfrtrcl3  43695  fvrtrcllb0d  43697  fvrtrcllb0da  43698  corcltrcl  43701  cotrclrcl  43704  k0004val0  44116  bccn0  44305  bccn1  44306  binomcxplemradcnv  44314  binomcxplemnotnn0  44318  rexanuz2nf  45461  dvnmul  45914  dvnprodlem3  45919  wallispilem2  46037  wallispi2lem2  46043  stirlinglem5  46049  stirlinglem7  46051  fourierdlem83  46160  fourierdlem112  46189  fouriersw  46202  elaa2lem  46204  elaa2  46205  etransclem48  46253  etransc  46254  iccelpart  47407  fmtno0  47514  fmtnorec2  47517  fmtno5lem1  47527  fmtno5lem2  47528  fmtno5lem4  47530  257prm  47535  fmtnofac2  47543  fmtnofac1  47544  fmtno4prmfac  47546  fmtno4nprmfac193  47548  fmtno5faclem1  47553  fmtno5faclem2  47554  fmtno5faclem3  47555  fmtno5fac  47556  fmtno5nprm  47557  139prmALT  47570  31prm  47571  127prm  47573  m11nprm  47575  bits0ALTV  47653  2exp340mod341  47707  nfermltl2rev  47717  evengpoap3  47773  tgoldbachlt  47790  tgoldbach  47791  stgr0  47932  usgrexmpl1lem  47985  usgrexmpl2lem  47990  gpgprismgr4cycllem6  48063  gpgprismgr4cycllem7  48064  gpgprismgr4cycllem10  48067  nn0mnd  48140  ssnn0ssfz  48310  dig1  48570  0dig2nn0e  48574  0dig2nn0o  48575  0aryfvalel  48596  itcoval0  48624  itcoval1  48625  ackval0  48642  ackval1  48643  ackvalsuc0val  48649  ackval0012  48651  ackval1012  48652  ackval2012  48653  ackval3012  48654  ackval41a  48656