Theorem 0nn0 12457

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 12444	. . . 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 11068  ℕcn 12186  ℕ₀cn0 12442

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 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-i2m1 11136

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 3449  df-un 3919  df-sn 4590  df-n0 12443

This theorem is referenced by:  0xnn0  12521  nn0ind-raph  12634  10nn0  12667  declei  12685  numlti  12686  nummul1c  12698  decaddc2  12705  decrmanc  12706  decrmac  12707  decaddm10  12708  decaddi  12709  decaddci  12710  decaddci2  12711  decmul1  12713  decmulnc  12716  6p5e11  12722  7p4e11  12725  8p3e11  12730  9p2e11  12736  10p10e20  12744  xnn0n0n1ge2b  13092  0elfz  13585  4fvwrd4  13609  fvinim0ffz  13747  ssnn0fi  13950  fsuppmapnn0fiubex  13957  exple1  14142  nn0opth2  14237  faclbnd4lem3  14260  bc0k  14276  bcn1  14278  bccl  14287  hasheq0  14328  hashrabrsn  14337  hashbc  14418  fi1uzind  14472  brfi1ind  14474  opfi1ind  14477  iswrdi  14482  wrdnfi  14513  s1fv  14575  ccat2s1fst  14604  splfv2a  14721  repsw0  14742  0csh0  14758  cshw1  14787  s2fv0  14853  s3fv0  14857  s4fv0  14861  pfx2  14913  ofs1  14936  relexp0g  14988  relexpaddg  15019  rtrclreclem2  15025  fsumnn0cl  15702  binom  15796  bcxmas  15801  isumnn0nn  15808  climcndslem1  15815  geoser  15833  geomulcvg  15842  risefac0  15993  fallfac0  15994  risefac1  15999  fallfac1  16000  binomfallfaclem2  16006  binomfallfac  16007  bpoly0  16016  bpoly2  16023  bpoly3  16024  bpoly4  16025  fsumcube  16026  ef0lem  16044  ege2le3  16056  ef4p  16081  efgt1p2  16082  efgt1p  16083  ruclem11  16208  nthruz  16221  nn0o  16353  ndvdssub  16379  5ndvds3  16383  bits0  16398  0bits  16409  sadcf  16423  sadc0  16424  sadcaddlem  16427  sadcadd  16428  sadadd2lem  16429  sadadd2  16430  smupf  16448  smup0  16449  smumullem  16462  gcdcl  16476  nn0seqcvgd  16540  algcvg  16546  eucalg  16557  lcmcl  16571  lcmfval  16591  lcmfcl  16598  pclem  16809  pcfac  16870  vdwap0  16947  vdwap1  16948  vdwlem6  16957  hashbc0  16976  0ram  16991  0ramcl  16994  ramz2  16995  ramz  16996  ramcl  17000  prmo0  17007  dec5dvds2  17036  2exp11  17060  2exp16  17061  11prm  17085  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  plendxnocndx  17347  slotsdifdsndx  17357  slotsdifunifndx  17364  odrngstr  17366  slotsdifplendx2  17379  imasvalstr  17414  ipostr  18488  gsumws1  18765  cycsubm  19134  psgnunilem2  19425  psgnunilem3  19426  odfval  19462  oddvdsnn0  19474  pgp0  19526  sylow1lem1  19528  cyggex2  19827  telgsums  19923  srgbinomlem3  20137  srgbinomlem4  20138  srgbinom  20140  cnfldstr  21266  cnfldstrOLD  21281  nn0subm  21339  expmhm  21353  nn0srg  21354  znf1o  21461  zzngim  21462  cygznlem1  21476  cygznlem2a  21477  cygznlem3  21479  cygth  21481  freshmansdream  21484  snifpsrbag  21829  fczpsrbag  21830  psrbagaddcl  21833  psrlidm  21871  mvrf1  21895  mplcoe3  21945  mplcoe5  21947  ltbwe  21951  psrbag0  21969  psrbagsn  21970  evlslem1  21989  mhpsclcl  22034  mhpmulcl  22036  psdmul  22053  psdmvr  22056  00ply1bas  22124  ply1plusgfvi  22126  coe1sclmul  22168  coe1sclmul2  22170  coe1scl  22173  ply1sclid  22174  ply1idvr1OLD  22182  cply1coe0bi  22189  ply1scleq  22192  cpm2mf  22639  m2cpminvid2lem  22641  m2cpminvid2  22642  m2cpmfo  22643  decpmatid  22657  pmatcollpw3  22671  pmatcollpw3fi1lem1  22673  pmatcollpwscmatlem1  22676  pmatcollpwscmatlem2  22677  idpm2idmp  22688  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  cpmadugsumlemF  22763  dscmet  24460  ehl0base  25316  ehl0  25317  itgcnlem  25691  dvn0  25826  dvn1  25828  cpncn  25838  dveflem  25883  c1lip2  25903  deg1le0  26016  ply1divex  26042  mon1pid  26059  ply1rem  26071  fta1g  26075  plyconst  26111  plypf1  26117  plyco  26146  0dgr  26150  0dgrb  26151  coefv0  26153  dgreq0  26171  vieta1lem2  26219  vieta1  26220  aareccl  26234  aannenlem2  26237  taylthlem1  26281  radcnv0  26325  abelthlem6  26346  abelthlem9  26350  logtayl  26569  cxp0  26579  cxpeq  26667  leibpilem2  26851  leibpi  26852  log2ublem3  26858  log2ub  26859  log2le1  26860  divsqrtsumlem  26890  dmgmn0  26936  lgambdd  26947  sqff1o  27092  ppiublem2  27114  chtublem  27122  bclbnd  27191  bposlem8  27202  lgsval  27212  dchrisum0flblem1  27419  dchrisum0flb  27421  ostth2lem2  27545  usgrexmplef  29186  usgr0edg0rusgr  29503  usgr2pthlem  29693  wwlksn0s  29791  rusgrnumwwlkb0  29901  erclwwlkref  29949  clwwlkf1  29978  0wlkonlem1  30047  upgr4cycl4dv4e  30114  1kp2ke3k  30375  ex-fac  30380  ex-prmo  30388  nn0min  32745  dpmul1000  32819  dp0h  32822  dpexpp1  32828  dpmul4  32834  threehalves  32835  1mhdrd  32836  s1f1  32864  s2f1  32866  cshw1s2  32882  cycpm2tr  33076  deg1le0eq0  33542  ply1unit  33544  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  ply1dg1rt  33548  m1pmeq  33552  minplyirredlem  33700  rtelextdg2lem  33716  fldext2chn  33718  constraddcl  33752  constrnegcl  33753  constrdircl  33755  constrremulcl  33757  2sqr3minply  33770  lmatcl  33806  lmat22e12  33809  lmat22e21  33810  fsumcvg4  33940  oddpwdc  34345  eulerpartlems  34351  eulerpartlemb  34359  eulerpartlemt  34362  eulerpartgbij  34363  eulerpartlemmf  34366  eulerpartlemgf  34370  eulerpartlemgs2  34371  eulerpartlemn  34372  fib0  34390  fib1  34391  fibp1  34392  ofcs1  34535  signsply0  34542  signsvvf  34570  prodfzo03  34594  repr0  34602  breprexp  34624  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  tgoldbachgtde  34651  0nn0m1nnn0  35100  f1resfz0f1d  35101  usgrgt2cycl  35117  subfac0  35164  subfacval2  35174  subfaclim  35175  cvmliftlem7  35278  cvmliftlem13  35283  bccolsum  35726  fwddifn0  36152  heiborlem4  37808  heiborlem10  37814  12gcd5e1  41991  60gcd6e6  41992  60gcd7e1  41993  420gcd8e4  41994  12lcm5e60  41996  60lcm7e420  41998  420lcm8e840  41999  lcmineqlem  42040  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow5ineq2  42043  3lexlogpow5ineq5  42048  aks4d1p1  42064  aks6d1c2lem4  42115  aks6d1c2  42118  sticksstones11  42144  sticksstones22  42156  aks6d1c7lem1  42168  sqn5i  42273  decpmul  42276  sqdeccom12  42277  sq3deccom12  42278  235t711  42293  ex-decpmul  42294  mhphflem  42584  0prjspn  42616  sum9cubes  42660  nacsfix  42700  diophrw  42747  pell1qr1  42859  monotoddzzfi  42931  jm2.23  42985  hbtlem5  43117  mncn0  43128  aaitgo  43151  brfvrcld  43680  corclrcl  43696  dfrtrcl3  43722  fvrtrcllb0d  43724  fvrtrcllb0da  43725  corcltrcl  43728  cotrclrcl  43731  k0004val0  44143  bccn0  44332  bccn1  44333  binomcxplemradcnv  44341  binomcxplemnotnn0  44345  rexanuz2nf  45488  dvnmul  45941  dvnprodlem3  45946  wallispilem2  46064  wallispi2lem2  46070  stirlinglem5  46076  stirlinglem7  46078  fourierdlem83  46187  fourierdlem112  46216  fouriersw  46229  elaa2lem  46231  elaa2  46232  etransclem48  46280  etransc  46281  iccelpart  47434  fmtno0  47541  fmtnorec2  47544  fmtno5lem1  47554  fmtno5lem2  47555  fmtno5lem4  47557  257prm  47562  fmtnofac2  47570  fmtnofac1  47571  fmtno4prmfac  47573  fmtno4nprmfac193  47575  fmtno5faclem1  47580  fmtno5faclem2  47581  fmtno5faclem3  47582  fmtno5fac  47583  fmtno5nprm  47584  139prmALT  47597  31prm  47598  127prm  47600  m11nprm  47602  bits0ALTV  47680  2exp340mod341  47734  nfermltl2rev  47744  evengpoap3  47800  tgoldbachlt  47817  tgoldbach  47818  stgr0  47959  usgrexmpl1lem  48012  usgrexmpl2lem  48017  gpgprismgr4cycllem6  48090  gpgprismgr4cycllem7  48091  gpgprismgr4cycllem10  48094  nn0mnd  48167  ssnn0ssfz  48337  dig1  48597  0dig2nn0e  48601  0dig2nn0o  48602  0aryfvalel  48623  itcoval0  48651  itcoval1  48652  ackval0  48669  ackval1  48670  ackvalsuc0val  48676  ackval0012  48678  ackval1012  48679  ackval2012  48680  ackval3012  48681  ackval41a  48683