Theorem 0nn0 12614

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 2761	. 2 ⊢ 0 = 0
2		elnn0 12601	. . . 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 11193  ℕcn 12328  ℕ₀cn0 12599

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 2733  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-mulcl 11255  ax-i2m1 11261

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-n0 12600

This theorem is used by:  0xnn0  12678  0nn0m1nnn0  12746  nn0ind-raph  12792  10nn0  12829  declei  12848  numlti  12849  nummul1c  12861  decaddc2  12868  decrmanc  12869  decrmac  12870  decaddm10  12871  decaddi  12872  decaddci  12873  decaddci2  12874  decmul1  12876  decmulnc  12879  6p5e11  12885  7p4e11  12888  8p3e11  12893  9p2e11  12899  10p10e20  12907  xnn0n0n1ge2b  13254  0elfz  13751  4fvwrd4  13775  fvinim0ffz  13917  f1resfz0f1d  13920  ssnn0fi  14121  fsuppmapnn0fiubex  14128  exple1  14313  nn0opth2  14409  faclbnd4lem3  14432  bc0k  14448  bcn1  14450  bccl  14459  hasheq0  14500  hashrabrsn  14509  hashbc  14591  fi1uzind  14645  brfi1ind  14647  opfi1ind  14650  iswrdi  14655  wrdnfi  14686  s1f1  14749  s1fv  14751  ccat2s1fst  14780  splfv2a  14898  repsw0  14921  0csh0  14937  cshw1  14966  s2fv0  15031  s3fv0  15035  s4fv0  15039  pfx2  15091  ofs1  15116  relexp0g  15168  relexpaddg  15199  rtrclreclem2  15205  fsumnn0cl  15895  binom  15992  bcxmas  15997  isumnn0nn  16004  climcndslem1  16011  geoser  16029  geomulcvg  16038  risefac0  16186  fallfac0  16187  risefac1  16192  fallfac1  16193  binomfallfaclem2  16199  binomfallfac  16200  bpoly0  16209  bpoly2  16216  bpoly3  16217  bpoly4  16218  fsumcube  16219  ef0lem  16237  ege2le3  16249  ef4p  16274  efgt1p2  16275  efgt1p  16276  ruclem11  16401  nthruz  16414  nn0o  16546  ndvdssub  16572  5ndvds3  16576  bits0  16591  0bits  16602  sadcf  16616  sadc0  16617  sadcaddlem  16620  sadcadd  16621  sadadd2lem  16622  sadadd2  16623  smupf  16641  smup0  16642  smumullem  16655  gcdcl  16669  nn0seqcvgd  16738  algcvg  16744  eucalg  16755  lcmcl  16769  lcmfval  16789  lcmfcl  16796  pclem  17009  pcfac  17070  vdwap0  17147  vdwap1  17148  vdwlem6  17157  hashbc0  17176  0ram  17191  0ramcl  17194  ramz2  17195  ramz  17196  ramcl  17200  prmo0  17207  dec5dvds2  17236  2exp11  17260  2exp16  17261  10nprm  17284  11prm  17286  37prm  17292  43prm  17293  83prm  17294  139prm  17295  163prm  17296  317prm  17297  631prm  17298  1259lem1  17302  1259lem2  17303  1259lem3  17304  1259lem4  17305  1259lem5  17306  2503lem1  17308  2503lem2  17309  2503lem3  17310  2503prm  17311  4001lem1  17312  4001lem2  17313  4001lem3  17314  4001lem4  17315  4001prm  17316  plendxnocndx  17548  slotsdifdsndx  17558  slotsdifunifndx  17565  odrngstr  17567  slotsdifplendx2  17580  imasvalstr  17615  ipostr  18696  gsumws1  19027  cycsubm  19410  psgnunilem2  19702  psgnunilem3  19703  odfval  19739  oddvdsnn0  19751  pgp0  19803  sylow1lem1  19805  cyggex2  20104  telgsums  20200  srgbinomlem3  20447  srgbinomlem4  20448  srgbinom  20450  cnfldstr  21673  nn0subm  21721  expmhm  21735  nn0srg  21736  znf1o  21850  zzngim  21851  cygznlem1  21865  cygznlem2a  21866  cygznlem3  21868  cygth  21870  freshmansdream  21873  snifpsrbag  22221  fczpsrbag  22222  psrbagaddcl  22225  psrlidm  22262  mvrf1  22286  mplcoe3  22340  mplcoe5  22342  ltbwe  22346  psrbag0  22364  psrbagsn  22365  evlslem1  22384  mhpsclcl  22461  mhpmulcl  22463  psdmul  22480  psdmvr  22483  00ply1bas  22550  ply1plusgfvi  22552  coe1sclmul  22594  coe1sclmul2  22596  coe1scl  22599  ply1sclid  22600  cply1coe0bi  22613  ply1scleq  22616  cpm2mf  23063  m2cpminvid2lem  23065  m2cpminvid2  23066  m2cpmfo  23067  decpmatid  23081  pmatcollpw3  23095  pmatcollpw3fi1lem1  23097  pmatcollpwscmatlem1  23100  pmatcollpwscmatlem2  23101  idpm2idmp  23112  chfacfscmulgsum  23171  chfacfpmmulgsum  23175  cpmadugsumlemF  23187  dscmet  24884  ehl0base  25730  ehl0  25731  itgcnlem  26103  dvn0  26237  dvn1  26239  cpncn  26249  dveflem  26292  c1lip2  26311  deg1le0  26422  ply1divex  26448  mon1pid  26465  ply1rem  26477  fta1g  26481  plyconst  26517  plypf1  26524  plyco  26553  0dgr  26557  0dgrb  26558  coefv0  26560  dgreq0  26577  vieta1lem2  26627  vieta1  26628  aareccl  26646  aannenlem2  26649  taylthlem1  26693  radcnv0  26736  abelthlem6  26756  abelthlem9  26760  logtayl  26981  cxp0  26991  cxpeq  27078  leibpilem2  27262  leibpi  27263  log2ublem3  27269  log2ub  27270  log2le1  27271  divsqrtsumlem  27300  dmgmn0  27346  lgambdd  27357  sqff1o  27502  ppiublem2  27523  chtublem  27531  bclbnd  27600  bposlem8  27611  lgsval  27621  dchrisum0flblem1  27828  dchrisum0flb  27830  ostth2lem2  27954  usgrexmplef  29833  usgr0edg0rusgr  30149  usgr2pthlem  30342  wwlksn0s  30443  rusgrnumwwlkb0  30556  erclwwlkref  30604  clwwlkf1  30633  0wlkonlem1  30702  upgr4cycl4dv4e  30779  1kp2ke3k  31040  ex-fac  31045  ex-prmo  31053  nn0min  33405  dpmul1000  33458  dp0h  33461  dpexpp1  33467  dpmul4  33473  threehalves  33474  1mhdrd  33475  s2f1  33503  cshw1s2  33514  cycpm2tr  33673  deg1le0eq0  34098  ply1unit  34100  evl1deg1  34101  evl1deg2  34102  evl1deg3  34103  ply1dg1rt  34105  m1pmeq  34110  psrbasfsupp  34136  mplmulmvr  34164  evlextv  34167  mplvrpmlem  34168  mplvrpmfgalem  34169  mplvrpmga  34170  mplvrpmmhm  34171  mplvrpmrhm  34172  psrmonprod  34177  esplyfval0  34189  esplylem  34191  esplyfv1  34194  esplyfval1  34198  esplyfvaln  34199  esplyind  34200  vietalem  34204  vieta  34205  minplyirredlem  34335  rtelextdg2lem  34351  fldext2chn  34353  constraddcl  34387  constrnegcl  34388  constrdircl  34390  constrremulcl  34392  2sqr3minply  34405  lmatcl  34441  lmat22e12  34444  lmat22e21  34445  fsumcvg4  34575  oddpwdc  34979  eulerpartlems  34985  eulerpartlemb  34993  eulerpartlemt  34996  eulerpartgbij  34997  eulerpartlemmf  35000  eulerpartlemgf  35004  eulerpartlemgs2  35005  eulerpartlemn  35006  fib0  35024  fib1  35025  fibp1  35026  ofcs1  35169  signsply0  35173  signsvvf  35201  prodfzo03  35225  repr0  35233  breprexp  35255  hgt750lemd  35270  hgt750lem  35273  hgt750lem2  35274  hgt750leme  35280  tgoldbachgtde  35282  usgrgt2cycl  35888  subfac0  35921  subfacval2  35931  subfaclim  35932  cvmliftlem7  36035  cvmliftlem13  36040  bccolsum  36483  fwddifn0  36909  heiborlem4  38728  heiborlem10  38734  12gcd5e1  43033  60gcd6e6  43034  60gcd7e1  43035  420gcd8e4  43036  12lcm5e60  43038  60lcm7e420  43040  420lcm8e840  43041  lcmineqlem  43082  3exp7  43083  3lexlogpow5ineq1  43084  3lexlogpow5ineq2  43085  3lexlogpow5ineq5  43090  aks4d1p1  43106  aks6d1c2lem4  43157  aks6d1c2  43160  sticksstones11  43186  sticksstones22  43198  aks6d1c7lem1  43210  25or6to4  43236  sqn5i  43322  decpmul  43325  sqdeccom12  43326  sq3deccom12  43327  235t711  43342  ex-decpmul  43343  mhphflem  43604  0prjspn  43644  sum9cubes  43663  nacsfix  43702  diophrw  43749  pell1qr1  43857  monotoddzzfi  43928  jm2.23  43982  hbtlem5  44114  mncn0  44125  aaitgo  44148  brfvrcld  44676  corclrcl  44692  dfrtrcl3  44718  fvrtrcllb0d  44720  fvrtrcllb0da  44721  corcltrcl  44724  cotrclrcl  44727  k0004val0  45139  bccn0  45312  bccn1  45313  binomcxplemradcnv  45321  binomcxplemnotnn0  45325  rexanuz2nf  46471  dvnmul  46922  dvnprodlem3  46927  wallispilem2  47045  wallispi2lem2  47051  stirlinglem5  47057  stirlinglem7  47059  fourierdlem83  47168  fourierdlem112  47197  fouriersw  47210  elaa2lem  47212  elaa2  47213  etransclem48  47261  etransc  47262  iccelpart  48484  fmtno0  48594  fmtnorec2  48597  fmtno5lem1  48607  fmtno5lem2  48608  fmtno5lem4  48610  257prm  48615  fmtnofac2  48623  fmtnofac1  48624  fmtno4prmfac  48626  fmtno4nprmfac193  48628  fmtno5faclem1  48633  fmtno5faclem2  48634  fmtno5faclem3  48635  fmtno5fac  48636  fmtno5nprm  48637  139prmALT  48650  31prm  48651  127prm  48653  m11nprm  48655  bits0ALTV  48746  2exp340mod341  48800  nfermltl2rev  48810  evengpoap3  48866  tgoldbachlt  48883  tgoldbach  48884  stgr0  49027  usgrexmpl1lem  49088  usgrexmpl2lem  49093  gpgprismgr4cycllem6  49167  gpgprismgr4cycllem7  49168  gpgprismgr4cycllem10  49171  nn0mnd  49245  ssnn0ssfz  49430  dig1  49689  0dig2nn0e  49693  0dig2nn0o  49694  0aryfvalel  49715  itcoval0  49743  itcoval1  49744  ackval0  49761  ackval1  49762  ackvalsuc0val  49768  ackval0012  49770  ackval1012  49771  ackval2012  49772  ackval3012  49773  ackval41a  49775