Theorem 0nn0 12543

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 12530	. . . 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 11124  ℕcn 12257  ℕ₀cn0 12528

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 2732  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-mulcl 11186  ax-i2m1 11192

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-n0 12529

This theorem is used by:  0xnn0  12607  0nn0m1nnn0  12675  nn0ind-raph  12721  10nn0  12758  declei  12777  numlti  12778  nummul1c  12790  decaddc2  12797  decrmanc  12798  decrmac  12799  decaddm10  12800  decaddi  12801  decaddci  12802  decaddci2  12803  decmul1  12805  decmulnc  12808  6p5e11  12814  7p4e11  12817  8p3e11  12822  9p2e11  12828  10p10e20  12836  xnn0n0n1ge2b  13183  0elfz  13679  4fvwrd4  13703  fvinim0ffz  13845  f1resfz0f1d  13848  ssnn0fi  14049  fsuppmapnn0fiubex  14056  exple1  14241  nn0opth2  14336  faclbnd4lem3  14359  bc0k  14375  bcn1  14377  bccl  14386  hasheq0  14427  hashrabrsn  14436  hashbc  14518  fi1uzind  14572  brfi1ind  14574  opfi1ind  14577  iswrdi  14582  wrdnfi  14613  s1f1  14676  s1fv  14678  ccat2s1fst  14707  splfv2a  14825  repsw0  14848  0csh0  14864  cshw1  14893  s2fv0  14958  s3fv0  14962  s4fv0  14966  pfx2  15018  ofs1  15043  relexp0g  15095  relexpaddg  15126  rtrclreclem2  15132  fsumnn0cl  15822  binom  15919  bcxmas  15924  isumnn0nn  15931  climcndslem1  15938  geoser  15956  geomulcvg  15965  risefac0  16113  fallfac0  16114  risefac1  16119  fallfac1  16120  binomfallfaclem2  16126  binomfallfac  16127  bpoly0  16136  bpoly2  16143  bpoly3  16144  bpoly4  16145  fsumcube  16146  ef0lem  16164  ege2le3  16176  ef4p  16201  efgt1p2  16202  efgt1p  16203  ruclem11  16328  nthruz  16341  nn0o  16473  ndvdssub  16499  5ndvds3  16503  bits0  16518  0bits  16529  sadcf  16543  sadc0  16544  sadcaddlem  16547  sadcadd  16548  sadadd2lem  16549  sadadd2  16550  smupf  16568  smup0  16569  smumullem  16582  gcdcl  16596  nn0seqcvgd  16660  algcvg  16666  eucalg  16677  lcmcl  16691  lcmfval  16711  lcmfcl  16718  pclem  16930  pcfac  16991  vdwap0  17068  vdwap1  17069  vdwlem6  17078  hashbc0  17097  0ram  17112  0ramcl  17115  ramz2  17116  ramz  17117  ramcl  17121  prmo0  17128  dec5dvds2  17157  2exp11  17181  2exp16  17182  10nprm  17205  11prm  17207  37prm  17213  43prm  17214  83prm  17215  139prm  17216  163prm  17217  317prm  17218  631prm  17219  1259lem1  17223  1259lem2  17224  1259lem3  17225  1259lem4  17226  1259lem5  17227  2503lem1  17229  2503lem2  17230  2503lem3  17231  2503prm  17232  4001lem1  17233  4001lem2  17234  4001lem3  17235  4001lem4  17236  4001prm  17237  plendxnocndx  17469  slotsdifdsndx  17479  slotsdifunifndx  17486  odrngstr  17488  slotsdifplendx2  17501  imasvalstr  17536  ipostr  18617  gsumws1  18947  cycsubm  19330  psgnunilem2  19622  psgnunilem3  19623  odfval  19659  oddvdsnn0  19671  pgp0  19723  sylow1lem1  19725  cyggex2  20024  telgsums  20120  srgbinomlem3  20367  srgbinomlem4  20368  srgbinom  20370  cnfldstr  21587  nn0subm  21635  expmhm  21649  nn0srg  21650  znf1o  21764  zzngim  21765  cygznlem1  21779  cygznlem2a  21780  cygznlem3  21782  cygth  21784  freshmansdream  21787  snifpsrbag  22135  fczpsrbag  22136  psrbagaddcl  22139  psrlidm  22176  mvrf1  22200  mplcoe3  22254  mplcoe5  22256  ltbwe  22260  psrbag0  22278  psrbagsn  22279  evlslem1  22298  mhpsclcl  22375  mhpmulcl  22377  psdmul  22394  psdmvr  22397  00ply1bas  22464  ply1plusgfvi  22466  coe1sclmul  22508  coe1sclmul2  22510  coe1scl  22513  ply1sclid  22514  cply1coe0bi  22527  ply1scleq  22530  cpm2mf  22977  m2cpminvid2lem  22979  m2cpminvid2  22980  m2cpmfo  22981  decpmatid  22995  pmatcollpw3  23009  pmatcollpw3fi1lem1  23011  pmatcollpwscmatlem1  23014  pmatcollpwscmatlem2  23015  idpm2idmp  23026  chfacfscmulgsum  23085  chfacfpmmulgsum  23089  cpmadugsumlemF  23101  dscmet  24798  ehl0base  25644  ehl0  25645  itgcnlem  26017  dvn0  26151  dvn1  26153  cpncn  26163  dveflem  26206  c1lip2  26225  deg1le0  26336  ply1divex  26362  mon1pid  26379  ply1rem  26391  fta1g  26395  plyconst  26431  plypf1  26438  plyco  26467  0dgr  26471  0dgrb  26472  coefv0  26474  dgreq0  26491  vieta1lem2  26543  vieta1  26544  aareccl  26562  aannenlem2  26565  taylthlem1  26609  radcnv0  26652  abelthlem6  26672  abelthlem9  26676  logtayl  26897  cxp0  26907  cxpeq  26994  leibpilem2  27178  leibpi  27179  log2ublem3  27185  log2ub  27186  log2le1  27187  divsqrtsumlem  27216  dmgmn0  27262  lgambdd  27273  sqff1o  27418  ppiublem2  27439  chtublem  27447  bclbnd  27516  bposlem8  27527  lgsval  27537  dchrisum0flblem1  27744  dchrisum0flb  27746  ostth2lem2  27870  usgrexmplef  29719  usgr0edg0rusgr  30035  usgr2pthlem  30228  wwlksn0s  30329  rusgrnumwwlkb0  30442  erclwwlkref  30490  clwwlkf1  30519  0wlkonlem1  30588  upgr4cycl4dv4e  30665  1kp2ke3k  30926  ex-fac  30931  ex-prmo  30939  nn0min  33291  dpmul1000  33344  dp0h  33347  dpexpp1  33353  dpmul4  33359  threehalves  33360  1mhdrd  33361  s2f1  33389  cshw1s2  33400  cycpm2tr  33559  deg1le0eq0  33983  ply1unit  33985  evl1deg1  33986  evl1deg2  33987  evl1deg3  33988  ply1dg1rt  33990  m1pmeq  33995  psrbasfsupp  34021  mplmulmvr  34049  evlextv  34052  mplvrpmlem  34053  mplvrpmfgalem  34054  mplvrpmga  34055  mplvrpmmhm  34056  mplvrpmrhm  34057  psrmonprod  34062  esplyfval0  34074  esplylem  34076  esplyfv1  34079  esplyfval1  34083  esplyfvaln  34084  esplyind  34085  vietalem  34089  vieta  34090  minplyirredlem  34220  rtelextdg2lem  34236  fldext2chn  34238  constraddcl  34272  constrnegcl  34273  constrdircl  34275  constrremulcl  34277  2sqr3minply  34290  lmatcl  34326  lmat22e12  34329  lmat22e21  34330  fsumcvg4  34460  oddpwdc  34865  eulerpartlems  34871  eulerpartlemb  34879  eulerpartlemt  34882  eulerpartgbij  34883  eulerpartlemmf  34886  eulerpartlemgf  34890  eulerpartlemgs2  34891  eulerpartlemn  34892  fib0  34910  fib1  34911  fibp1  34912  ofcs1  35055  signsply0  35059  signsvvf  35087  prodfzo03  35111  repr0  35119  breprexp  35141  hgt750lemd  35156  hgt750lem  35159  hgt750lem2  35160  hgt750leme  35166  tgoldbachgtde  35168  usgrgt2cycl  35723  subfac0  35756  subfacval2  35766  subfaclim  35767  cvmliftlem7  35870  cvmliftlem13  35875  bccolsum  36318  fwddifn0  36744  heiborlem4  38564  heiborlem10  38570  12gcd5e1  42869  60gcd6e6  42870  60gcd7e1  42871  420gcd8e4  42872  12lcm5e60  42874  60lcm7e420  42876  420lcm8e840  42877  lcmineqlem  42918  3exp7  42919  3lexlogpow5ineq1  42920  3lexlogpow5ineq2  42921  3lexlogpow5ineq5  42926  aks4d1p1  42942  aks6d1c2lem4  42993  aks6d1c2  42996  sticksstones11  43022  sticksstones22  43034  aks6d1c7lem1  43046  25or6to4  43072  sqn5i  43160  decpmul  43163  sqdeccom12  43164  sq3deccom12  43165  235t711  43180  ex-decpmul  43181  mhphflem  43442  0prjspn  43474  sum9cubes  43518  nacsfix  43557  diophrw  43604  pell1qr1  43712  monotoddzzfi  43783  jm2.23  43837  hbtlem5  43969  mncn0  43980  aaitgo  44003  brfvrcld  44531  corclrcl  44547  dfrtrcl3  44573  fvrtrcllb0d  44575  fvrtrcllb0da  44576  corcltrcl  44579  cotrclrcl  44582  k0004val0  44994  bccn0  45167  bccn1  45168  binomcxplemradcnv  45176  binomcxplemnotnn0  45180  rexanuz2nf  46320  dvnmul  46771  dvnprodlem3  46776  wallispilem2  46894  wallispi2lem2  46900  stirlinglem5  46906  stirlinglem7  46908  fourierdlem83  47017  fourierdlem112  47046  fouriersw  47059  elaa2lem  47061  elaa2  47062  etransclem48  47110  etransc  47111  iccelpart  48333  fmtno0  48443  fmtnorec2  48446  fmtno5lem1  48456  fmtno5lem2  48457  fmtno5lem4  48459  257prm  48464  fmtnofac2  48472  fmtnofac1  48473  fmtno4prmfac  48475  fmtno4nprmfac193  48477  fmtno5faclem1  48482  fmtno5faclem2  48483  fmtno5faclem3  48484  fmtno5fac  48485  fmtno5nprm  48486  139prmALT  48499  31prm  48500  127prm  48502  m11nprm  48504  bits0ALTV  48595  2exp340mod341  48649  nfermltl2rev  48659  evengpoap3  48715  tgoldbachlt  48732  tgoldbach  48733  stgr0  48876  usgrexmpl1lem  48937  usgrexmpl2lem  48942  gpgprismgr4cycllem6  49016  gpgprismgr4cycllem7  49017  gpgprismgr4cycllem10  49020  nn0mnd  49094  ssnn0ssfz  49279  dig1  49538  0dig2nn0e  49542  0dig2nn0o  49543  0aryfvalel  49564  itcoval0  49592  itcoval1  49593  ackval0  49610  ackval1  49611  ackvalsuc0val  49617  ackval0012  49619  ackval1012  49620  ackval2012  49621  ackval3012  49622  ackval41a  49624