Theorem 0z 12685

Description: Zero is an integer. (Contributed by NM, 12-Jan-2002.)

Assertion

Ref	Expression
0z	⊢ 0 ∈ ℤ

Proof of Theorem 0z

Step	Hyp	Ref	Expression
1		0re 11291	. 2 ⊢ 0 ∈ ℝ
2		eqid 2761	. . 3 ⊢ 0 = 0
3	2	3mix1i 1352	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12676	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 724	1 ⊢ 0 ∈ ℤ

This proof depends on syntax axioms:   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145  ℝcr 11180  0cc0 11181  -cneg 11523  ℕcn 12316  ℤcz 12674

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 11239  ax-addrcl 11242  ax-rnegex 11252  ax-cnre 11254

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-neg 11525  df-z 12675

This theorem is used by:  0zd  12686  elnn0z  12687  nn0ssz  12697  znegcl  12712  zgt0ge1  12733  0nn0m1nnn0  12734  nnm1ge0  12748  gtndiv  12757  zeo  12766  nn0ind  12775  fnn0ind  12779  nn0uz  12984  1eluzge0  12988  nn0inf  13038  eqreznegel  13042  fz10  13658  fz00m1  13659  fz01en  13666  fzshftral  13729  fznn0  13733  fz1ssfz0  13737  fz0sn  13741  fz0tp  13742  fz0to3un2pr  13743  fz0to4untppr  13744  fz0to5un2tp  13745  elfz0ubfz0  13746  fz0sn0fz1  13759  1fv  13761  fzo0n  13796  lbfzo0  13814  elfzonlteqm1  13856  fzo01  13862  fzo0to2pr  13865  fz01pr  13866  fzo0to3tp  13867  ico01fl0  13939  flge0nn0  13940  divfl0  13944  btwnzge0  13948  zmodfz  14013  modid  14016  zmodid2  14019  modmuladdnn0  14038  ltweuz  14084  uzenom  14087  fzennn  14091  cardfz  14093  hashgf1o  14094  f13idfv  14123  seqfn  14136  seq1  14137  seqp1  14139  exp0  14188  bcnn  14436  bcval5  14442  bcpasc  14445  4bc2eq6  14453  hashgadd  14501  hashbc  14578  fz1isolem  14586  hashge2el2dif  14605  fi1uzind  14632  s111  14743  swrdnd  14784  swrds1  14796  revpfxsfxrev  14897  repswswrd  14915  cshw0  14925  s2f1o  15047  f1oun2prg  15048  rexfiuz  15495  climz  15696  climaddc1  15782  climmulc2  15784  climsubc1  15785  climsubc2  15786  climlec2  15806  sumss  15870  binomlem  15978  binom  15979  bcxmas  15984  climcndslem1  15998  arisum2  16010  explecnv  16014  geomulcvg  16025  bpoly1  16197  bpolydiflem  16200  bpoly2  16203  bpoly3  16204  bpoly4  16205  ef0lem  16224  efcvgfsum  16232  ege2le3  16236  eftlub  16257  efgt1p2  16262  efgt1p  16263  ruclem4  16382  ruclem6  16383  nthruc  16400  dvds0  16421  0dvds  16426  fsumdvds  16458  odd2np1lem  16490  divalglem6  16548  divalglem7  16549  divalglem8  16550  bitsfzo  16585  bitsmod  16586  0bits  16589  m1bits  16590  sadc0  16604  smup0  16629  gcd0val  16647  gcddvds  16653  gcd0id  16671  gcdid0  16672  gcdaddm  16677  gcdid  16679  bezoutlem1  16692  bezout  16696  dfgcd2  16699  lcm0val  16749  dvdslcm  16753  lcmeq0  16755  lcmgcd  16762  lcmdvds  16763  lcmftp  16791  lcmfunsnlem2  16795  dfphi2  16931  phiprmpw  16933  pc0  17012  pcdvdstr  17034  dvdsprmpweqnn  17043  pcfaclem  17056  prmreclem2  17075  prmreclem4  17077  zgz  17091  igz  17092  4sqlem19  17121  ramz  17183  1259lem1  17289  1259lem4  17292  2503lem2  17296  4001lem1  17299  4001lem3  17301  chnub  18776  gsumws1  19014  mulg0  19264  dfod2  19758  zaddablx  20066  0cyg  20087  srgbinomlem4  20435  zringsub  21741  zring0  21744  pzriprnglem3  21769  pzriprnglem4  21770  pzriprnglem5  21771  pzriprnglem6  21772  pzriprnglem10  21776  pzriprng1ALT  21782  zndvds0  21836  ltbwe  22333  pmatcollpw3fi1  23086  iscmet3lem3  25591  vitalilem1  25909  itgcnlem  26090  dvn0  26224  dvexp3  26278  plyco  26540  0dgr  26544  0dgrb  26545  coefv0  26547  coemulc  26554  plyn0mulidp  26584  vieta1lem2  26616  vieta1  26617  elqaalem1  26624  elqaalem3  26626  0aa  26631  aareccl  26635  aannenlem1  26637  aannenlem2  26638  aalioulem1  26641  taylfval  26668  taylplem1  26672  taylplem2  26673  taylpfval  26674  dvtaylp  26679  dvradcnv  26730  pserulm  26731  pserdvlem2  26737  abelthlem6  26745  abelthlem9  26749  logf1o2  26960  ang180lem3  27121  1cubr  27152  leibpi  27252  fsumharmonic  27321  muf  27449  0sgm  27453  1sgmprm  27508  ppiub  27513  bposlem1  27593  bposlem2  27594  lgslem2  27607  lgsfcl2  27612  lgsval2lem  27616  lgs0  27619  lgsdir2lem3  27636  lgsdirnn0  27653  lgsdinn0  27654  pntrlog2bndlem4  27889  padicabv  27939  ostth2lem2  27943  usgrexmpldifpr  29821  usgrexmplef  29822  wlkv0  30212  spthispth  30291  dfpth2  30296  uhgrwkspthlem2  30322  pthdlem2  30336  clwwlkccatlem  30562  0ewlk  30687  0wlkons1  30694  0pth  30698  0pthon  30700  wlk2v2elem2  30739  ntrl2v2e  30741  fzo0opth  33377  0dp2dp  33457  cycpmrn  33686  elrgspnlem1  33785  constrextdg2  34363  zringnm  34572  qqh0  34598  qqhcn  34605  qqhucn  34606  rrh0  34629  eulerpartlemmf  34990  ballotlem2  35104  ballotlemfc0  35108  ballotlemfcc  35109  signstf0  35180  signsvf0  35192  hgt750lemd  35260  hgt750lem  35263  subfacval2  35921  cvmliftlem4  36022  cvmliftlem5  36023  fz0n  36465  bcneg1  36470  bccolsum  36473  fwddifn0  36899  fwddifnp1  36900  knoppcnlem8  37336  knoppcnlem11  37339  poimirlem24  38530  poimirlem27  38533  poimirlem28  38534  sdclem1  38645  heibor1lem  38711  heiborlem4  38716  bccl2d  43009  aks6d1c1  43134  aks6d1c2lem4  43145  0dvds0  43352  mzpnegmpt  43708  diophrw  43723  vdioph  43743  diophren  43773  irrapxlem1  43782  rmxy0  43883  monotoddzzfi  43902  zindbi  43906  rmyeq0  43913  jm2.18  43948  jm2.15nn0  43963  jm2.16nn0  43964  mpaaeu  44110  nzss  45260  hashnzfz2  45264  dvradcnv2  45290  binomcxplemnn0  45292  binomcxplemrat  45293  binomcxplemnotnn0  45299  halffl  46255  lmbr3v  46699  dvnmul  46897  stoweidlem11  46965  stoweidlem17  46971  stirlinglem7  47034  fourierdlem20  47081  etransclem25  47213  etransclem26  47214  etransclem37  47225  smfmullem4  47748  chnsubseqwl  47833  2ffzoeq  48342  fmtnorec2  48572  0evenALTV  48730  0noddALTV  48731  2exp340mod341  48775  8exp8mod9  48778  nfermltl8rev  48784  gpgusgralem  49098  1odd  49212  0even  49278  2zrngamgm  49286  altgsumbcALT  49409  blen1  49640  blen1b  49644  0dig1  49665  0dig2pr01  49666  nn0sumshdiglem1  49677  itcoval0  49718  ackval0  49736  aacllem  50883