Theorem 0nn0 12487

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 12474	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 227	. . 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 1542   ∈ wcel 2107  0cc0 11110  ℕcn 12212  ℕ₀cn0 12472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-mulcl 11172  ax-i2m1 11178

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-sn 4630  df-n0 12473

This theorem is referenced by:  0xnn0  12550  nn0ind-raph  12662  10nn0  12695  declei  12713  numlti  12714  nummul1c  12726  decaddc2  12733  decrmanc  12734  decrmac  12735  decaddm10  12736  decaddi  12737  decaddci  12738  decaddci2  12739  decmul1  12741  decmulnc  12744  6p5e11  12750  7p4e11  12753  8p3e11  12758  9p2e11  12764  10p10e20  12772  xnn0n0n1ge2b  13111  0elfz  13598  4fvwrd4  13621  fvinim0ffz  13751  ssnn0fi  13950  fsuppmapnn0fiubex  13957  exple1  14141  nn0opth2  14232  faclbnd4lem3  14255  bc0k  14271  bcn1  14273  bccl  14282  hasheq0  14323  hashrabrsn  14332  hashbc  14412  fi1uzind  14458  brfi1ind  14460  opfi1ind  14463  iswrdi  14468  wrdnfi  14498  s1fv  14560  ccat2s1fst  14589  splfv2a  14706  repsw0  14727  0csh0  14743  cshw1  14772  s2fv0  14838  s3fv0  14842  s4fv0  14846  pfx2  14898  ofs1  14917  relexp0g  14969  relexpaddg  15000  rtrclreclem2  15006  fsumnn0cl  15682  binom  15776  bcxmas  15781  isumnn0nn  15788  climcndslem1  15795  geoser  15813  geomulcvg  15822  risefac0  15971  fallfac0  15972  risefac1  15977  fallfac1  15978  binomfallfaclem2  15984  binomfallfac  15985  bpoly0  15994  bpoly2  16001  bpoly3  16002  bpoly4  16003  fsumcube  16004  ef0lem  16022  ege2le3  16033  ef4p  16056  efgt1p2  16057  efgt1p  16058  ruclem11  16183  nthruz  16196  nn0o  16326  ndvdssub  16352  bits0  16369  0bits  16380  sadcf  16394  sadc0  16395  sadcaddlem  16398  sadcadd  16399  sadadd2lem  16400  sadadd2  16401  smupf  16419  smup0  16420  smumullem  16433  gcdcl  16447  nn0seqcvgd  16507  algcvg  16513  eucalg  16524  lcmcl  16538  lcmfval  16558  lcmfcl  16565  pclem  16771  pcfac  16832  vdwap0  16909  vdwap1  16910  vdwlem6  16919  hashbc0  16938  0ram  16953  0ramcl  16956  ramz2  16957  ramz  16958  ramcl  16962  prmo0  16969  dec5dvds2  16998  2exp11  17023  2exp16  17024  11prm  17048  37prm  17054  43prm  17055  83prm  17056  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  4001prm  17078  plendxnocndx  17329  slotsdifdsndx  17339  slotsdifunifndx  17346  odrngstr  17348  slotsdifplendx2  17362  imasvalstr  17397  ipostr  18482  gsumws1  18719  cycsubm  19079  psgnunilem2  19363  psgnunilem3  19364  odfval  19400  oddvdsnn0  19412  pgp0  19464  sylow1lem1  19466  cyggex2  19765  telgsums  19861  srgbinomlem3  20051  srgbinomlem4  20052  srgbinom  20054  cnfldstr  20946  cnfldfunALTOLD  20958  nn0subm  21000  expmhm  21014  nn0srg  21015  znf1o  21107  zzngim  21108  cygznlem1  21122  cygznlem2a  21123  cygznlem3  21125  cygth  21127  thlleOLD  21252  snifpsrbag  21475  fczpsrbag  21476  psrbagaddcl  21481  psrlidm  21523  mvrf1  21545  mplcoe3  21593  mplcoe5  21595  ltbwe  21599  psrbag0  21623  psrbagsn  21624  evlslem1  21645  mhpsclcl  21690  mhpmulcl  21692  00ply1bas  21762  ply1plusgfvi  21764  coe1sclmul  21804  coe1sclmul2  21806  coe1scl  21809  ply1sclid  21810  ply1idvr1  21817  cply1coe0bi  21824  cpm2mf  22254  m2cpminvid2lem  22256  m2cpminvid2  22257  m2cpmfo  22258  decpmatid  22272  pmatcollpw3  22286  pmatcollpw3fi1lem1  22288  pmatcollpwscmatlem1  22291  pmatcollpwscmatlem2  22292  idpm2idmp  22303  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  cpmadugsumlemF  22378  dscmet  24081  ehl0base  24933  ehl0  24934  itgcnlem  25307  dvn0  25441  dvn1  25443  cpncn  25453  dveflem  25496  c1lip2  25515  tdeglem4OLD  25578  deg1le0  25629  ply1divex  25654  ply1rem  25681  fta1g  25685  plyconst  25720  plypf1  25726  plyco  25755  0dgr  25759  0dgrb  25760  coefv0  25762  dgreq0  25779  vieta1lem2  25824  vieta1  25825  aareccl  25839  aannenlem2  25842  taylthlem1  25885  radcnv0  25928  abelthlem6  25948  abelthlem9  25952  logtayl  26168  cxp0  26178  cxpeq  26265  leibpilem2  26446  leibpi  26447  log2ublem3  26453  log2ub  26454  log2le1  26455  divsqrtsumlem  26484  dmgmn0  26530  lgambdd  26541  sqff1o  26686  ppiublem2  26706  chtublem  26714  bclbnd  26783  bposlem8  26794  lgsval  26804  dchrisum0flblem1  27011  dchrisum0flb  27013  ostth2lem2  27137  usgrexmplef  28516  usgr0edg0rusgr  28832  usgr2pthlem  29020  wwlksn0s  29115  rusgrnumwwlkb0  29225  erclwwlkref  29273  clwwlkf1  29302  0wlkonlem1  29371  upgr4cycl4dv4e  29438  1kp2ke3k  29699  ex-fac  29704  ex-prmo  29712  nn0min  32026  dpmul1000  32065  dp0h  32068  dpexpp1  32074  dpmul4  32080  threehalves  32081  1mhdrd  32082  s1f1  32109  s2f1  32111  cshw1s2  32124  cycpm2tr  32278  freshmansdream  32381  ply1scleq  32639  deg1le0eq0  32655  minplyirredlem  32769  lmatcl  32796  lmat22e12  32799  lmat22e21  32800  fsumcvg4  32930  oddpwdc  33353  eulerpartlems  33359  eulerpartlemb  33367  eulerpartlemt  33370  eulerpartgbij  33371  eulerpartlemmf  33374  eulerpartlemgf  33378  eulerpartlemgs2  33379  eulerpartlemn  33380  fib0  33398  fib1  33399  fibp1  33400  ofcs1  33555  signsply0  33562  signsvvf  33590  prodfzo03  33615  repr0  33623  breprexp  33645  hgt750lemd  33660  hgt750lem  33663  hgt750lem2  33664  hgt750leme  33670  tgoldbachgtde  33672  0nn0m1nnn0  34102  f1resfz0f1d  34103  usgrgt2cycl  34121  subfac0  34168  subfacval2  34178  subfaclim  34179  cvmliftlem7  34282  cvmliftlem13  34287  bccolsum  34709  fwddifn0  35136  heiborlem4  36682  heiborlem10  36688  12gcd5e1  40868  60gcd6e6  40869  60gcd7e1  40870  420gcd8e4  40871  12lcm5e60  40873  60lcm7e420  40875  420lcm8e840  40876  lcmineqlem  40917  3exp7  40918  3lexlogpow5ineq1  40919  3lexlogpow5ineq2  40920  3lexlogpow5ineq5  40925  aks4d1p1  40941  sticksstones11  40972  sticksstones22  40984  mhphflem  41168  sqn5i  41197  decpmul  41200  sqdeccom12  41201  sq3deccom12  41202  235t711  41205  ex-decpmul  41206  0prjspn  41370  sum9cubes  41414  nacsfix  41450  diophrw  41497  pell1qr1  41609  monotoddzzfi  41681  jm2.23  41735  hbtlem5  41870  mncn0  41881  aaitgo  41904  mon1pid  41947  brfvrcld  42442  corclrcl  42458  dfrtrcl3  42484  fvrtrcllb0d  42486  fvrtrcllb0da  42487  corcltrcl  42490  cotrclrcl  42493  k0004val0  42905  bccn0  43102  bccn1  43103  binomcxplemradcnv  43111  binomcxplemnotnn0  43115  rexanuz2nf  44203  dvnmul  44659  dvnprodlem3  44664  wallispilem2  44782  wallispi2lem2  44788  stirlinglem5  44794  stirlinglem7  44796  fourierdlem83  44905  fourierdlem112  44934  fouriersw  44947  elaa2lem  44949  elaa2  44950  etransclem48  44998  etransc  44999  iccelpart  46101  fmtno0  46208  fmtnorec2  46211  fmtno5lem1  46221  fmtno5lem2  46222  fmtno5lem4  46224  257prm  46229  fmtnofac2  46237  fmtnofac1  46238  fmtno4prmfac  46240  fmtno4nprmfac193  46242  fmtno5faclem1  46247  fmtno5faclem2  46248  fmtno5faclem3  46249  fmtno5fac  46250  fmtno5nprm  46251  139prmALT  46264  31prm  46265  127prm  46267  m11nprm  46269  bits0ALTV  46347  2exp340mod341  46401  nfermltl2rev  46411  evengpoap3  46467  tgoldbachlt  46484  tgoldbach  46485  nn0mnd  46589  ssnn0ssfz  47025  dig1  47294  0dig2nn0e  47298  0dig2nn0o  47299  0aryfvalel  47320  itcoval0  47348  itcoval1  47349  ackval0  47366  ackval1  47367  ackvalsuc0val  47373  ackval0012  47375  ackval1012  47376  ackval2012  47377  ackval3012  47378  ackval41a  47380  prstclevalOLD  47689