Theorem 0nn0 12490

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 12477	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 230	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 887	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 858   = wceq 1559   ∈ wcel 2141  0cc0 11067  ℕcn 12204  ℕ₀cn0 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-mulcl 11129  ax-i2m1 11135

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-sn 4580  df-n0 12476

This theorem is referenced by:  0xnn0  12554  nn0ind-raph  12667  10nn0  12704  declei  12723  numlti  12724  nummul1c  12736  decaddc2  12743  decrmanc  12744  decrmac  12745  decaddm10  12746  decaddi  12747  decaddci  12748  decaddci2  12749  decmul1  12751  decmulnc  12754  6p5e11  12760  7p4e11  12763  8p3e11  12768  9p2e11  12774  10p10e20  12782  xnn0n0n1ge2b  13128  0elfz  13623  4fvwrd4  13647  fvinim0ffz  13789  ssnn0fi  13992  fsuppmapnn0fiubex  13999  exple1  14184  nn0opth2  14279  faclbnd4lem3  14302  bc0k  14318  bcn1  14320  bccl  14329  hasheq0  14370  hashrabrsn  14379  hashbc  14460  fi1uzind  14514  brfi1ind  14516  opfi1ind  14519  iswrdi  14524  wrdnfi  14555  s1fv  14618  ccat2s1fst  14647  splfv2a  14763  repsw0  14784  0csh0  14800  cshw1  14829  s2fv0  14894  s3fv0  14898  s4fv0  14902  pfx2  14954  ofs1  14977  relexp0g  15029  relexpaddg  15060  rtrclreclem2  15066  fsumnn0cl  15754  binom  15851  bcxmas  15856  isumnn0nn  15863  climcndslem1  15870  geoser  15888  geomulcvg  15897  risefac0  16048  fallfac0  16049  risefac1  16054  fallfac1  16055  binomfallfaclem2  16061  binomfallfac  16062  bpoly0  16071  bpoly2  16078  bpoly3  16079  bpoly4  16080  fsumcube  16081  ef0lem  16099  ege2le3  16111  ef4p  16136  efgt1p2  16137  efgt1p  16138  ruclem11  16263  nthruz  16276  nn0o  16408  ndvdssub  16434  5ndvds3  16438  bits0  16453  0bits  16464  sadcf  16478  sadc0  16479  sadcaddlem  16482  sadcadd  16483  sadadd2lem  16484  sadadd2  16485  smupf  16503  smup0  16504  smumullem  16517  gcdcl  16531  nn0seqcvgd  16595  algcvg  16601  eucalg  16612  lcmcl  16626  lcmfval  16646  lcmfcl  16653  pclem  16865  pcfac  16926  vdwap0  17003  vdwap1  17004  vdwlem6  17013  hashbc0  17032  0ram  17047  0ramcl  17050  ramz2  17051  ramz  17052  ramcl  17056  prmo0  17063  dec5dvds2  17092  2exp11  17116  2exp16  17117  10nprm  17140  11prm  17142  37prm  17148  43prm  17149  83prm  17150  139prm  17151  163prm  17152  317prm  17153  631prm  17154  1259lem1  17158  1259lem2  17159  1259lem3  17160  1259lem4  17161  1259lem5  17162  2503lem1  17164  2503lem2  17165  2503lem3  17166  2503prm  17167  4001lem1  17168  4001lem2  17169  4001lem3  17170  4001lem4  17171  4001prm  17172  plendxnocndx  17404  slotsdifdsndx  17414  slotsdifunifndx  17421  odrngstr  17423  slotsdifplendx2  17436  imasvalstr  17471  ipostr  18552  gsumws1  18863  cycsubm  19234  psgnunilem2  19526  psgnunilem3  19527  odfval  19563  oddvdsnn0  19575  pgp0  19627  sylow1lem1  19629  cyggex2  19928  telgsums  20024  srgbinomlem3  20265  srgbinomlem4  20266  srgbinom  20268  cnfldstr  21414  nn0subm  21462  expmhm  21476  nn0srg  21477  znf1o  21591  zzngim  21592  cygznlem1  21606  cygznlem2a  21607  cygznlem3  21609  cygth  21611  freshmansdream  21614  snifpsrbag  21960  fczpsrbag  21961  psrbagaddcl  21964  psrlidm  22001  mvrf1  22025  mplcoe3  22079  mplcoe5  22081  ltbwe  22085  psrbag0  22103  psrbagsn  22104  evlslem1  22123  mhpsclcl  22200  mhpmulcl  22202  psdmul  22219  psdmvr  22222  00ply1bas  22289  ply1plusgfvi  22291  coe1sclmul  22333  coe1sclmul2  22335  coe1scl  22338  ply1sclid  22339  ply1idvr1OLD  22346  cply1coe0bi  22353  ply1scleq  22356  cpm2mf  22800  m2cpminvid2lem  22802  m2cpminvid2  22803  m2cpmfo  22804  decpmatid  22818  pmatcollpw3  22832  pmatcollpw3fi1lem1  22834  pmatcollpwscmatlem1  22837  pmatcollpwscmatlem2  22838  idpm2idmp  22849  chfacfscmulgsum  22908  chfacfpmmulgsum  22912  cpmadugsumlemF  22924  dscmet  24620  ehl0base  25466  ehl0  25467  itgcnlem  25840  dvn0  25974  dvn1  25976  cpncn  25986  dveflem  26029  c1lip2  26048  deg1le0  26159  ply1divex  26185  mon1pid  26202  ply1rem  26214  fta1g  26218  plyconst  26254  plypf1  26260  plyco  26289  0dgr  26293  0dgrb  26294  coefv0  26296  dgreq0  26313  vieta1lem2  26363  vieta1  26364  aareccl  26378  aannenlem2  26381  taylthlem1  26424  radcnv0  26467  abelthlem6  26487  abelthlem9  26491  logtayl  26713  cxp0  26723  cxpeq  26810  leibpilem2  26994  leibpi  26995  log2ublem3  27001  log2ub  27002  log2le1  27003  divsqrtsumlem  27032  dmgmn0  27078  lgambdd  27089  sqff1o  27234  ppiublem2  27255  chtublem  27263  bclbnd  27332  bposlem8  27343  lgsval  27353  dchrisum0flblem1  27560  dchrisum0flb  27562  ostth2lem2  27686  usgrexmplef  29417  usgr0edg0rusgr  29733  usgr2pthlem  29920  wwlksn0s  30018  rusgrnumwwlkb0  30131  erclwwlkref  30179  clwwlkf1  30208  0wlkonlem1  30277  upgr4cycl4dv4e  30344  1kp2ke3k  30605  ex-fac  30610  ex-prmo  30618  nn0min  32984  dpmul1000  33037  dp0h  33040  dpexpp1  33046  dpmul4  33052  threehalves  33053  1mhdrd  33054  s1f1  33082  s2f1  33084  cshw1s2  33099  cycpm2tr  33260  deg1le0eq0  33730  ply1unit  33732  evl1deg1  33733  evl1deg2  33734  evl1deg3  33735  ply1dg1rt  33737  m1pmeq  33742  psrbasfsupp  33769  mplmulmvr  33797  evlextv  33800  mplvrpmlem  33801  mplvrpmfgalem  33802  mplvrpmga  33803  mplvrpmmhm  33804  mplvrpmrhm  33805  psrmonprod  33810  esplyfval0  33822  esplylem  33824  esplyfv1  33827  esplyfval1  33831  esplyfvaln  33832  esplyind  33833  vietalem  33837  vieta  33838  minplyirredlem  33968  rtelextdg2lem  33984  fldext2chn  33986  constraddcl  34020  constrnegcl  34021  constrdircl  34023  constrremulcl  34025  2sqr3minply  34038  lmatcl  34074  lmat22e12  34077  lmat22e21  34078  fsumcvg4  34208  oddpwdc  34612  eulerpartlems  34618  eulerpartlemb  34626  eulerpartlemt  34629  eulerpartgbij  34630  eulerpartlemmf  34633  eulerpartlemgf  34637  eulerpartlemgs2  34638  eulerpartlemn  34639  fib0  34657  fib1  34658  fibp1  34659  ofcs1  34802  signsply0  34806  signsvvf  34834  prodfzo03  34858  repr0  34866  breprexp  34888  hgt750lemd  34903  hgt750lem  34906  hgt750lem2  34907  hgt750leme  34913  tgoldbachgtde  34915  0nn0m1nnn0  35424  f1resfz0f1d  35425  usgrgt2cycl  35441  subfac0  35488  subfacval2  35498  subfaclim  35499  cvmliftlem7  35602  cvmliftlem13  35607  bccolsum  36050  fwddifn0  36475  heiborlem4  38274  heiborlem10  38280  12gcd5e1  42581  60gcd6e6  42582  60gcd7e1  42583  420gcd8e4  42584  12lcm5e60  42586  60lcm7e420  42588  420lcm8e840  42589  lcmineqlem  42630  3exp7  42631  3lexlogpow5ineq1  42632  3lexlogpow5ineq2  42633  3lexlogpow5ineq5  42638  aks4d1p1  42654  aks6d1c2lem4  42705  aks6d1c2  42708  sticksstones11  42734  sticksstones22  42746  aks6d1c7lem1  42758  sqn5i  42855  decpmul  42858  sqdeccom12  42859  sq3deccom12  42860  235t711  42875  ex-decpmul  42876  mhphflem  43139  0prjspn  43171  sum9cubes  43215  nacsfix  43254  diophrw  43301  pell1qr1  43409  monotoddzzfi  43480  jm2.23  43534  hbtlem5  43666  mncn0  43677  aaitgo  43700  brfvrcld  44228  corclrcl  44244  dfrtrcl3  44270  fvrtrcllb0d  44272  fvrtrcllb0da  44273  corcltrcl  44276  cotrclrcl  44279  k0004val0  44691  bccn0  44880  bccn1  44881  binomcxplemradcnv  44889  binomcxplemnotnn0  44893  rexanuz2nf  46027  dvnmul  46478  dvnprodlem3  46483  wallispilem2  46601  wallispi2lem2  46607  stirlinglem5  46613  stirlinglem7  46615  fourierdlem83  46724  fourierdlem112  46753  fouriersw  46766  elaa2lem  46768  elaa2  46769  etransclem48  46817  etransc  46818  iccelpart  48000  fmtno0  48110  fmtnorec2  48113  fmtno5lem1  48123  fmtno5lem2  48124  fmtno5lem4  48126  257prm  48131  fmtnofac2  48139  fmtnofac1  48140  fmtno4prmfac  48142  fmtno4nprmfac193  48144  fmtno5faclem1  48149  fmtno5faclem2  48150  fmtno5faclem3  48151  fmtno5fac  48152  fmtno5nprm  48153  139prmALT  48166  31prm  48167  127prm  48169  m11nprm  48171  bits0ALTV  48262  2exp340mod341  48316  nfermltl2rev  48326  evengpoap3  48382  tgoldbachlt  48399  tgoldbach  48400  stgr0  48543  usgrexmpl1lem  48604  usgrexmpl2lem  48609  gpgprismgr4cycllem6  48683  gpgprismgr4cycllem7  48684  gpgprismgr4cycllem10  48687  nn0mnd  48762  ssnn0ssfz  48932  dig1  49191  0dig2nn0e  49195  0dig2nn0o  49196  0aryfvalel  49217  itcoval0  49245  itcoval1  49246  ackval0  49263  ackval1  49264  ackvalsuc0val  49270  ackval0012  49272  ackval1012  49273  ackval2012  49274  ackval3012  49275  ackval41a  49277