Theorem 0nn0 12464

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 2730	. 2 ⊢ 0 = 0
2		elnn0 12451	. . . 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 11075  ℕcn 12193  ℕ₀cn0 12449

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 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-i2m1 11143

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-n0 12450

This theorem is referenced by:  0xnn0  12528  nn0ind-raph  12641  10nn0  12674  declei  12692  numlti  12693  nummul1c  12705  decaddc2  12712  decrmanc  12713  decrmac  12714  decaddm10  12715  decaddi  12716  decaddci  12717  decaddci2  12718  decmul1  12720  decmulnc  12723  6p5e11  12729  7p4e11  12732  8p3e11  12737  9p2e11  12743  10p10e20  12751  xnn0n0n1ge2b  13099  0elfz  13592  4fvwrd4  13616  fvinim0ffz  13754  ssnn0fi  13957  fsuppmapnn0fiubex  13964  exple1  14149  nn0opth2  14244  faclbnd4lem3  14267  bc0k  14283  bcn1  14285  bccl  14294  hasheq0  14335  hashrabrsn  14344  hashbc  14425  fi1uzind  14479  brfi1ind  14481  opfi1ind  14484  iswrdi  14489  wrdnfi  14520  s1fv  14582  ccat2s1fst  14611  splfv2a  14728  repsw0  14749  0csh0  14765  cshw1  14794  s2fv0  14860  s3fv0  14864  s4fv0  14868  pfx2  14920  ofs1  14943  relexp0g  14995  relexpaddg  15026  rtrclreclem2  15032  fsumnn0cl  15709  binom  15803  bcxmas  15808  isumnn0nn  15815  climcndslem1  15822  geoser  15840  geomulcvg  15849  risefac0  16000  fallfac0  16001  risefac1  16006  fallfac1  16007  binomfallfaclem2  16013  binomfallfac  16014  bpoly0  16023  bpoly2  16030  bpoly3  16031  bpoly4  16032  fsumcube  16033  ef0lem  16051  ege2le3  16063  ef4p  16088  efgt1p2  16089  efgt1p  16090  ruclem11  16215  nthruz  16228  nn0o  16360  ndvdssub  16386  5ndvds3  16390  bits0  16405  0bits  16416  sadcf  16430  sadc0  16431  sadcaddlem  16434  sadcadd  16435  sadadd2lem  16436  sadadd2  16437  smupf  16455  smup0  16456  smumullem  16469  gcdcl  16483  nn0seqcvgd  16547  algcvg  16553  eucalg  16564  lcmcl  16578  lcmfval  16598  lcmfcl  16605  pclem  16816  pcfac  16877  vdwap0  16954  vdwap1  16955  vdwlem6  16964  hashbc0  16983  0ram  16998  0ramcl  17001  ramz2  17002  ramz  17003  ramcl  17007  prmo0  17014  dec5dvds2  17043  2exp11  17067  2exp16  17068  11prm  17092  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  plendxnocndx  17354  slotsdifdsndx  17364  slotsdifunifndx  17371  odrngstr  17373  slotsdifplendx2  17386  imasvalstr  17421  ipostr  18495  gsumws1  18772  cycsubm  19141  psgnunilem2  19432  psgnunilem3  19433  odfval  19469  oddvdsnn0  19481  pgp0  19533  sylow1lem1  19535  cyggex2  19834  telgsums  19930  srgbinomlem3  20144  srgbinomlem4  20145  srgbinom  20147  cnfldstr  21273  cnfldstrOLD  21288  nn0subm  21346  expmhm  21360  nn0srg  21361  znf1o  21468  zzngim  21469  cygznlem1  21483  cygznlem2a  21484  cygznlem3  21486  cygth  21488  freshmansdream  21491  snifpsrbag  21836  fczpsrbag  21837  psrbagaddcl  21840  psrlidm  21878  mvrf1  21902  mplcoe3  21952  mplcoe5  21954  ltbwe  21958  psrbag0  21976  psrbagsn  21977  evlslem1  21996  mhpsclcl  22041  mhpmulcl  22043  psdmul  22060  psdmvr  22063  00ply1bas  22131  ply1plusgfvi  22133  coe1sclmul  22175  coe1sclmul2  22177  coe1scl  22180  ply1sclid  22181  ply1idvr1OLD  22189  cply1coe0bi  22196  ply1scleq  22199  cpm2mf  22646  m2cpminvid2lem  22648  m2cpminvid2  22649  m2cpmfo  22650  decpmatid  22664  pmatcollpw3  22678  pmatcollpw3fi1lem1  22680  pmatcollpwscmatlem1  22683  pmatcollpwscmatlem2  22684  idpm2idmp  22695  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  cpmadugsumlemF  22770  dscmet  24467  ehl0base  25323  ehl0  25324  itgcnlem  25698  dvn0  25833  dvn1  25835  cpncn  25845  dveflem  25890  c1lip2  25910  deg1le0  26023  ply1divex  26049  mon1pid  26066  ply1rem  26078  fta1g  26082  plyconst  26118  plypf1  26124  plyco  26153  0dgr  26157  0dgrb  26158  coefv0  26160  dgreq0  26178  vieta1lem2  26226  vieta1  26227  aareccl  26241  aannenlem2  26244  taylthlem1  26288  radcnv0  26332  abelthlem6  26353  abelthlem9  26357  logtayl  26576  cxp0  26586  cxpeq  26674  leibpilem2  26858  leibpi  26859  log2ublem3  26865  log2ub  26866  log2le1  26867  divsqrtsumlem  26897  dmgmn0  26943  lgambdd  26954  sqff1o  27099  ppiublem2  27121  chtublem  27129  bclbnd  27198  bposlem8  27209  lgsval  27219  dchrisum0flblem1  27426  dchrisum0flb  27428  ostth2lem2  27552  usgrexmplef  29193  usgr0edg0rusgr  29510  usgr2pthlem  29700  wwlksn0s  29798  rusgrnumwwlkb0  29908  erclwwlkref  29956  clwwlkf1  29985  0wlkonlem1  30054  upgr4cycl4dv4e  30121  1kp2ke3k  30382  ex-fac  30387  ex-prmo  30395  nn0min  32752  dpmul1000  32826  dp0h  32829  dpexpp1  32835  dpmul4  32841  threehalves  32842  1mhdrd  32843  s1f1  32871  s2f1  32873  cshw1s2  32889  cycpm2tr  33083  deg1le0eq0  33549  ply1unit  33551  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  ply1dg1rt  33555  m1pmeq  33559  minplyirredlem  33707  rtelextdg2lem  33723  fldext2chn  33725  constraddcl  33759  constrnegcl  33760  constrdircl  33762  constrremulcl  33764  2sqr3minply  33777  lmatcl  33813  lmat22e12  33816  lmat22e21  33817  fsumcvg4  33947  oddpwdc  34352  eulerpartlems  34358  eulerpartlemb  34366  eulerpartlemt  34369  eulerpartgbij  34370  eulerpartlemmf  34373  eulerpartlemgf  34377  eulerpartlemgs2  34378  eulerpartlemn  34379  fib0  34397  fib1  34398  fibp1  34399  ofcs1  34542  signsply0  34549  signsvvf  34577  prodfzo03  34601  repr0  34609  breprexp  34631  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  hgt750leme  34656  tgoldbachgtde  34658  0nn0m1nnn0  35107  f1resfz0f1d  35108  usgrgt2cycl  35124  subfac0  35171  subfacval2  35181  subfaclim  35182  cvmliftlem7  35285  cvmliftlem13  35290  bccolsum  35733  fwddifn0  36159  heiborlem4  37815  heiborlem10  37821  12gcd5e1  41998  60gcd6e6  41999  60gcd7e1  42000  420gcd8e4  42001  12lcm5e60  42003  60lcm7e420  42005  420lcm8e840  42006  lcmineqlem  42047  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow5ineq2  42050  3lexlogpow5ineq5  42055  aks4d1p1  42071  aks6d1c2lem4  42122  aks6d1c2  42125  sticksstones11  42151  sticksstones22  42163  aks6d1c7lem1  42175  sqn5i  42280  decpmul  42283  sqdeccom12  42284  sq3deccom12  42285  235t711  42300  ex-decpmul  42301  mhphflem  42591  0prjspn  42623  sum9cubes  42667  nacsfix  42707  diophrw  42754  pell1qr1  42866  monotoddzzfi  42938  jm2.23  42992  hbtlem5  43124  mncn0  43135  aaitgo  43158  brfvrcld  43687  corclrcl  43703  dfrtrcl3  43729  fvrtrcllb0d  43731  fvrtrcllb0da  43732  corcltrcl  43735  cotrclrcl  43738  k0004val0  44150  bccn0  44339  bccn1  44340  binomcxplemradcnv  44348  binomcxplemnotnn0  44352  rexanuz2nf  45495  dvnmul  45948  dvnprodlem3  45953  wallispilem2  46071  wallispi2lem2  46077  stirlinglem5  46083  stirlinglem7  46085  fourierdlem83  46194  fourierdlem112  46223  fouriersw  46236  elaa2lem  46238  elaa2  46239  etransclem48  46287  etransc  46288  iccelpart  47438  fmtno0  47545  fmtnorec2  47548  fmtno5lem1  47558  fmtno5lem2  47559  fmtno5lem4  47561  257prm  47566  fmtnofac2  47574  fmtnofac1  47575  fmtno4prmfac  47577  fmtno4nprmfac193  47579  fmtno5faclem1  47584  fmtno5faclem2  47585  fmtno5faclem3  47586  fmtno5fac  47587  fmtno5nprm  47588  139prmALT  47601  31prm  47602  127prm  47604  m11nprm  47606  bits0ALTV  47684  2exp340mod341  47738  nfermltl2rev  47748  evengpoap3  47804  tgoldbachlt  47821  tgoldbach  47822  stgr0  47963  usgrexmpl1lem  48016  usgrexmpl2lem  48021  gpgprismgr4cycllem6  48094  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem10  48098  nn0mnd  48171  ssnn0ssfz  48341  dig1  48601  0dig2nn0e  48605  0dig2nn0o  48606  0aryfvalel  48627  itcoval0  48655  itcoval1  48656  ackval0  48673  ackval1  48674  ackvalsuc0val  48680  ackval0012  48682  ackval1012  48683  ackval2012  48684  ackval3012  48685  ackval41a  48687