Theorem 0nn0 12399

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 2729	. 2 ⊢ 0 = 0
2		elnn0 12386	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 228	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 876	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 847   = wceq 1540   ∈ wcel 2109  0cc0 11009  ℕcn 12128  ℕ₀cn0 12384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-i2m1 11077

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-sn 4578  df-n0 12385

This theorem is referenced by:  0xnn0  12463  nn0ind-raph  12576  10nn0  12609  declei  12627  numlti  12628  nummul1c  12640  decaddc2  12647  decrmanc  12648  decrmac  12649  decaddm10  12650  decaddi  12651  decaddci  12652  decaddci2  12653  decmul1  12655  decmulnc  12658  6p5e11  12664  7p4e11  12667  8p3e11  12672  9p2e11  12678  10p10e20  12686  xnn0n0n1ge2b  13034  0elfz  13527  4fvwrd4  13551  fvinim0ffz  13689  ssnn0fi  13892  fsuppmapnn0fiubex  13899  exple1  14084  nn0opth2  14179  faclbnd4lem3  14202  bc0k  14218  bcn1  14220  bccl  14229  hasheq0  14270  hashrabrsn  14279  hashbc  14360  fi1uzind  14414  brfi1ind  14416  opfi1ind  14419  iswrdi  14424  wrdnfi  14455  s1fv  14517  ccat2s1fst  14546  splfv2a  14662  repsw0  14683  0csh0  14699  cshw1  14728  s2fv0  14794  s3fv0  14798  s4fv0  14802  pfx2  14854  ofs1  14877  relexp0g  14929  relexpaddg  14960  rtrclreclem2  14966  fsumnn0cl  15643  binom  15737  bcxmas  15742  isumnn0nn  15749  climcndslem1  15756  geoser  15774  geomulcvg  15783  risefac0  15934  fallfac0  15935  risefac1  15940  fallfac1  15941  binomfallfaclem2  15947  binomfallfac  15948  bpoly0  15957  bpoly2  15964  bpoly3  15965  bpoly4  15966  fsumcube  15967  ef0lem  15985  ege2le3  15997  ef4p  16022  efgt1p2  16023  efgt1p  16024  ruclem11  16149  nthruz  16162  nn0o  16294  ndvdssub  16320  5ndvds3  16324  bits0  16339  0bits  16350  sadcf  16364  sadc0  16365  sadcaddlem  16368  sadcadd  16369  sadadd2lem  16370  sadadd2  16371  smupf  16389  smup0  16390  smumullem  16403  gcdcl  16417  nn0seqcvgd  16481  algcvg  16487  eucalg  16498  lcmcl  16512  lcmfval  16532  lcmfcl  16539  pclem  16750  pcfac  16811  vdwap0  16888  vdwap1  16889  vdwlem6  16898  hashbc0  16917  0ram  16932  0ramcl  16935  ramz2  16936  ramz  16937  ramcl  16941  prmo0  16948  dec5dvds2  16977  2exp11  17001  2exp16  17002  11prm  17026  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  plendxnocndx  17288  slotsdifdsndx  17298  slotsdifunifndx  17305  odrngstr  17307  slotsdifplendx2  17320  imasvalstr  17355  ipostr  18435  gsumws1  18712  cycsubm  19081  psgnunilem2  19374  psgnunilem3  19375  odfval  19411  oddvdsnn0  19423  pgp0  19475  sylow1lem1  19477  cyggex2  19776  telgsums  19872  srgbinomlem3  20113  srgbinomlem4  20114  srgbinom  20116  cnfldstr  21263  cnfldstrOLD  21278  nn0subm  21329  expmhm  21343  nn0srg  21344  znf1o  21458  zzngim  21459  cygznlem1  21473  cygznlem2a  21474  cygznlem3  21476  cygth  21478  freshmansdream  21481  snifpsrbag  21827  fczpsrbag  21828  psrbagaddcl  21831  psrlidm  21869  mvrf1  21893  mplcoe3  21943  mplcoe5  21945  ltbwe  21949  psrbag0  21967  psrbagsn  21968  evlslem1  21987  mhpsclcl  22032  mhpmulcl  22034  psdmul  22051  psdmvr  22054  00ply1bas  22122  ply1plusgfvi  22124  coe1sclmul  22166  coe1sclmul2  22168  coe1scl  22171  ply1sclid  22172  ply1idvr1OLD  22180  cply1coe0bi  22187  ply1scleq  22190  cpm2mf  22637  m2cpminvid2lem  22639  m2cpminvid2  22640  m2cpmfo  22641  decpmatid  22655  pmatcollpw3  22669  pmatcollpw3fi1lem1  22671  pmatcollpwscmatlem1  22674  pmatcollpwscmatlem2  22675  idpm2idmp  22686  chfacfscmulgsum  22745  chfacfpmmulgsum  22749  cpmadugsumlemF  22761  dscmet  24458  ehl0base  25314  ehl0  25315  itgcnlem  25689  dvn0  25824  dvn1  25826  cpncn  25836  dveflem  25881  c1lip2  25901  deg1le0  26014  ply1divex  26040  mon1pid  26057  ply1rem  26069  fta1g  26073  plyconst  26109  plypf1  26115  plyco  26144  0dgr  26148  0dgrb  26149  coefv0  26151  dgreq0  26169  vieta1lem2  26217  vieta1  26218  aareccl  26232  aannenlem2  26235  taylthlem1  26279  radcnv0  26323  abelthlem6  26344  abelthlem9  26348  logtayl  26567  cxp0  26577  cxpeq  26665  leibpilem2  26849  leibpi  26850  log2ublem3  26856  log2ub  26857  log2le1  26858  divsqrtsumlem  26888  dmgmn0  26934  lgambdd  26945  sqff1o  27090  ppiublem2  27112  chtublem  27120  bclbnd  27189  bposlem8  27200  lgsval  27210  dchrisum0flblem1  27417  dchrisum0flb  27419  ostth2lem2  27543  usgrexmplef  29204  usgr0edg0rusgr  29521  usgr2pthlem  29708  wwlksn0s  29806  rusgrnumwwlkb0  29916  erclwwlkref  29964  clwwlkf1  29993  0wlkonlem1  30062  upgr4cycl4dv4e  30129  1kp2ke3k  30390  ex-fac  30395  ex-prmo  30403  nn0min  32765  dpmul1000  32839  dp0h  32842  dpexpp1  32848  dpmul4  32854  threehalves  32855  1mhdrd  32856  s1f1  32884  s2f1  32886  cshw1s2  32902  cycpm2tr  33061  deg1le0eq0  33508  ply1unit  33510  evl1deg1  33511  evl1deg2  33512  evl1deg3  33513  ply1dg1rt  33515  m1pmeq  33519  psrbasfsupp  33544  mplvrpmfgalem  33545  mplvrpmga  33546  minplyirredlem  33677  rtelextdg2lem  33693  fldext2chn  33695  constraddcl  33729  constrnegcl  33730  constrdircl  33732  constrremulcl  33734  2sqr3minply  33747  lmatcl  33783  lmat22e12  33786  lmat22e21  33787  fsumcvg4  33917  oddpwdc  34322  eulerpartlems  34328  eulerpartlemb  34336  eulerpartlemt  34339  eulerpartgbij  34340  eulerpartlemmf  34343  eulerpartlemgf  34347  eulerpartlemgs2  34348  eulerpartlemn  34349  fib0  34367  fib1  34368  fibp1  34369  ofcs1  34512  signsply0  34519  signsvvf  34547  prodfzo03  34571  repr0  34579  breprexp  34601  hgt750lemd  34616  hgt750lem  34619  hgt750lem2  34620  hgt750leme  34626  tgoldbachgtde  34628  0nn0m1nnn0  35086  f1resfz0f1d  35087  usgrgt2cycl  35103  subfac0  35150  subfacval2  35160  subfaclim  35161  cvmliftlem7  35264  cvmliftlem13  35269  bccolsum  35712  fwddifn0  36138  heiborlem4  37794  heiborlem10  37800  12gcd5e1  41976  60gcd6e6  41977  60gcd7e1  41978  420gcd8e4  41979  12lcm5e60  41981  60lcm7e420  41983  420lcm8e840  41984  lcmineqlem  42025  3exp7  42026  3lexlogpow5ineq1  42027  3lexlogpow5ineq2  42028  3lexlogpow5ineq5  42033  aks4d1p1  42049  aks6d1c2lem4  42100  aks6d1c2  42103  sticksstones11  42129  sticksstones22  42141  aks6d1c7lem1  42153  sqn5i  42258  decpmul  42261  sqdeccom12  42262  sq3deccom12  42263  235t711  42278  ex-decpmul  42279  mhphflem  42569  0prjspn  42601  sum9cubes  42645  nacsfix  42685  diophrw  42732  pell1qr1  42844  monotoddzzfi  42915  jm2.23  42969  hbtlem5  43101  mncn0  43112  aaitgo  43135  brfvrcld  43664  corclrcl  43680  dfrtrcl3  43706  fvrtrcllb0d  43708  fvrtrcllb0da  43709  corcltrcl  43712  cotrclrcl  43715  k0004val0  44127  bccn0  44316  bccn1  44317  binomcxplemradcnv  44325  binomcxplemnotnn0  44329  rexanuz2nf  45471  dvnmul  45924  dvnprodlem3  45929  wallispilem2  46047  wallispi2lem2  46053  stirlinglem5  46059  stirlinglem7  46061  fourierdlem83  46170  fourierdlem112  46199  fouriersw  46212  elaa2lem  46214  elaa2  46215  etransclem48  46263  etransc  46264  iccelpart  47417  fmtno0  47524  fmtnorec2  47527  fmtno5lem1  47537  fmtno5lem2  47538  fmtno5lem4  47540  257prm  47545  fmtnofac2  47553  fmtnofac1  47554  fmtno4prmfac  47556  fmtno4nprmfac193  47558  fmtno5faclem1  47563  fmtno5faclem2  47564  fmtno5faclem3  47565  fmtno5fac  47566  fmtno5nprm  47567  139prmALT  47580  31prm  47581  127prm  47583  m11nprm  47585  bits0ALTV  47663  2exp340mod341  47717  nfermltl2rev  47727  evengpoap3  47783  tgoldbachlt  47800  tgoldbach  47801  stgr0  47944  usgrexmpl1lem  48005  usgrexmpl2lem  48010  gpgprismgr4cycllem6  48084  gpgprismgr4cycllem7  48085  gpgprismgr4cycllem10  48088  nn0mnd  48163  ssnn0ssfz  48333  dig1  48593  0dig2nn0e  48597  0dig2nn0o  48598  0aryfvalel  48619  itcoval0  48647  itcoval1  48648  ackval0  48665  ackval1  48666  ackvalsuc0val  48672  ackval0012  48674  ackval1012  48675  ackval2012  48676  ackval3012  48677  ackval41a  48679