Theorem 0nn0 12178

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 2738	. 2 ⊢ 0 = 0
2		elnn0 12165	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 227	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 872	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 843   = wceq 1539   ∈ wcel 2108  0cc0 10802  ℕcn 11903  ℕ₀cn0 12163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-i2m1 10870

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-n0 12164

This theorem is referenced by:  0xnn0  12241  nn0ind-raph  12350  10nn0  12384  declei  12402  numlti  12403  nummul1c  12415  decaddc2  12422  decrmanc  12423  decrmac  12424  decaddm10  12425  decaddi  12426  decaddci  12427  decaddci2  12428  decmul1  12430  decmulnc  12433  6p5e11  12439  7p4e11  12442  8p3e11  12447  9p2e11  12453  10p10e20  12461  xnn0n0n1ge2b  12796  0elfz  13282  4fvwrd4  13305  fvinim0ffz  13434  ssnn0fi  13633  fsuppmapnn0fiubex  13640  exple1  13822  nn0opth2  13914  faclbnd4lem3  13937  bc0k  13953  bcn1  13955  bccl  13964  hasheq0  14006  hashrabrsn  14015  hashbc  14093  fi1uzind  14139  brfi1ind  14141  opfi1ind  14144  iswrdi  14149  wrdnfi  14179  s1fv  14243  ccat2s1fst  14279  ccat2s1fstOLD  14280  splfv2a  14397  repsw0  14418  0csh0  14434  cshw1  14463  s2fv0  14528  s3fv0  14532  s4fv0  14536  pfx2  14588  ofs1  14609  relexp0g  14661  relexpaddg  14692  rtrclreclem2  14698  fsumnn0cl  15376  binom  15470  bcxmas  15475  isumnn0nn  15482  climcndslem1  15489  geoser  15507  geomulcvg  15516  risefac0  15665  fallfac0  15666  risefac1  15671  fallfac1  15672  binomfallfaclem2  15678  binomfallfac  15679  bpoly0  15688  bpoly2  15695  bpoly3  15696  bpoly4  15697  fsumcube  15698  ef0lem  15716  ege2le3  15727  ef4p  15750  efgt1p2  15751  efgt1p  15752  ruclem11  15877  nthruz  15890  nn0o  16020  ndvdssub  16046  bits0  16063  0bits  16074  sadcf  16088  sadc0  16089  sadcaddlem  16092  sadcadd  16093  sadadd2lem  16094  sadadd2  16095  smupf  16113  smup0  16114  smumullem  16127  gcdcl  16141  nn0seqcvgd  16203  algcvg  16209  eucalg  16220  lcmcl  16234  lcmfval  16254  lcmfcl  16261  pclem  16467  pcfac  16528  vdwap0  16605  vdwap1  16606  vdwlem6  16615  hashbc0  16634  0ram  16649  0ramcl  16652  ramz2  16653  ramz  16654  ramcl  16658  prmo0  16665  dec5dvds2  16694  2exp11  16719  2exp16  16720  11prm  16744  37prm  16750  43prm  16751  83prm  16752  139prm  16753  163prm  16754  317prm  16755  631prm  16756  1259lem1  16760  1259lem2  16761  1259lem3  16762  1259lem4  16763  1259lem5  16764  2503lem1  16766  2503lem2  16767  2503lem3  16768  2503prm  16769  4001lem1  16770  4001lem2  16771  4001lem3  16772  4001lem4  16773  4001prm  16774  odrngstr  17032  imasvalstr  17079  ipostr  18162  gsumws1  18391  cycsubm  18736  psgnunilem2  19018  psgnunilem3  19019  odfval  19055  oddvdsnn0  19067  pgp0  19116  sylow1lem1  19118  cyggex2  19413  telgsums  19509  srgbinomlem3  19693  srgbinomlem4  19694  srgbinom  19696  cnfldstr  20512  cnfldfun  20522  nn0subm  20565  expmhm  20579  nn0srg  20580  znf1o  20671  zzngim  20672  cygznlem1  20686  cygznlem2a  20687  cygznlem3  20689  cygth  20691  thlle  20814  snifpsrbag  21035  fczpsrbag  21036  psrbagaddcl  21041  psrlidm  21082  mvrf1  21104  mplcoe3  21149  mplcoe5  21151  ltbwe  21155  psrbag0  21180  psrbagsn  21181  evlslem1  21202  mhpsclcl  21247  mhpmulcl  21249  00ply1bas  21321  ply1plusgfvi  21323  coe1sclmul  21363  coe1sclmul2  21365  coe1scl  21368  ply1sclid  21369  ply1idvr1  21374  cply1coe0bi  21381  cpm2mf  21809  m2cpminvid2lem  21811  m2cpminvid2  21812  m2cpmfo  21813  decpmatid  21827  pmatcollpw3  21841  pmatcollpw3fi1lem1  21843  pmatcollpwscmatlem1  21846  pmatcollpwscmatlem2  21847  idpm2idmp  21858  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  cpmadugsumlemF  21933  dscmet  23634  ehl0base  24485  ehl0  24486  itgcnlem  24859  dvn0  24993  dvn1  24995  cpncn  25005  dveflem  25048  c1lip2  25067  tdeglem4OLD  25130  deg1le0  25181  ply1divex  25206  ply1rem  25233  fta1g  25237  plyconst  25272  plypf1  25278  plyco  25307  0dgr  25311  0dgrb  25312  coefv0  25314  dgreq0  25331  vieta1lem2  25376  vieta1  25377  aareccl  25391  aannenlem2  25394  taylthlem1  25437  radcnv0  25480  abelthlem6  25500  abelthlem9  25504  logtayl  25720  cxp0  25730  cxpeq  25815  leibpilem2  25996  leibpi  25997  log2ublem3  26003  log2ub  26004  log2le1  26005  divsqrtsumlem  26034  dmgmn0  26080  lgambdd  26091  sqff1o  26236  ppiublem2  26256  chtublem  26264  bclbnd  26333  bposlem8  26344  lgsval  26354  dchrisum0flblem1  26561  dchrisum0flb  26563  ostth2lem2  26687  usgrexmplef  27529  usgr0edg0rusgr  27845  usgr2pthlem  28032  wwlksn0s  28127  rusgrnumwwlkb0  28237  erclwwlkref  28285  clwwlkf1  28314  0wlkonlem1  28383  upgr4cycl4dv4e  28450  1kp2ke3k  28711  ex-fac  28716  ex-prmo  28724  nn0min  31036  dpmul1000  31075  dp0h  31078  dpexpp1  31084  dpmul4  31090  threehalves  31091  1mhdrd  31092  s1f1  31119  s2f1  31121  cshw1s2  31134  cycpm2tr  31288  freshmansdream  31386  ply1scleq  31570  lmatcl  31668  lmat22e12  31671  lmat22e21  31672  fsumcvg4  31802  oddpwdc  32221  eulerpartlems  32227  eulerpartlemb  32235  eulerpartlemt  32238  eulerpartgbij  32239  eulerpartlemmf  32242  eulerpartlemgf  32246  eulerpartlemgs2  32247  eulerpartlemn  32248  fib0  32266  fib1  32267  fibp1  32268  ofcs1  32423  signsply0  32430  signsvvf  32458  prodfzo03  32483  repr0  32491  breprexp  32513  hgt750lemd  32528  hgt750lem  32531  hgt750lem2  32532  hgt750leme  32538  tgoldbachgtde  32540  0nn0m1nnn0  32971  f1resfz0f1d  32972  usgrgt2cycl  32992  subfac0  33039  subfacval2  33049  subfaclim  33050  cvmliftlem7  33153  cvmliftlem13  33158  bccolsum  33611  fwddifn0  34393  heiborlem4  35899  heiborlem10  35905  12gcd5e1  39939  60gcd6e6  39940  60gcd7e1  39941  420gcd8e4  39942  12lcm5e60  39944  60lcm7e420  39946  420lcm8e840  39947  lcmineqlem  39988  3exp7  39989  3lexlogpow5ineq1  39990  3lexlogpow5ineq2  39991  3lexlogpow5ineq5  39996  aks4d1p1  40012  sticksstones11  40040  sticksstones22  40052  mhphflem  40207  sqn5i  40234  decpmul  40237  sqdeccom12  40238  sq3deccom12  40239  235t711  40240  ex-decpmul  40241  0prjspn  40386  nacsfix  40450  diophrw  40497  pell1qr1  40609  monotoddzzfi  40680  jm2.23  40734  hbtlem5  40869  mncn0  40880  aaitgo  40903  mon1pid  40946  brfvrcld  41188  corclrcl  41204  dfrtrcl3  41230  fvrtrcllb0d  41232  fvrtrcllb0da  41233  corcltrcl  41236  cotrclrcl  41239  k0004val0  41653  bccn0  41850  bccn1  41851  binomcxplemradcnv  41859  binomcxplemnotnn0  41863  dvnmul  43374  dvnprodlem3  43379  wallispilem2  43497  wallispi2lem2  43503  stirlinglem5  43509  stirlinglem7  43511  fourierdlem83  43620  fourierdlem112  43649  fouriersw  43662  elaa2lem  43664  elaa2  43665  etransclem48  43713  etransc  43714  iccelpart  44773  fmtno0  44880  fmtnorec2  44883  fmtno5lem1  44893  fmtno5lem2  44894  fmtno5lem4  44896  257prm  44901  fmtnofac2  44909  fmtnofac1  44910  fmtno4prmfac  44912  fmtno4nprmfac193  44914  fmtno5faclem1  44919  fmtno5faclem2  44920  fmtno5faclem3  44921  fmtno5fac  44922  fmtno5nprm  44923  139prmALT  44936  31prm  44937  127prm  44939  m11nprm  44941  bits0ALTV  45019  2exp340mod341  45073  nfermltl2rev  45083  evengpoap3  45139  tgoldbachlt  45156  tgoldbach  45157  nn0mnd  45261  ssnn0ssfz  45573  dig1  45842  0dig2nn0e  45846  0dig2nn0o  45847  0aryfvalel  45868  itcoval0  45896  itcoval1  45897  ackval0  45914  ackval1  45915  ackvalsuc0val  45921  ackval0012  45923  ackval1012  45924  ackval2012  45925  ackval3012  45926  ackval41a  45928  prstcleval  46237