Theorem 0nn0 12628

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 2760	. 2 ⊢ 0 = 0
2		elnn0 12615	. . . 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 1569   ∈ wcel 2144  0cc0 11207  ℕcn 12342  ℕ₀cn0 12613

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-mulcl 11269  ax-i2m1 11275

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150  df-sn 4585  df-n0 12614

This theorem is used by:  0xnn0  12692  0nn0m1nnn0  12760  nn0ind-raph  12806  10nn0  12843  declei  12862  numlti  12863  nummul1c  12875  decaddc2  12882  decrmanc  12883  decrmac  12884  decaddm10  12885  decaddi  12886  decaddci  12887  decaddci2  12888  decmul1  12890  decmulnc  12893  6p5e11  12899  7p4e11  12902  8p3e11  12907  9p2e11  12913  10p10e20  12921  xnn0n0n1ge2b  13268  0elfz  13765  4fvwrd4  13789  fvinim0ffz  13931  f1resfz0f1d  13934  ssnn0fi  14135  fsuppmapnn0fiubex  14142  exple1  14327  nn0opth2  14423  faclbnd4lem3  14446  bc0k  14462  bcn1  14464  bccl  14473  hasheq0  14514  hashrabrsn  14523  hashbc  14605  fi1uzind  14659  brfi1ind  14661  opfi1ind  14664  iswrdi  14669  wrdnfi  14700  s1f1  14764  s1fv  14766  ccat2s1fst  14795  splfv2a  14913  repsw0  14936  0csh0  14952  cshw1  14981  s2fv0  15046  s3fv0  15051  s4fv0  15055  pfx2  15107  ofs1  15132  relexp0g  15184  relexpaddg  15215  rtrclreclem2  15221  fsumnn0cl  15911  binom  16008  bcxmas  16013  isumnn0nn  16020  climcndslem1  16027  geoser  16045  geomulcvg  16054  risefac0  16202  fallfac0  16203  risefac1  16208  fallfac1  16209  binomfallfaclem2  16215  binomfallfac  16216  bpoly0  16225  bpoly2  16232  bpoly3  16233  bpoly4  16234  fsumcube  16235  ef0lem  16253  ege2le3  16265  ef4p  16290  efgt1p2  16291  efgt1p  16292  ruclem11  16417  nthruz  16430  nn0o  16562  ndvdssub  16588  5ndvds3  16592  bits0  16607  0bits  16618  sadcf  16632  sadc0  16633  sadcaddlem  16636  sadcadd  16637  sadadd2lem  16638  sadadd2  16639  smupf  16657  smup0  16658  smumullem  16671  gcdcl  16685  nn0seqcvgd  16754  algcvg  16760  eucalg  16771  lcmcl  16785  lcmfval  16805  lcmfcl  16812  pclem  17025  pcfac  17086  vdwap0  17163  vdwap1  17164  vdwlem6  17173  hashbc0  17192  0ram  17207  0ramcl  17210  ramz2  17211  ramz  17212  ramcl  17216  prmo0  17223  dec5dvds2  17252  2exp11  17276  2exp16  17277  10nprm  17300  11prm  17302  37prm  17308  43prm  17309  83prm  17310  139prm  17311  163prm  17312  317prm  17313  631prm  17314  1259lem1  17318  1259lem2  17319  1259lem3  17320  1259lem4  17321  1259lem5  17322  2503lem1  17324  2503lem2  17325  2503lem3  17326  2503prm  17327  4001lem1  17328  4001lem2  17329  4001lem3  17330  4001lem4  17331  4001prm  17332  plendxnocndx  17564  slotsdifdsndx  17574  slotsdifunifndx  17581  odrngstr  17583  slotsdifplendx2  17596  imasvalstr  17631  ipostr  18712  gsumws1  19043  cycsubm  19426  psgnunilem2  19718  psgnunilem3  19719  odfval  19755  oddvdsnn0  19767  pgp0  19819  sylow1lem1  19821  cyggex2  20120  telgsums  20216  srgbinomlem3  20463  srgbinomlem4  20464  srgbinom  20466  cnfldstr  21689  nn0subm  21737  expmhm  21751  nn0srg  21752  znf1o  21866  zzngim  21867  cygznlem1  21881  cygznlem2a  21882  cygznlem3  21884  cygth  21886  freshmansdream  21889  snifpsrbag  22237  fczpsrbag  22238  psrbagaddcl  22241  psrlidm  22278  mvrf1  22302  mplcoe3  22356  mplcoe5  22358  ltbwe  22362  psrbag0  22380  psrbagsn  22381  evlslem1  22400  mhpsclcl  22477  mhpmulcl  22479  psdmul  22496  psdmvr  22499  00ply1bas  22566  ply1plusgfvi  22568  coe1sclmul  22610  coe1sclmul2  22612  coe1scl  22615  ply1sclid  22616  cply1coe0bi  22629  ply1scleq  22632  cpm2mf  23079  m2cpminvid2lem  23081  m2cpminvid2  23082  m2cpmfo  23083  decpmatid  23097  pmatcollpw3  23111  pmatcollpw3fi1lem1  23113  pmatcollpwscmatlem1  23116  pmatcollpwscmatlem2  23117  idpm2idmp  23128  chfacfscmulgsum  23187  chfacfpmmulgsum  23191  cpmadugsumlemF  23203  dscmet  24900  ehl0base  25746  ehl0  25747  itgcnlem  26119  dvn0  26253  dvn1  26255  cpncn  26265  dveflem  26308  c1lip2  26327  deg1le0  26438  ply1divex  26464  mon1pid  26481  ply1rem  26493  fta1g  26497  plyconst  26533  plypf1  26540  plyco  26569  0dgr  26573  0dgrb  26574  coefv0  26576  dgreq0  26593  vieta1lem2  26643  vieta1  26644  aareccl  26662  aannenlem2  26665  taylthlem1  26709  radcnv0  26752  abelthlem6  26772  abelthlem9  26776  logtayl  26997  cxp0  27007  cxpeq  27094  leibpilem2  27278  leibpi  27279  log2ublem3  27285  log2ub  27286  log2le1  27287  divsqrtsumlem  27316  dmgmn0  27362  lgambdd  27373  sqff1o  27518  ppiublem2  27539  chtublem  27547  bclbnd  27616  bposlem8  27627  lgsval  27637  dchrisum0flblem1  27844  dchrisum0flb  27846  ostth2lem2  27970  usgrexmplef  29849  usgr0edg0rusgr  30165  usgr2pthlem  30358  wwlksn0s  30459  rusgrnumwwlkb0  30572  erclwwlkref  30620  clwwlkf1  30649  0wlkonlem1  30718  upgr4cycl4dv4e  30795  1kp2ke3k  31056  ex-fac  31061  ex-prmo  31069  nn0min  33462  dpmul1000  33515  dp0h  33518  dpexpp1  33524  dpmul4  33530  threehalves  33531  1mhdrd  33532  s2f1  33560  cshw1s2  33571  cycpm2tr  33730  deg1le0eq0  34155  ply1unit  34157  evl1deg1  34158  evl1deg2  34159  evl1deg3  34160  ply1dg1rt  34162  m1pmeq  34167  psrbasfsupp  34193  mplmulmvr  34221  evlextv  34224  mplvrpmlem  34225  mplvrpmfgalem  34226  mplvrpmga  34227  mplvrpmmhm  34228  mplvrpmrhm  34229  psrmonprod  34234  esplyfval0  34246  esplylem  34248  esplyfv1  34251  esplyfval1  34255  esplyfvaln  34256  esplyind  34257  vietalem  34261  vieta  34262  minplyirredlem  34392  rtelextdg2lem  34408  fldext2chn  34410  constraddcl  34444  constrnegcl  34445  constrdircl  34447  constrremulcl  34449  2sqr3minply  34462  lmatcl  34498  lmat22e12  34501  lmat22e21  34502  fsumcvg4  34632  oddpwdc  35036  eulerpartlems  35042  eulerpartlemb  35050  eulerpartlemt  35053  eulerpartgbij  35054  eulerpartlemmf  35057  eulerpartlemgf  35061  eulerpartlemgs2  35062  eulerpartlemn  35063  fib0  35081  fib1  35082  fibp1  35083  ofcs1  35226  signsply0  35230  signsvvf  35258  prodfzo03  35282  repr0  35290  breprexp  35312  hgt750lemd  35327  hgt750lem  35330  hgt750lem2  35331  hgt750leme  35337  tgoldbachgtde  35339  usgrgt2cycl  35989  subfac0  36032  subfacval2  36042  subfaclim  36043  cvmliftlem7  36146  cvmliftlem13  36151  bccolsum  36600  fwddifn0  37025  heiborlem4  38857  heiborlem10  38863  12gcd5e1  43162  60gcd6e6  43163  60gcd7e1  43164  420gcd8e4  43165  12lcm5e60  43167  60lcm7e420  43169  420lcm8e840  43170  lcmineqlem  43211  3exp7  43212  3lexlogpow5ineq1  43213  3lexlogpow5ineq2  43214  3lexlogpow5ineq5  43219  aks4d1p1  43235  aks6d1c2lem4  43286  aks6d1c2  43289  sticksstones11  43315  sticksstones22  43327  aks6d1c7lem1  43339  25or6to4  43365  sqn5i  43451  decpmul  43454  sqdeccom12  43455  sq3deccom12  43456  235t711  43471  ex-decpmul  43472  mhphflem  43733  0prjspn  43773  sum9cubes  43792  nacsfix  43832  diophrw  43879  pell1qr1  43987  monotoddzzfi  44058  jm2.23  44112  hbtlem5  44239  mncn0  44250  aaitgo  44273  brfvrcld  44800  corclrcl  44816  dfrtrcl3  44842  fvrtrcllb0d  44844  fvrtrcllb0da  44845  corcltrcl  44848  cotrclrcl  44851  k0004val0  45263  bccn0  45436  bccn1  45437  binomcxplemradcnv  45445  binomcxplemnotnn0  45449  rexanuz2nf  46610  dvnmul  47061  dvnprodlem3  47066  wallispilem2  47184  wallispi2lem2  47190  stirlinglem5  47196  stirlinglem7  47198  fourierdlem83  47307  fourierdlem112  47336  fouriersw  47349  elaa2lem  47351  elaa2  47352  etransclem48  47400  etransc  47401  iccelpart  48623  fmtno0  48733  fmtnorec2  48736  fmtno5lem1  48746  fmtno5lem2  48747  fmtno5lem4  48749  257prm  48754  fmtnofac2  48762  fmtnofac1  48763  fmtno4prmfac  48765  fmtno4nprmfac193  48767  fmtno5faclem1  48772  fmtno5faclem2  48773  fmtno5faclem3  48774  fmtno5fac  48775  fmtno5nprm  48776  139prmALT  48789  31prm  48790  127prm  48792  m11nprm  48794  bits0ALTV  48885  2exp340mod341  48939  nfermltl2rev  48949  evengpoap3  49005  tgoldbachlt  49022  tgoldbach  49023  stgr0  49166  usgrexmpl1lem  49227  usgrexmpl2lem  49232  gpgprismgr4cycllem6  49306  gpgprismgr4cycllem7  49307  gpgprismgr4cycllem10  49310  nn0mnd  49384  ssnn0ssfz  49569  dig1  49828  0dig2nn0e  49832  0dig2nn0o  49833  0aryfvalel  49854  itcoval0  49882  itcoval1  49883  ackval0  49900  ackval1  49901  ackvalsuc0val  49907  ackval0012  49909  ackval1012  49910  ackval2012  49911  ackval3012  49912  ackval41a  49914