Theorem 0nn0 12546

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 2762	. 2 ⊢ 0 = 0
2		elnn0 12533	. . . 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 2145  0cc0 11127  ℕcn 12260  ℕ₀cn0 12531

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-i2m1 11195

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-n0 12532

This theorem is used by:  0xnn0  12610  0nn0m1nnn0  12678  nn0ind-raph  12724  10nn0  12761  declei  12780  numlti  12781  nummul1c  12793  decaddc2  12800  decrmanc  12801  decrmac  12802  decaddm10  12803  decaddi  12804  decaddci  12805  decaddci2  12806  decmul1  12808  decmulnc  12811  6p5e11  12817  7p4e11  12820  8p3e11  12825  9p2e11  12831  10p10e20  12839  xnn0n0n1ge2b  13185  0elfz  13681  4fvwrd4  13705  fvinim0ffz  13847  f1resfz0f1d  13850  ssnn0fi  14051  fsuppmapnn0fiubex  14058  exple1  14243  nn0opth2  14338  faclbnd4lem3  14361  bc0k  14377  bcn1  14379  bccl  14388  hasheq0  14429  hashrabrsn  14438  hashbc  14520  fi1uzind  14574  brfi1ind  14576  opfi1ind  14579  iswrdi  14584  wrdnfi  14615  s1f1  14678  s1fv  14680  ccat2s1fst  14709  splfv2a  14827  repsw0  14850  0csh0  14866  cshw1  14895  s2fv0  14960  s3fv0  14964  s4fv0  14968  pfx2  15020  ofs1  15045  relexp0g  15097  relexpaddg  15128  rtrclreclem2  15134  fsumnn0cl  15824  binom  15921  bcxmas  15926  isumnn0nn  15933  climcndslem1  15940  geoser  15958  geomulcvg  15967  risefac0  16117  fallfac0  16118  risefac1  16123  fallfac1  16124  binomfallfaclem2  16130  binomfallfac  16131  bpoly0  16140  bpoly2  16147  bpoly3  16148  bpoly4  16149  fsumcube  16150  ef0lem  16168  ege2le3  16180  ef4p  16205  efgt1p2  16206  efgt1p  16207  ruclem11  16332  nthruz  16345  nn0o  16477  ndvdssub  16503  5ndvds3  16507  bits0  16522  0bits  16533  sadcf  16547  sadc0  16548  sadcaddlem  16551  sadcadd  16552  sadadd2lem  16553  sadadd2  16554  smupf  16572  smup0  16573  smumullem  16586  gcdcl  16600  nn0seqcvgd  16664  algcvg  16670  eucalg  16681  lcmcl  16695  lcmfval  16715  lcmfcl  16722  pclem  16934  pcfac  16995  vdwap0  17072  vdwap1  17073  vdwlem6  17082  hashbc0  17101  0ram  17116  0ramcl  17119  ramz2  17120  ramz  17121  ramcl  17125  prmo0  17132  dec5dvds2  17161  2exp11  17185  2exp16  17186  10nprm  17209  11prm  17211  37prm  17217  43prm  17218  83prm  17219  139prm  17220  163prm  17221  317prm  17222  631prm  17223  1259lem1  17227  1259lem2  17228  1259lem3  17229  1259lem4  17230  1259lem5  17231  2503lem1  17233  2503lem2  17234  2503lem3  17235  2503prm  17236  4001lem1  17237  4001lem2  17238  4001lem3  17239  4001lem4  17240  4001prm  17241  plendxnocndx  17473  slotsdifdsndx  17483  slotsdifunifndx  17490  odrngstr  17492  slotsdifplendx2  17505  imasvalstr  17540  ipostr  18621  gsumws1  18951  cycsubm  19334  psgnunilem2  19626  psgnunilem3  19627  odfval  19663  oddvdsnn0  19675  pgp0  19727  sylow1lem1  19729  cyggex2  20028  telgsums  20124  srgbinomlem3  20371  srgbinomlem4  20372  srgbinom  20374  cnfldstr  21591  nn0subm  21639  expmhm  21653  nn0srg  21654  znf1o  21768  zzngim  21769  cygznlem1  21783  cygznlem2a  21784  cygznlem3  21786  cygth  21788  freshmansdream  21791  snifpsrbag  22139  fczpsrbag  22140  psrbagaddcl  22143  psrlidm  22180  mvrf1  22204  mplcoe3  22258  mplcoe5  22260  ltbwe  22264  psrbag0  22282  psrbagsn  22283  evlslem1  22302  mhpsclcl  22379  mhpmulcl  22381  psdmul  22398  psdmvr  22401  00ply1bas  22468  ply1plusgfvi  22470  coe1sclmul  22512  coe1sclmul2  22514  coe1scl  22517  ply1sclid  22518  cply1coe0bi  22531  ply1scleq  22534  cpm2mf  22981  m2cpminvid2lem  22983  m2cpminvid2  22984  m2cpmfo  22985  decpmatid  22999  pmatcollpw3  23013  pmatcollpw3fi1lem1  23015  pmatcollpwscmatlem1  23018  pmatcollpwscmatlem2  23019  idpm2idmp  23030  chfacfscmulgsum  23089  chfacfpmmulgsum  23093  cpmadugsumlemF  23105  dscmet  24802  ehl0base  25648  ehl0  25649  itgcnlem  26022  dvn0  26156  dvn1  26158  cpncn  26168  dveflem  26211  c1lip2  26230  deg1le0  26341  ply1divex  26367  mon1pid  26384  ply1rem  26396  fta1g  26400  plyconst  26436  plypf1  26442  plyco  26471  0dgr  26475  0dgrb  26476  coefv0  26478  dgreq0  26495  vieta1lem2  26545  vieta1  26546  aareccl  26562  aannenlem2  26565  taylthlem1  26609  radcnv0  26652  abelthlem6  26672  abelthlem9  26676  logtayl  26898  cxp0  26908  cxpeq  26995  leibpilem2  27179  leibpi  27180  log2ublem3  27186  log2ub  27187  log2le1  27188  divsqrtsumlem  27217  dmgmn0  27263  lgambdd  27274  sqff1o  27419  ppiublem2  27440  chtublem  27448  bclbnd  27517  bposlem8  27528  lgsval  27538  dchrisum0flblem1  27745  dchrisum0flb  27747  ostth2lem2  27871  usgrexmplef  29720  usgr0edg0rusgr  30036  usgr2pthlem  30229  wwlksn0s  30330  rusgrnumwwlkb0  30443  erclwwlkref  30491  clwwlkf1  30520  0wlkonlem1  30589  upgr4cycl4dv4e  30666  1kp2ke3k  30927  ex-fac  30932  ex-prmo  30940  nn0min  33293  dpmul1000  33346  dp0h  33349  dpexpp1  33355  dpmul4  33361  threehalves  33362  1mhdrd  33363  s2f1  33391  cshw1s2  33402  cycpm2tr  33561  deg1le0eq0  33985  ply1unit  33987  evl1deg1  33988  evl1deg2  33989  evl1deg3  33990  ply1dg1rt  33992  m1pmeq  33997  psrbasfsupp  34023  mplmulmvr  34051  evlextv  34054  mplvrpmlem  34055  mplvrpmfgalem  34056  mplvrpmga  34057  mplvrpmmhm  34058  mplvrpmrhm  34059  psrmonprod  34064  esplyfval0  34076  esplylem  34078  esplyfv1  34081  esplyfval1  34085  esplyfvaln  34086  esplyind  34087  vietalem  34091  vieta  34092  minplyirredlem  34222  rtelextdg2lem  34238  fldext2chn  34240  constraddcl  34274  constrnegcl  34275  constrdircl  34277  constrremulcl  34279  2sqr3minply  34292  lmatcl  34328  lmat22e12  34331  lmat22e21  34332  fsumcvg4  34462  oddpwdc  34867  eulerpartlems  34873  eulerpartlemb  34881  eulerpartlemt  34884  eulerpartgbij  34885  eulerpartlemmf  34888  eulerpartlemgf  34892  eulerpartlemgs2  34893  eulerpartlemn  34894  fib0  34912  fib1  34913  fibp1  34914  ofcs1  35057  signsply0  35061  signsvvf  35089  prodfzo03  35113  repr0  35121  breprexp  35143  hgt750lemd  35158  hgt750lem  35161  hgt750lem2  35162  hgt750leme  35168  tgoldbachgtde  35170  usgrgt2cycl  35725  subfac0  35758  subfacval2  35768  subfaclim  35769  cvmliftlem7  35872  cvmliftlem13  35877  bccolsum  36320  fwddifn0  36746  heiborlem4  38566  heiborlem10  38572  12gcd5e1  42871  60gcd6e6  42872  60gcd7e1  42873  420gcd8e4  42874  12lcm5e60  42876  60lcm7e420  42878  420lcm8e840  42879  lcmineqlem  42920  3exp7  42921  3lexlogpow5ineq1  42922  3lexlogpow5ineq2  42923  3lexlogpow5ineq5  42928  aks4d1p1  42944  aks6d1c2lem4  42995  aks6d1c2  42998  sticksstones11  43024  sticksstones22  43036  aks6d1c7lem1  43048  25or6to4  43074  sqn5i  43162  decpmul  43165  sqdeccom12  43166  sq3deccom12  43167  235t711  43182  ex-decpmul  43183  mhphflem  43444  0prjspn  43476  sum9cubes  43520  nacsfix  43559  diophrw  43606  pell1qr1  43714  monotoddzzfi  43785  jm2.23  43839  hbtlem5  43971  mncn0  43982  aaitgo  44005  brfvrcld  44533  corclrcl  44549  dfrtrcl3  44575  fvrtrcllb0d  44577  fvrtrcllb0da  44578  corcltrcl  44581  cotrclrcl  44584  k0004val0  44996  bccn0  45169  bccn1  45170  binomcxplemradcnv  45178  binomcxplemnotnn0  45182  rexanuz2nf  46322  dvnmul  46773  dvnprodlem3  46778  wallispilem2  46896  wallispi2lem2  46902  stirlinglem5  46908  stirlinglem7  46910  fourierdlem83  47019  fourierdlem112  47048  fouriersw  47061  elaa2lem  47063  elaa2  47064  etransclem48  47112  etransc  47113  iccelpart  48335  fmtno0  48445  fmtnorec2  48448  fmtno5lem1  48458  fmtno5lem2  48459  fmtno5lem4  48461  257prm  48466  fmtnofac2  48474  fmtnofac1  48475  fmtno4prmfac  48477  fmtno4nprmfac193  48479  fmtno5faclem1  48484  fmtno5faclem2  48485  fmtno5faclem3  48486  fmtno5fac  48487  fmtno5nprm  48488  139prmALT  48501  31prm  48502  127prm  48504  m11nprm  48506  bits0ALTV  48597  2exp340mod341  48651  nfermltl2rev  48661  evengpoap3  48717  tgoldbachlt  48734  tgoldbach  48735  stgr0  48878  usgrexmpl1lem  48939  usgrexmpl2lem  48944  gpgprismgr4cycllem6  49018  gpgprismgr4cycllem7  49019  gpgprismgr4cycllem10  49022  nn0mnd  49096  ssnn0ssfz  49281  dig1  49540  0dig2nn0e  49544  0dig2nn0o  49545  0aryfvalel  49566  itcoval0  49594  itcoval1  49595  ackval0  49612  ackval1  49613  ackvalsuc0val  49619  ackval0012  49621  ackval1012  49622  ackval2012  49623  ackval3012  49624  ackval41a  49626