Theorem 0nn0 12428

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 12415	. . . 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 11038  ℕcn 12157  ℕ₀cn0 12413

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 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-i2m1 11106

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 3444  df-un 3908  df-sn 4583  df-n0 12414

This theorem is referenced by:  0xnn0  12492  nn0ind-raph  12604  10nn0  12637  declei  12655  numlti  12656  nummul1c  12668  decaddc2  12675  decrmanc  12676  decrmac  12677  decaddm10  12678  decaddi  12679  decaddci  12680  decaddci2  12681  decmul1  12683  decmulnc  12686  6p5e11  12692  7p4e11  12695  8p3e11  12700  9p2e11  12706  10p10e20  12714  xnn0n0n1ge2b  13058  0elfz  13552  4fvwrd4  13576  fvinim0ffz  13717  ssnn0fi  13920  fsuppmapnn0fiubex  13927  exple1  14112  nn0opth2  14207  faclbnd4lem3  14230  bc0k  14246  bcn1  14248  bccl  14257  hasheq0  14298  hashrabrsn  14307  hashbc  14388  fi1uzind  14442  brfi1ind  14444  opfi1ind  14447  iswrdi  14452  wrdnfi  14483  s1fv  14546  ccat2s1fst  14575  splfv2a  14691  repsw0  14712  0csh0  14728  cshw1  14757  s2fv0  14822  s3fv0  14826  s4fv0  14830  pfx2  14882  ofs1  14905  relexp0g  14957  relexpaddg  14988  rtrclreclem2  14994  fsumnn0cl  15671  binom  15765  bcxmas  15770  isumnn0nn  15777  climcndslem1  15784  geoser  15802  geomulcvg  15811  risefac0  15962  fallfac0  15963  risefac1  15968  fallfac1  15969  binomfallfaclem2  15975  binomfallfac  15976  bpoly0  15985  bpoly2  15992  bpoly3  15993  bpoly4  15994  fsumcube  15995  ef0lem  16013  ege2le3  16025  ef4p  16050  efgt1p2  16051  efgt1p  16052  ruclem11  16177  nthruz  16190  nn0o  16322  ndvdssub  16348  5ndvds3  16352  bits0  16367  0bits  16378  sadcf  16392  sadc0  16393  sadcaddlem  16396  sadcadd  16397  sadadd2lem  16398  sadadd2  16399  smupf  16417  smup0  16418  smumullem  16431  gcdcl  16445  nn0seqcvgd  16509  algcvg  16515  eucalg  16526  lcmcl  16540  lcmfval  16560  lcmfcl  16567  pclem  16778  pcfac  16839  vdwap0  16916  vdwap1  16917  vdwlem6  16926  hashbc0  16945  0ram  16960  0ramcl  16963  ramz2  16964  ramz  16965  ramcl  16969  prmo0  16976  dec5dvds2  17005  2exp11  17029  2exp16  17030  11prm  17054  37prm  17060  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  plendxnocndx  17316  slotsdifdsndx  17326  slotsdifunifndx  17333  odrngstr  17335  slotsdifplendx2  17348  imasvalstr  17383  ipostr  18464  gsumws1  18775  cycsubm  19143  psgnunilem2  19436  psgnunilem3  19437  odfval  19473  oddvdsnn0  19485  pgp0  19537  sylow1lem1  19539  cyggex2  19838  telgsums  19934  srgbinomlem3  20175  srgbinomlem4  20176  srgbinom  20178  cnfldstr  21323  cnfldstrOLD  21338  nn0subm  21389  expmhm  21403  nn0srg  21404  znf1o  21518  zzngim  21519  cygznlem1  21533  cygznlem2a  21534  cygznlem3  21536  cygth  21538  freshmansdream  21541  snifpsrbag  21888  fczpsrbag  21889  psrbagaddcl  21892  psrlidm  21929  mvrf1  21953  mplcoe3  22005  mplcoe5  22007  ltbwe  22011  psrbag0  22029  psrbagsn  22030  evlslem1  22049  mhpsclcl  22102  mhpmulcl  22104  psdmul  22121  psdmvr  22124  00ply1bas  22192  ply1plusgfvi  22194  coe1sclmul  22236  coe1sclmul2  22238  coe1scl  22241  ply1sclid  22242  ply1idvr1OLD  22251  cply1coe0bi  22258  ply1scleq  22261  cpm2mf  22708  m2cpminvid2lem  22710  m2cpminvid2  22711  m2cpmfo  22712  decpmatid  22726  pmatcollpw3  22740  pmatcollpw3fi1lem1  22742  pmatcollpwscmatlem1  22745  pmatcollpwscmatlem2  22746  idpm2idmp  22757  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  cpmadugsumlemF  22832  dscmet  24528  ehl0base  25384  ehl0  25385  itgcnlem  25759  dvn0  25894  dvn1  25896  cpncn  25906  dveflem  25951  c1lip2  25971  deg1le0  26084  ply1divex  26110  mon1pid  26127  ply1rem  26139  fta1g  26143  plyconst  26179  plypf1  26185  plyco  26214  0dgr  26218  0dgrb  26219  coefv0  26221  dgreq0  26239  vieta1lem2  26287  vieta1  26288  aareccl  26302  aannenlem2  26305  taylthlem1  26349  radcnv0  26393  abelthlem6  26414  abelthlem9  26418  logtayl  26637  cxp0  26647  cxpeq  26735  leibpilem2  26919  leibpi  26920  log2ublem3  26926  log2ub  26927  log2le1  26928  divsqrtsumlem  26958  dmgmn0  27004  lgambdd  27015  sqff1o  27160  ppiublem2  27182  chtublem  27190  bclbnd  27259  bposlem8  27270  lgsval  27280  dchrisum0flblem1  27487  dchrisum0flb  27489  ostth2lem2  27613  usgrexmplef  29344  usgr0edg0rusgr  29661  usgr2pthlem  29848  wwlksn0s  29946  rusgrnumwwlkb0  30059  erclwwlkref  30107  clwwlkf1  30136  0wlkonlem1  30205  upgr4cycl4dv4e  30272  1kp2ke3k  30533  ex-fac  30538  ex-prmo  30546  nn0min  32912  dpmul1000  32991  dp0h  32994  dpexpp1  33000  dpmul4  33006  threehalves  33007  1mhdrd  33008  s1f1  33036  s2f1  33038  cshw1s2  33053  cycpm2tr  33213  deg1le0eq0  33666  ply1unit  33668  evl1deg1  33669  evl1deg2  33670  evl1deg3  33671  ply1dg1rt  33673  m1pmeq  33678  psrbasfsupp  33705  mplmulmvr  33716  evlextv  33719  mplvrpmlem  33720  mplvrpmfgalem  33721  mplvrpmga  33722  mplvrpmmhm  33723  mplvrpmrhm  33724  psrmonprod  33729  esplyfval0  33741  esplylem  33743  esplyfv1  33746  esplyfval1  33750  esplyfvaln  33751  esplyind  33752  vietalem  33756  vieta  33757  minplyirredlem  33888  rtelextdg2lem  33904  fldext2chn  33906  constraddcl  33940  constrnegcl  33941  constrdircl  33943  constrremulcl  33945  2sqr3minply  33958  lmatcl  33994  lmat22e12  33997  lmat22e21  33998  fsumcvg4  34128  oddpwdc  34532  eulerpartlems  34538  eulerpartlemb  34546  eulerpartlemt  34549  eulerpartgbij  34550  eulerpartlemmf  34553  eulerpartlemgf  34557  eulerpartlemgs2  34558  eulerpartlemn  34559  fib0  34577  fib1  34578  fibp1  34579  ofcs1  34722  signsply0  34729  signsvvf  34757  prodfzo03  34781  repr0  34789  breprexp  34811  hgt750lemd  34826  hgt750lem  34829  hgt750lem2  34830  hgt750leme  34836  tgoldbachgtde  34838  0nn0m1nnn0  35329  f1resfz0f1d  35330  usgrgt2cycl  35346  subfac0  35393  subfacval2  35403  subfaclim  35404  cvmliftlem7  35507  cvmliftlem13  35512  bccolsum  35955  fwddifn0  36380  heiborlem4  38065  heiborlem10  38071  12gcd5e1  42373  60gcd6e6  42374  60gcd7e1  42375  420gcd8e4  42376  12lcm5e60  42378  60lcm7e420  42380  420lcm8e840  42381  lcmineqlem  42422  3exp7  42423  3lexlogpow5ineq1  42424  3lexlogpow5ineq2  42425  3lexlogpow5ineq5  42430  aks4d1p1  42446  aks6d1c2lem4  42497  aks6d1c2  42500  sticksstones11  42526  sticksstones22  42538  aks6d1c7lem1  42550  sqn5i  42655  decpmul  42658  sqdeccom12  42659  sq3deccom12  42660  235t711  42675  ex-decpmul  42676  mhphflem  42954  0prjspn  42986  sum9cubes  43030  nacsfix  43069  diophrw  43116  pell1qr1  43228  monotoddzzfi  43299  jm2.23  43353  hbtlem5  43485  mncn0  43496  aaitgo  43519  brfvrcld  44047  corclrcl  44063  dfrtrcl3  44089  fvrtrcllb0d  44091  fvrtrcllb0da  44092  corcltrcl  44095  cotrclrcl  44098  k0004val0  44510  bccn0  44699  bccn1  44700  binomcxplemradcnv  44708  binomcxplemnotnn0  44712  rexanuz2nf  45850  dvnmul  46301  dvnprodlem3  46306  wallispilem2  46424  wallispi2lem2  46430  stirlinglem5  46436  stirlinglem7  46438  fourierdlem83  46547  fourierdlem112  46576  fouriersw  46589  elaa2lem  46591  elaa2  46592  etransclem48  46640  etransc  46641  iccelpart  47793  fmtno0  47900  fmtnorec2  47903  fmtno5lem1  47913  fmtno5lem2  47914  fmtno5lem4  47916  257prm  47921  fmtnofac2  47929  fmtnofac1  47930  fmtno4prmfac  47932  fmtno4nprmfac193  47934  fmtno5faclem1  47939  fmtno5faclem2  47940  fmtno5faclem3  47941  fmtno5fac  47942  fmtno5nprm  47943  139prmALT  47956  31prm  47957  127prm  47959  m11nprm  47961  bits0ALTV  48039  2exp340mod341  48093  nfermltl2rev  48103  evengpoap3  48159  tgoldbachlt  48176  tgoldbach  48177  stgr0  48320  usgrexmpl1lem  48381  usgrexmpl2lem  48386  gpgprismgr4cycllem6  48460  gpgprismgr4cycllem7  48461  gpgprismgr4cycllem10  48464  nn0mnd  48539  ssnn0ssfz  48709  dig1  48968  0dig2nn0e  48972  0dig2nn0o  48973  0aryfvalel  48994  itcoval0  49022  itcoval1  49023  ackval0  49040  ackval1  49041  ackvalsuc0val  49047  ackval0012  49049  ackval1012  49050  ackval2012  49051  ackval3012  49052  ackval41a  49054