Theorem 0nn0 12541

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

Syntax hints:   ∨ wo 848   = wceq 1540   ∈ wcel 2108  0cc0 11155  ℕcn 12266  ℕ₀cn0 12526

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 2708  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-i2m1 11223

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-n0 12527

This theorem is referenced by:  0xnn0  12605  nn0ind-raph  12718  10nn0  12751  declei  12769  numlti  12770  nummul1c  12782  decaddc2  12789  decrmanc  12790  decrmac  12791  decaddm10  12792  decaddi  12793  decaddci  12794  decaddci2  12795  decmul1  12797  decmulnc  12800  6p5e11  12806  7p4e11  12809  8p3e11  12814  9p2e11  12820  10p10e20  12828  xnn0n0n1ge2b  13174  0elfz  13664  4fvwrd4  13688  fvinim0ffz  13825  ssnn0fi  14026  fsuppmapnn0fiubex  14033  exple1  14216  nn0opth2  14311  faclbnd4lem3  14334  bc0k  14350  bcn1  14352  bccl  14361  hasheq0  14402  hashrabrsn  14411  hashbc  14492  fi1uzind  14546  brfi1ind  14548  opfi1ind  14551  iswrdi  14556  wrdnfi  14586  s1fv  14648  ccat2s1fst  14677  splfv2a  14794  repsw0  14815  0csh0  14831  cshw1  14860  s2fv0  14926  s3fv0  14930  s4fv0  14934  pfx2  14986  ofs1  15009  relexp0g  15061  relexpaddg  15092  rtrclreclem2  15098  fsumnn0cl  15772  binom  15866  bcxmas  15871  isumnn0nn  15878  climcndslem1  15885  geoser  15903  geomulcvg  15912  risefac0  16063  fallfac0  16064  risefac1  16069  fallfac1  16070  binomfallfaclem2  16076  binomfallfac  16077  bpoly0  16086  bpoly2  16093  bpoly3  16094  bpoly4  16095  fsumcube  16096  ef0lem  16114  ege2le3  16126  ef4p  16149  efgt1p2  16150  efgt1p  16151  ruclem11  16276  nthruz  16289  nn0o  16420  ndvdssub  16446  5ndvds3  16450  bits0  16465  0bits  16476  sadcf  16490  sadc0  16491  sadcaddlem  16494  sadcadd  16495  sadadd2lem  16496  sadadd2  16497  smupf  16515  smup0  16516  smumullem  16529  gcdcl  16543  nn0seqcvgd  16607  algcvg  16613  eucalg  16624  lcmcl  16638  lcmfval  16658  lcmfcl  16665  pclem  16876  pcfac  16937  vdwap0  17014  vdwap1  17015  vdwlem6  17024  hashbc0  17043  0ram  17058  0ramcl  17061  ramz2  17062  ramz  17063  ramcl  17067  prmo0  17074  dec5dvds2  17103  2exp11  17127  2exp16  17128  11prm  17152  37prm  17158  43prm  17159  83prm  17160  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  4001prm  17182  plendxnocndx  17428  slotsdifdsndx  17438  slotsdifunifndx  17445  odrngstr  17447  slotsdifplendx2  17461  imasvalstr  17496  ipostr  18574  gsumws1  18851  cycsubm  19220  psgnunilem2  19513  psgnunilem3  19514  odfval  19550  oddvdsnn0  19562  pgp0  19614  sylow1lem1  19616  cyggex2  19915  telgsums  20011  srgbinomlem3  20225  srgbinomlem4  20226  srgbinom  20228  cnfldstr  21366  cnfldstrOLD  21381  cnfldfunALTOLDOLD  21393  nn0subm  21440  expmhm  21454  nn0srg  21455  znf1o  21570  zzngim  21571  cygznlem1  21585  cygznlem2a  21586  cygznlem3  21588  cygth  21590  freshmansdream  21593  thlleOLD  21717  snifpsrbag  21940  fczpsrbag  21941  psrbagaddcl  21944  psrlidm  21982  mvrf1  22006  mplcoe3  22056  mplcoe5  22058  ltbwe  22062  psrbag0  22086  psrbagsn  22087  evlslem1  22106  mhpsclcl  22151  mhpmulcl  22153  psdmul  22170  psdmvr  22173  00ply1bas  22241  ply1plusgfvi  22243  coe1sclmul  22285  coe1sclmul2  22287  coe1scl  22290  ply1sclid  22291  ply1idvr1OLD  22299  cply1coe0bi  22306  ply1scleq  22309  cpm2mf  22758  m2cpminvid2lem  22760  m2cpminvid2  22761  m2cpmfo  22762  decpmatid  22776  pmatcollpw3  22790  pmatcollpw3fi1lem1  22792  pmatcollpwscmatlem1  22795  pmatcollpwscmatlem2  22796  idpm2idmp  22807  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  cpmadugsumlemF  22882  dscmet  24585  ehl0base  25450  ehl0  25451  itgcnlem  25825  dvn0  25960  dvn1  25962  cpncn  25972  dveflem  26017  c1lip2  26037  deg1le0  26150  ply1divex  26176  mon1pid  26193  ply1rem  26205  fta1g  26209  plyconst  26245  plypf1  26251  plyco  26280  0dgr  26284  0dgrb  26285  coefv0  26287  dgreq0  26305  vieta1lem2  26353  vieta1  26354  aareccl  26368  aannenlem2  26371  taylthlem1  26415  radcnv0  26459  abelthlem6  26480  abelthlem9  26484  logtayl  26702  cxp0  26712  cxpeq  26800  leibpilem2  26984  leibpi  26985  log2ublem3  26991  log2ub  26992  log2le1  26993  divsqrtsumlem  27023  dmgmn0  27069  lgambdd  27080  sqff1o  27225  ppiublem2  27247  chtublem  27255  bclbnd  27324  bposlem8  27335  lgsval  27345  dchrisum0flblem1  27552  dchrisum0flb  27554  ostth2lem2  27678  usgrexmplef  29276  usgr0edg0rusgr  29593  usgr2pthlem  29783  wwlksn0s  29881  rusgrnumwwlkb0  29991  erclwwlkref  30039  clwwlkf1  30068  0wlkonlem1  30137  upgr4cycl4dv4e  30204  1kp2ke3k  30465  ex-fac  30470  ex-prmo  30478  nn0min  32822  dpmul1000  32881  dp0h  32884  dpexpp1  32890  dpmul4  32896  threehalves  32897  1mhdrd  32898  s1f1  32927  s2f1  32929  cshw1s2  32945  cycpm2tr  33139  deg1le0eq0  33598  ply1unit  33600  evl1deg1  33601  evl1deg2  33602  evl1deg3  33603  ply1dg1rt  33604  m1pmeq  33608  minplyirredlem  33753  rtelextdg2lem  33767  fldext2chn  33769  2sqr3minply  33791  lmatcl  33815  lmat22e12  33818  lmat22e21  33819  fsumcvg4  33949  oddpwdc  34356  eulerpartlems  34362  eulerpartlemb  34370  eulerpartlemt  34373  eulerpartgbij  34374  eulerpartlemmf  34377  eulerpartlemgf  34381  eulerpartlemgs2  34382  eulerpartlemn  34383  fib0  34401  fib1  34402  fibp1  34403  ofcs1  34559  signsply0  34566  signsvvf  34594  prodfzo03  34618  repr0  34626  breprexp  34648  hgt750lemd  34663  hgt750lem  34666  hgt750lem2  34667  hgt750leme  34673  tgoldbachgtde  34675  0nn0m1nnn0  35118  f1resfz0f1d  35119  usgrgt2cycl  35135  subfac0  35182  subfacval2  35192  subfaclim  35193  cvmliftlem7  35296  cvmliftlem13  35301  bccolsum  35739  fwddifn0  36165  heiborlem4  37821  heiborlem10  37827  12gcd5e1  42004  60gcd6e6  42005  60gcd7e1  42006  420gcd8e4  42007  12lcm5e60  42009  60lcm7e420  42011  420lcm8e840  42012  lcmineqlem  42053  3exp7  42054  3lexlogpow5ineq1  42055  3lexlogpow5ineq2  42056  3lexlogpow5ineq5  42061  aks4d1p1  42077  aks6d1c2lem4  42128  aks6d1c2  42131  sticksstones11  42157  sticksstones22  42169  aks6d1c7lem1  42181  sqn5i  42320  decpmul  42323  sqdeccom12  42324  sq3deccom12  42325  235t711  42339  ex-decpmul  42340  mhphflem  42606  0prjspn  42638  sum9cubes  42682  nacsfix  42723  diophrw  42770  pell1qr1  42882  monotoddzzfi  42954  jm2.23  43008  hbtlem5  43140  mncn0  43151  aaitgo  43174  brfvrcld  43704  corclrcl  43720  dfrtrcl3  43746  fvrtrcllb0d  43748  fvrtrcllb0da  43749  corcltrcl  43752  cotrclrcl  43755  k0004val0  44167  bccn0  44362  bccn1  44363  binomcxplemradcnv  44371  binomcxplemnotnn0  44375  rexanuz2nf  45503  dvnmul  45958  dvnprodlem3  45963  wallispilem2  46081  wallispi2lem2  46087  stirlinglem5  46093  stirlinglem7  46095  fourierdlem83  46204  fourierdlem112  46233  fouriersw  46246  elaa2lem  46248  elaa2  46249  etransclem48  46297  etransc  46298  iccelpart  47420  fmtno0  47527  fmtnorec2  47530  fmtno5lem1  47540  fmtno5lem2  47541  fmtno5lem4  47543  257prm  47548  fmtnofac2  47556  fmtnofac1  47557  fmtno4prmfac  47559  fmtno4nprmfac193  47561  fmtno5faclem1  47566  fmtno5faclem2  47567  fmtno5faclem3  47568  fmtno5fac  47569  fmtno5nprm  47570  139prmALT  47583  31prm  47584  127prm  47586  m11nprm  47588  bits0ALTV  47666  2exp340mod341  47720  nfermltl2rev  47730  evengpoap3  47786  tgoldbachlt  47803  tgoldbach  47804  stgr0  47927  usgrexmpl1lem  47980  usgrexmpl2lem  47985  nn0mnd  48095  ssnn0ssfz  48265  dig1  48529  0dig2nn0e  48533  0dig2nn0o  48534  0aryfvalel  48555  itcoval0  48583  itcoval1  48584  ackval0  48601  ackval1  48602  ackvalsuc0val  48608  ackval0012  48610  ackval1012  48611  ackval2012  48612  ackval3012  48613  ackval41a  48615  prstclevalOLD  49158