Theorem 0nn0 12534

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 2765	. 2 ⊢ 0 = 0
2		elnn0 12521	. . . 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 2146  0cc0 11115  ℕcn 12248  ℕ₀cn0 12519

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-mulcl 11177  ax-i2m1 11183

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-n0 12520

This theorem is used by:  0xnn0  12598  0nn0m1nnn0  12666  nn0ind-raph  12712  10nn0  12749  declei  12768  numlti  12769  nummul1c  12781  decaddc2  12788  decrmanc  12789  decrmac  12790  decaddm10  12791  decaddi  12792  decaddci  12793  decaddci2  12794  decmul1  12796  decmulnc  12799  6p5e11  12805  7p4e11  12808  8p3e11  12813  9p2e11  12819  10p10e20  12827  xnn0n0n1ge2b  13173  0elfz  13669  4fvwrd4  13693  fvinim0ffz  13835  f1resfz0f1d  13838  ssnn0fi  14039  fsuppmapnn0fiubex  14046  exple1  14231  nn0opth2  14326  faclbnd4lem3  14349  bc0k  14365  bcn1  14367  bccl  14376  hasheq0  14417  hashrabrsn  14426  hashbc  14508  fi1uzind  14562  brfi1ind  14564  opfi1ind  14567  iswrdi  14572  wrdnfi  14603  s1f1  14666  s1fv  14668  ccat2s1fst  14697  splfv2a  14815  repsw0  14838  0csh0  14854  cshw1  14883  s2fv0  14948  s3fv0  14952  s4fv0  14956  pfx2  15008  ofs1  15031  relexp0g  15083  relexpaddg  15114  rtrclreclem2  15120  fsumnn0cl  15810  binom  15907  bcxmas  15912  isumnn0nn  15919  climcndslem1  15926  geoser  15944  geomulcvg  15953  risefac0  16103  fallfac0  16104  risefac1  16109  fallfac1  16110  binomfallfaclem2  16116  binomfallfac  16117  bpoly0  16126  bpoly2  16133  bpoly3  16134  bpoly4  16135  fsumcube  16136  ef0lem  16154  ege2le3  16166  ef4p  16191  efgt1p2  16192  efgt1p  16193  ruclem11  16318  nthruz  16331  nn0o  16463  ndvdssub  16489  5ndvds3  16493  bits0  16508  0bits  16519  sadcf  16533  sadc0  16534  sadcaddlem  16537  sadcadd  16538  sadadd2lem  16539  sadadd2  16540  smupf  16558  smup0  16559  smumullem  16572  gcdcl  16586  nn0seqcvgd  16650  algcvg  16656  eucalg  16667  lcmcl  16681  lcmfval  16701  lcmfcl  16708  pclem  16920  pcfac  16981  vdwap0  17058  vdwap1  17059  vdwlem6  17068  hashbc0  17087  0ram  17102  0ramcl  17105  ramz2  17106  ramz  17107  ramcl  17111  prmo0  17118  dec5dvds2  17147  2exp11  17171  2exp16  17172  10nprm  17195  11prm  17197  37prm  17203  43prm  17204  83prm  17205  139prm  17206  163prm  17207  317prm  17208  631prm  17209  1259lem1  17213  1259lem2  17214  1259lem3  17215  1259lem4  17216  1259lem5  17217  2503lem1  17219  2503lem2  17220  2503lem3  17221  2503prm  17222  4001lem1  17223  4001lem2  17224  4001lem3  17225  4001lem4  17226  4001prm  17227  plendxnocndx  17459  slotsdifdsndx  17469  slotsdifunifndx  17476  odrngstr  17478  slotsdifplendx2  17491  imasvalstr  17526  ipostr  18607  gsumws1  18934  cycsubm  19317  psgnunilem2  19609  psgnunilem3  19610  odfval  19646  oddvdsnn0  19658  pgp0  19710  sylow1lem1  19712  cyggex2  20011  telgsums  20107  srgbinomlem3  20354  srgbinomlem4  20355  srgbinom  20357  cnfldstr  21574  nn0subm  21622  expmhm  21636  nn0srg  21637  znf1o  21751  zzngim  21752  cygznlem1  21766  cygznlem2a  21767  cygznlem3  21769  cygth  21771  freshmansdream  21774  snifpsrbag  22120  fczpsrbag  22121  psrbagaddcl  22124  psrlidm  22161  mvrf1  22185  mplcoe3  22239  mplcoe5  22241  ltbwe  22245  psrbag0  22263  psrbagsn  22264  evlslem1  22283  mhpsclcl  22360  mhpmulcl  22362  psdmul  22379  psdmvr  22382  00ply1bas  22449  ply1plusgfvi  22451  coe1sclmul  22493  coe1sclmul2  22495  coe1scl  22498  ply1sclid  22499  cply1coe0bi  22512  ply1scleq  22515  cpm2mf  22959  m2cpminvid2lem  22961  m2cpminvid2  22962  m2cpmfo  22963  decpmatid  22977  pmatcollpw3  22991  pmatcollpw3fi1lem1  22993  pmatcollpwscmatlem1  22996  pmatcollpwscmatlem2  22997  idpm2idmp  23008  chfacfscmulgsum  23067  chfacfpmmulgsum  23071  cpmadugsumlemF  23083  dscmet  24780  ehl0base  25626  ehl0  25627  itgcnlem  26000  dvn0  26134  dvn1  26136  cpncn  26146  dveflem  26189  c1lip2  26208  deg1le0  26319  ply1divex  26345  mon1pid  26362  ply1rem  26374  fta1g  26378  plyconst  26414  plypf1  26420  plyco  26449  0dgr  26453  0dgrb  26454  coefv0  26456  dgreq0  26473  vieta1lem2  26523  vieta1  26524  aareccl  26540  aannenlem2  26543  taylthlem1  26587  radcnv0  26630  abelthlem6  26650  abelthlem9  26654  logtayl  26876  cxp0  26886  cxpeq  26973  leibpilem2  27157  leibpi  27158  log2ublem3  27164  log2ub  27165  log2le1  27166  divsqrtsumlem  27195  dmgmn0  27241  lgambdd  27252  sqff1o  27397  ppiublem2  27418  chtublem  27426  bclbnd  27495  bposlem8  27506  lgsval  27516  dchrisum0flblem1  27723  dchrisum0flb  27725  ostth2lem2  27849  usgrexmplef  29667  usgr0edg0rusgr  29983  usgr2pthlem  30176  wwlksn0s  30277  rusgrnumwwlkb0  30390  erclwwlkref  30438  clwwlkf1  30467  0wlkonlem1  30536  upgr4cycl4dv4e  30607  1kp2ke3k  30868  ex-fac  30873  ex-prmo  30881  nn0min  33235  dpmul1000  33288  dp0h  33291  dpexpp1  33297  dpmul4  33303  threehalves  33304  1mhdrd  33305  s2f1  33333  cshw1s2  33344  cycpm2tr  33503  deg1le0eq0  33927  ply1unit  33929  evl1deg1  33930  evl1deg2  33931  evl1deg3  33932  ply1dg1rt  33934  m1pmeq  33939  psrbasfsupp  33965  mplmulmvr  33993  evlextv  33996  mplvrpmlem  33997  mplvrpmfgalem  33998  mplvrpmga  33999  mplvrpmmhm  34000  mplvrpmrhm  34001  psrmonprod  34006  esplyfval0  34018  esplylem  34020  esplyfv1  34023  esplyfval1  34027  esplyfvaln  34028  esplyind  34029  vietalem  34033  vieta  34034  minplyirredlem  34164  rtelextdg2lem  34180  fldext2chn  34182  constraddcl  34216  constrnegcl  34217  constrdircl  34219  constrremulcl  34221  2sqr3minply  34234  lmatcl  34270  lmat22e12  34273  lmat22e21  34274  fsumcvg4  34404  oddpwdc  34809  eulerpartlems  34815  eulerpartlemb  34823  eulerpartlemt  34826  eulerpartgbij  34827  eulerpartlemmf  34830  eulerpartlemgf  34834  eulerpartlemgs2  34835  eulerpartlemn  34836  fib0  34854  fib1  34855  fibp1  34856  ofcs1  34999  signsply0  35003  signsvvf  35031  prodfzo03  35055  repr0  35063  breprexp  35085  hgt750lemd  35100  hgt750lem  35103  hgt750lem2  35104  hgt750leme  35110  tgoldbachgtde  35112  usgrgt2cycl  35667  subfac0  35706  subfacval2  35716  subfaclim  35717  cvmliftlem7  35820  cvmliftlem13  35825  bccolsum  36268  fwddifn0  36693  heiborlem4  38523  heiborlem10  38529  12gcd5e1  42828  60gcd6e6  42829  60gcd7e1  42830  420gcd8e4  42831  12lcm5e60  42833  60lcm7e420  42835  420lcm8e840  42836  lcmineqlem  42877  3exp7  42878  3lexlogpow5ineq1  42879  3lexlogpow5ineq2  42880  3lexlogpow5ineq5  42885  aks4d1p1  42901  aks6d1c2lem4  42952  aks6d1c2  42955  sticksstones11  42981  sticksstones22  42993  aks6d1c7lem1  43005  25or6to4  43031  sqn5i  43104  decpmul  43107  sqdeccom12  43108  sq3deccom12  43109  235t711  43124  ex-decpmul  43125  mhphflem  43386  0prjspn  43418  sum9cubes  43462  nacsfix  43501  diophrw  43548  pell1qr1  43656  monotoddzzfi  43727  jm2.23  43781  hbtlem5  43913  mncn0  43924  aaitgo  43947  brfvrcld  44475  corclrcl  44491  dfrtrcl3  44517  fvrtrcllb0d  44519  fvrtrcllb0da  44520  corcltrcl  44523  cotrclrcl  44526  k0004val0  44938  bccn0  45111  bccn1  45112  binomcxplemradcnv  45120  binomcxplemnotnn0  45124  rexanuz2nf  46264  dvnmul  46715  dvnprodlem3  46720  wallispilem2  46838  wallispi2lem2  46844  stirlinglem5  46850  stirlinglem7  46852  fourierdlem83  46961  fourierdlem112  46990  fouriersw  47003  elaa2lem  47005  elaa2  47006  etransclem48  47054  etransc  47055  iccelpart  48240  fmtno0  48350  fmtnorec2  48353  fmtno5lem1  48363  fmtno5lem2  48364  fmtno5lem4  48366  257prm  48371  fmtnofac2  48379  fmtnofac1  48380  fmtno4prmfac  48382  fmtno4nprmfac193  48384  fmtno5faclem1  48389  fmtno5faclem2  48390  fmtno5faclem3  48391  fmtno5fac  48392  fmtno5nprm  48393  139prmALT  48406  31prm  48407  127prm  48409  m11nprm  48411  bits0ALTV  48502  2exp340mod341  48556  nfermltl2rev  48566  evengpoap3  48622  tgoldbachlt  48639  tgoldbach  48640  stgr0  48783  usgrexmpl1lem  48844  usgrexmpl2lem  48849  gpgprismgr4cycllem6  48923  gpgprismgr4cycllem7  48924  gpgprismgr4cycllem10  48927  nn0mnd  49001  ssnn0ssfz  49186  dig1  49445  0dig2nn0e  49449  0dig2nn0o  49450  0aryfvalel  49471  itcoval0  49499  itcoval1  49500  ackval0  49517  ackval1  49518  ackvalsuc0val  49524  ackval0012  49526  ackval1012  49527  ackval2012  49528  ackval3012  49529  ackval41a  49531