Theorem 0nn0 12661

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 2763	. 2 ⊢ 0 = 0
2		elnn0 12648	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 231	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 890	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

This proof depends on syntax axioms:   ∨ wo 861   = wceq 1570   ∈ wcel 2147  0cc0 11239  ℕcn 12375  ℕ₀cn0 12646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-mulcl 11301  ax-i2m1 11307

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-n0 12647

This theorem is used by:  0xnn0  12725  0nn0m1nnn0  12793  nn0ind-raph  12839  10nn0  12876  declei  12895  numlti  12896  nummul1c  12908  decaddc2  12915  decrmanc  12916  decrmac  12917  decaddm10  12918  decaddi  12919  decaddci  12920  decaddci2  12921  decmul1  12923  decmulnc  12926  6p5e11  12932  7p4e11  12935  8p3e11  12940  9p2e11  12946  10p10e20  12954  xnn0n0n1ge2b  13301  0elfz  13798  4fvwrd4  13822  fvinim0ffz  13964  f1resfz0f1d  13967  ssnn0fi  14168  fsuppmapnn0fiubex  14175  exple1  14360  nn0opth2  14457  faclbnd4lem3  14480  bc0k  14496  bcn1  14498  bccl  14507  hasheq0  14548  hashrabrsn  14557  hashbc  14639  fi1uzind  14693  brfi1ind  14695  opfi1ind  14698  iswrdi  14703  wrdnfi  14734  s1f1  14798  s1fv  14800  ccat2s1fst  14829  splfv2a  14947  repsw0  14970  0csh0  14986  cshw1  15015  s2fv0  15080  s3fv0  15085  s4fv0  15089  pfx2  15141  ofs1  15166  relexp0g  15218  relexpaddg  15249  rtrclreclem2  15255  fsumnn0cl  15946  binom  16043  bcxmas  16048  isumnn0nn  16055  climcndslem1  16062  geoser  16080  geomulcvg  16089  risefac0  16237  fallfac0  16238  risefac1  16243  fallfac1  16244  binomfallfaclem2  16250  binomfallfac  16251  bpoly0  16260  bpoly2  16267  bpoly3  16268  bpoly4  16269  fsumcube  16270  ef0lem  16288  ege2le3  16300  ef4p  16325  efgt1p2  16326  efgt1p  16327  ruclem11  16452  nthruz  16465  nn0o  16597  ndvdssub  16623  5ndvds3  16627  bits0  16642  0bits  16653  sadcf  16667  sadc0  16668  sadcaddlem  16671  sadcadd  16672  sadadd2lem  16673  sadadd2  16674  smupf  16692  smup0  16693  smumullem  16706  gcdcl  16720  nn0seqcvgd  16789  algcvg  16795  eucalg  16806  lcmcl  16820  lcmfval  16840  lcmfcl  16847  pclem  17060  pcfac  17121  vdwap0  17198  vdwap1  17199  vdwlem6  17208  hashbc0  17227  0ram  17242  0ramcl  17245  ramz2  17246  ramz  17247  ramcl  17251  prmo0  17258  dec5dvds2  17287  2exp11  17311  2exp16  17312  10nprm  17335  11prm  17337  37prm  17343  43prm  17344  83prm  17345  139prm  17346  163prm  17347  317prm  17348  631prm  17349  1259lem1  17353  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  2503lem1  17359  2503lem2  17360  2503lem3  17361  2503prm  17362  4001lem1  17363  4001lem2  17364  4001lem3  17365  4001lem4  17366  4001prm  17367  plendxnocndx  17601  slotsdifdsndx  17611  slotsdifunifndx  17618  odrngstr  17620  slotsdifplendx2  17637  imasvalstr  17672  ipostr  18753  gsumws1  19084  cycsubm  19467  psgnunilem2  19760  psgnunilem3  19761  odfval  19797  oddvdsnn0  19809  pgp0  19861  sylow1lem1  19863  cyggex2  20162  telgsums  20258  srgbinomlem3  20505  srgbinomlem4  20506  srgbinom  20508  cnfldstr  21731  cnfldfunALT  21745  nn0subm  21782  expmhm  21796  nn0srg  21797  znf1o  21912  zzngim  21913  cygznlem1  21927  cygznlem2a  21928  cygznlem3  21930  cygth  21932  freshmansdream  21935  snifpsrbag  22283  fczpsrbag  22284  psrbagaddcl  22287  psrlidm  22324  mvrf1  22348  mplcoe3  22402  mplcoe5  22404  ltbwe  22408  psrbag0  22426  psrbagsn  22427  evlslem1  22446  mhpsclcl  22523  mhpmulcl  22525  psdmul  22542  psdmvr  22545  00ply1bas  22612  ply1plusgfvi  22614  coe1sclmul  22656  coe1sclmul2  22658  coe1scl  22661  ply1sclid  22662  cply1coe0bi  22675  ply1scleq  22678  cpm2mf  23125  m2cpminvid2lem  23127  m2cpminvid2  23128  m2cpmfo  23129  decpmatid  23143  pmatcollpw3  23157  pmatcollpw3fi1lem1  23159  pmatcollpwscmatlem1  23162  pmatcollpwscmatlem2  23163  idpm2idmp  23174  chfacfscmulgsum  23233  chfacfpmmulgsum  23237  cpmadugsumlemF  23249  dscmet  24946  ehl0base  25792  ehl0  25793  itgcnlem  26165  dvn0  26299  dvn1  26301  cpncn  26311  dveflem  26354  c1lip2  26373  deg1le0  26484  ply1divex  26510  mon1pid  26527  ply1rem  26539  fta1g  26543  plyconst  26579  plypf1  26586  plyco  26615  0dgr  26619  0dgrb  26620  coefv0  26622  dgreq0  26639  vieta1lem2  26689  vieta1  26690  aareccl  26710  aannenlem2  26713  taylthlem1  26757  radcnv0  26800  abelthlem6  26820  abelthlem9  26824  logtayl  27045  cxp0  27055  cxpeq  27142  leibpilem2  27326  leibpi  27327  log2ublem3  27333  log2ub  27334  log2le1  27335  divsqrtsumlem  27364  dmgmn0  27410  lgambdd  27421  sqff1o  27566  ppiublem2  27587  chtublem  27595  bclbnd  27664  bposlem8  27675  lgsval  27685  dchrisum0flblem1  27892  dchrisum0flb  27894  ostth2lem2  28018  usgrexmplef  29897  usgr0edg0rusgr  30213  usgr2pthlem  30406  wwlksn0s  30507  rusgrnumwwlkb0  30620  erclwwlkref  30668  clwwlkf1  30697  0wlkonlem1  30766  upgr4cycl4dv4e  30843  1kp2ke3k  31104  ex-fac  31109  ex-prmo  31117  nn0min  33508  dpmul1000  33561  dp0h  33564  dpexpp1  33570  dpmul4  33576  threehalves  33577  1mhdrd  33578  s2f1  33606  cshw1s2  33617  cycpm2tr  33779  deg1le0eq0  34208  ply1unit  34210  evl1deg1  34211  evl1deg2  34212  evl1deg3  34213  ply1dg1rt  34215  m1pmeq  34220  evls1degle1  34239  rngunsnply1chr2  34253  psrbasfsupp  34254  mplmulmvr  34282  evlextv  34285  mplvrpmlem  34286  mplvrpmfgalem  34287  mplvrpmga  34288  mplvrpmmhm  34289  mplvrpmrhm  34290  psrmonprod  34295  esplyfval0  34307  esplylem  34309  esplyfv1  34312  esplyfval1  34316  esplyfvaln  34317  esplyind  34318  vietalem  34322  vieta  34323  minplyirredlem  34453  rtelextdg2lem  34469  fldext2chn  34471  constraddcl  34505  constrnegcl  34506  constrdircl  34508  constrremulcl  34510  2sqr3minply  34523  lmatcl  34559  lmat22e12  34562  lmat22e21  34563  fsumcvg4  34693  oddpwdc  35097  eulerpartlems  35103  eulerpartlemb  35111  eulerpartlemt  35114  eulerpartgbij  35115  eulerpartlemmf  35118  eulerpartlemgf  35122  eulerpartlemgs2  35123  eulerpartlemn  35124  fib0  35142  fib1  35143  fibp1  35144  ofcs1  35287  signsply0  35291  signsvvf  35319  prodfzo03  35343  repr0  35351  breprexp  35373  hgt750lemd  35388  hgt750lem  35391  hgt750lem2  35392  hgt750leme  35398  tgoldbachgtde  35400  usgrgt2cycl  36107  subfac0  36150  subfacval2  36160  subfaclim  36161  cvmliftlem7  36264  cvmliftlem13  36269  bccolsum  36719  fwddifn0  37144  heiborlem4  39014  heiborlem10  39020  12gcd5e1  43319  60gcd6e6  43320  60gcd7e1  43321  420gcd8e4  43322  12lcm5e60  43324  60lcm7e420  43326  420lcm8e840  43327  lcmineqlem  43368  3exp7  43369  3lexlogpow5ineq1  43370  3lexlogpow5ineq2  43371  3lexlogpow5ineq5  43376  aks4d1p1  43392  aks6d1c2lem4  43443  aks6d1c2  43446  sticksstones11  43472  sticksstones22  43484  aks6d1c7lem1  43496  25or6to4  43522  sqn5i  43608  decpmul  43611  sqdeccom12  43612  sq3deccom12  43613  235t711  43628  ex-decpmul  43629  mhphflem  43890  0prjspn  43930  sum9cubes  43949  nacsfix  43989  diophrw  44036  pell1qr1  44144  monotoddzzfi  44215  jm2.23  44269  hbtlem5  44395  mncn0  44406  aaitgo  44429  brfvrcld  44952  corclrcl  44968  dfrtrcl3  44994  fvrtrcllb0d  44996  fvrtrcllb0da  44997  corcltrcl  45000  cotrclrcl  45003  k0004val0  45415  bccn0  45588  bccn1  45589  binomcxplemradcnv  45597  binomcxplemnotnn0  45601  rexanuz2nf  46775  dvnmul  47226  dvnprodlem3  47231  wallispilem2  47349  wallispi2lem2  47355  stirlinglem5  47361  stirlinglem7  47363  fourierdlem83  47472  fourierdlem112  47501  fouriersw  47514  elaa2lem  47516  elaa2  47517  etransclem48  47565  etransc  47566  iccelpart  48788  fmtno0  48898  fmtnorec2  48901  fmtno5lem1  48911  fmtno5lem2  48912  fmtno5lem4  48914  257prm  48919  fmtnofac2  48927  fmtnofac1  48928  fmtno4prmfac  48930  fmtno4nprmfac193  48932  fmtno5faclem1  48937  fmtno5faclem2  48938  fmtno5faclem3  48939  fmtno5fac  48940  fmtno5nprm  48941  139prmALT  48954  31prm  48955  127prm  48957  m11nprm  48959  bits0ALTV  49050  2exp340mod341  49104  nfermltl2rev  49114  evengpoap3  49170  tgoldbachlt  49187  tgoldbach  49188  stgr0  49331  usgrexmpl1lem  49392  usgrexmpl2lem  49397  gpgprismgr4cycllem6  49471  gpgprismgr4cycllem7  49472  gpgprismgr4cycllem10  49475  nn0mnd  49549  linplyfv  49711  linply2cfv  49712  ssnn0ssfz  49792  dig1  50051  0dig2nn0e  50055  0dig2nn0o  50056  0aryfvalel  50077  itcoval0  50105  itcoval1  50106  ackval0  50123  ackval1  50124  ackvalsuc0val  50130  ackval0012  50132  ackval1012  50133  ackval2012  50134  ackval3012  50135  ackval41a  50137