Theorem 0nn0 12420

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 12407	. . . 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 1542   ∈ wcel 2114  0cc0 11030  ℕcn 12149  ℕ₀cn0 12405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-mulcl 11092  ax-i2m1 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-un 3907  df-sn 4582  df-n0 12406

This theorem is referenced by:  0xnn0  12484  nn0ind-raph  12596  10nn0  12629  declei  12647  numlti  12648  nummul1c  12660  decaddc2  12667  decrmanc  12668  decrmac  12669  decaddm10  12670  decaddi  12671  decaddci  12672  decaddci2  12673  decmul1  12675  decmulnc  12678  6p5e11  12684  7p4e11  12687  8p3e11  12692  9p2e11  12698  10p10e20  12706  xnn0n0n1ge2b  13050  0elfz  13544  4fvwrd4  13568  fvinim0ffz  13709  ssnn0fi  13912  fsuppmapnn0fiubex  13919  exple1  14104  nn0opth2  14199  faclbnd4lem3  14222  bc0k  14238  bcn1  14240  bccl  14249  hasheq0  14290  hashrabrsn  14299  hashbc  14380  fi1uzind  14434  brfi1ind  14436  opfi1ind  14439  iswrdi  14444  wrdnfi  14475  s1fv  14538  ccat2s1fst  14567  splfv2a  14683  repsw0  14704  0csh0  14720  cshw1  14749  s2fv0  14814  s3fv0  14818  s4fv0  14822  pfx2  14874  ofs1  14897  relexp0g  14949  relexpaddg  14980  rtrclreclem2  14986  fsumnn0cl  15663  binom  15757  bcxmas  15762  isumnn0nn  15769  climcndslem1  15776  geoser  15794  geomulcvg  15803  risefac0  15954  fallfac0  15955  risefac1  15960  fallfac1  15961  binomfallfaclem2  15967  binomfallfac  15968  bpoly0  15977  bpoly2  15984  bpoly3  15985  bpoly4  15986  fsumcube  15987  ef0lem  16005  ege2le3  16017  ef4p  16042  efgt1p2  16043  efgt1p  16044  ruclem11  16169  nthruz  16182  nn0o  16314  ndvdssub  16340  5ndvds3  16344  bits0  16359  0bits  16370  sadcf  16384  sadc0  16385  sadcaddlem  16388  sadcadd  16389  sadadd2lem  16390  sadadd2  16391  smupf  16409  smup0  16410  smumullem  16423  gcdcl  16437  nn0seqcvgd  16501  algcvg  16507  eucalg  16518  lcmcl  16532  lcmfval  16552  lcmfcl  16559  pclem  16770  pcfac  16831  vdwap0  16908  vdwap1  16909  vdwlem6  16918  hashbc0  16937  0ram  16952  0ramcl  16955  ramz2  16956  ramz  16957  ramcl  16961  prmo0  16968  dec5dvds2  16997  2exp11  17021  2exp16  17022  11prm  17046  37prm  17052  43prm  17053  83prm  17054  139prm  17055  163prm  17056  317prm  17057  631prm  17058  1259lem1  17062  1259lem2  17063  1259lem3  17064  1259lem4  17065  1259lem5  17066  2503lem1  17068  2503lem2  17069  2503lem3  17070  2503prm  17071  4001lem1  17072  4001lem2  17073  4001lem3  17074  4001lem4  17075  4001prm  17076  plendxnocndx  17308  slotsdifdsndx  17318  slotsdifunifndx  17325  odrngstr  17327  slotsdifplendx2  17340  imasvalstr  17375  ipostr  18456  gsumws1  18767  cycsubm  19135  psgnunilem2  19428  psgnunilem3  19429  odfval  19465  oddvdsnn0  19477  pgp0  19529  sylow1lem1  19531  cyggex2  19830  telgsums  19926  srgbinomlem3  20167  srgbinomlem4  20168  srgbinom  20170  cnfldstr  21315  cnfldstrOLD  21330  nn0subm  21381  expmhm  21395  nn0srg  21396  znf1o  21510  zzngim  21511  cygznlem1  21525  cygznlem2a  21526  cygznlem3  21528  cygth  21530  freshmansdream  21533  snifpsrbag  21880  fczpsrbag  21881  psrbagaddcl  21884  psrlidm  21921  mvrf1  21945  mplcoe3  21997  mplcoe5  21999  ltbwe  22003  psrbag0  22021  psrbagsn  22022  evlslem1  22041  mhpsclcl  22094  mhpmulcl  22096  psdmul  22113  psdmvr  22116  00ply1bas  22184  ply1plusgfvi  22186  coe1sclmul  22228  coe1sclmul2  22230  coe1scl  22233  ply1sclid  22234  ply1idvr1OLD  22243  cply1coe0bi  22250  ply1scleq  22253  cpm2mf  22700  m2cpminvid2lem  22702  m2cpminvid2  22703  m2cpmfo  22704  decpmatid  22718  pmatcollpw3  22732  pmatcollpw3fi1lem1  22734  pmatcollpwscmatlem1  22737  pmatcollpwscmatlem2  22738  idpm2idmp  22749  chfacfscmulgsum  22808  chfacfpmmulgsum  22812  cpmadugsumlemF  22824  dscmet  24520  ehl0base  25376  ehl0  25377  itgcnlem  25751  dvn0  25886  dvn1  25888  cpncn  25898  dveflem  25943  c1lip2  25963  deg1le0  26076  ply1divex  26102  mon1pid  26119  ply1rem  26131  fta1g  26135  plyconst  26171  plypf1  26177  plyco  26206  0dgr  26210  0dgrb  26211  coefv0  26213  dgreq0  26231  vieta1lem2  26279  vieta1  26280  aareccl  26294  aannenlem2  26297  taylthlem1  26341  radcnv0  26385  abelthlem6  26406  abelthlem9  26410  logtayl  26629  cxp0  26639  cxpeq  26727  leibpilem2  26911  leibpi  26912  log2ublem3  26918  log2ub  26919  log2le1  26920  divsqrtsumlem  26950  dmgmn0  26996  lgambdd  27007  sqff1o  27152  ppiublem2  27174  chtublem  27182  bclbnd  27251  bposlem8  27262  lgsval  27272  dchrisum0flblem1  27479  dchrisum0flb  27481  ostth2lem2  27605  usgrexmplef  29315  usgr0edg0rusgr  29632  usgr2pthlem  29819  wwlksn0s  29917  rusgrnumwwlkb0  30030  erclwwlkref  30078  clwwlkf1  30107  0wlkonlem1  30176  upgr4cycl4dv4e  30243  1kp2ke3k  30504  ex-fac  30509  ex-prmo  30517  nn0min  32882  dpmul1000  32961  dp0h  32964  dpexpp1  32970  dpmul4  32976  threehalves  32977  1mhdrd  32978  s1f1  33006  s2f1  33008  cshw1s2  33023  cycpm2tr  33182  deg1le0eq0  33635  ply1unit  33637  evl1deg1  33638  evl1deg2  33639  evl1deg3  33640  ply1dg1rt  33642  m1pmeq  33647  psrbasfsupp  33674  mplmulmvr  33685  evlextv  33688  mplvrpmlem  33689  mplvrpmfgalem  33690  mplvrpmga  33691  mplvrpmmhm  33692  mplvrpmrhm  33693  esplyfval0  33703  esplylem  33705  esplyfv1  33708  esplyind  33712  vietalem  33716  vieta  33717  minplyirredlem  33848  rtelextdg2lem  33864  fldext2chn  33866  constraddcl  33900  constrnegcl  33901  constrdircl  33903  constrremulcl  33905  2sqr3minply  33918  lmatcl  33954  lmat22e12  33957  lmat22e21  33958  fsumcvg4  34088  oddpwdc  34492  eulerpartlems  34498  eulerpartlemb  34506  eulerpartlemt  34509  eulerpartgbij  34510  eulerpartlemmf  34513  eulerpartlemgf  34517  eulerpartlemgs2  34518  eulerpartlemn  34519  fib0  34537  fib1  34538  fibp1  34539  ofcs1  34682  signsply0  34689  signsvvf  34717  prodfzo03  34741  repr0  34749  breprexp  34771  hgt750lemd  34786  hgt750lem  34789  hgt750lem2  34790  hgt750leme  34796  tgoldbachgtde  34798  0nn0m1nnn0  35288  f1resfz0f1d  35289  usgrgt2cycl  35305  subfac0  35352  subfacval2  35362  subfaclim  35363  cvmliftlem7  35466  cvmliftlem13  35471  bccolsum  35914  fwddifn0  36339  heiborlem4  37986  heiborlem10  37992  12gcd5e1  42294  60gcd6e6  42295  60gcd7e1  42296  420gcd8e4  42297  12lcm5e60  42299  60lcm7e420  42301  420lcm8e840  42302  lcmineqlem  42343  3exp7  42344  3lexlogpow5ineq1  42345  3lexlogpow5ineq2  42346  3lexlogpow5ineq5  42351  aks4d1p1  42367  aks6d1c2lem4  42418  aks6d1c2  42421  sticksstones11  42447  sticksstones22  42459  aks6d1c7lem1  42471  sqn5i  42576  decpmul  42579  sqdeccom12  42580  sq3deccom12  42581  235t711  42596  ex-decpmul  42597  mhphflem  42875  0prjspn  42907  sum9cubes  42951  nacsfix  42990  diophrw  43037  pell1qr1  43149  monotoddzzfi  43220  jm2.23  43274  hbtlem5  43406  mncn0  43417  aaitgo  43440  brfvrcld  43968  corclrcl  43984  dfrtrcl3  44010  fvrtrcllb0d  44012  fvrtrcllb0da  44013  corcltrcl  44016  cotrclrcl  44019  k0004val0  44431  bccn0  44620  bccn1  44621  binomcxplemradcnv  44629  binomcxplemnotnn0  44633  rexanuz2nf  45772  dvnmul  46223  dvnprodlem3  46228  wallispilem2  46346  wallispi2lem2  46352  stirlinglem5  46358  stirlinglem7  46360  fourierdlem83  46469  fourierdlem112  46498  fouriersw  46511  elaa2lem  46513  elaa2  46514  etransclem48  46562  etransc  46563  iccelpart  47715  fmtno0  47822  fmtnorec2  47825  fmtno5lem1  47835  fmtno5lem2  47836  fmtno5lem4  47838  257prm  47843  fmtnofac2  47851  fmtnofac1  47852  fmtno4prmfac  47854  fmtno4nprmfac193  47856  fmtno5faclem1  47861  fmtno5faclem2  47862  fmtno5faclem3  47863  fmtno5fac  47864  fmtno5nprm  47865  139prmALT  47878  31prm  47879  127prm  47881  m11nprm  47883  bits0ALTV  47961  2exp340mod341  48015  nfermltl2rev  48025  evengpoap3  48081  tgoldbachlt  48098  tgoldbach  48099  stgr0  48242  usgrexmpl1lem  48303  usgrexmpl2lem  48308  gpgprismgr4cycllem6  48382  gpgprismgr4cycllem7  48383  gpgprismgr4cycllem10  48386  nn0mnd  48461  ssnn0ssfz  48631  dig1  48890  0dig2nn0e  48894  0dig2nn0o  48895  0aryfvalel  48916  itcoval0  48944  itcoval1  48945  ackval0  48962  ackval1  48963  ackvalsuc0val  48969  ackval0012  48971  ackval1012  48972  ackval2012  48973  ackval3012  48974  ackval41a  48976