Theorem 0z 12606

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 11214	. 2 ⊢ 0 ∈ ℝ
2		eqid 2763	. . 3 ⊢ 0 = 0
3	2	3mix1i 1352	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12597	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 723	1 ⊢ 0 ∈ ℤ

This proof depends on syntax axioms:   ∨ w3o 1102   = wceq 1570   ∈ wcel 2143  ℝcr 11103  0cc0 11104  -cneg 11446  ℕcn 12237  ℤcz 12595

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11162  ax-addrcl 11165  ax-rnegex 11175  ax-cnre 11177

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-neg 11448  df-z 12596

This theorem is used by:  0zd  12607  elnn0z  12608  nn0ssz  12618  znegcl  12633  zgt0ge1  12654  nnm1ge0  12668  gtndiv  12677  zeo  12686  nn0ind  12695  fnn0ind  12699  nn0uz  12904  1eluzge0  12908  nn0inf  12958  eqreznegel  12962  fz10  13577  fz00m1  13578  fz01en  13585  fzshftral  13648  fznn0  13652  fz1ssfz0  13656  fz0sn  13660  fz0tp  13661  fz0to3un2pr  13662  fz0to4untppr  13663  fz0to5un2tp  13664  elfz0ubfz0  13665  fz0sn0fz1  13678  1fv  13680  fzo0n  13715  lbfzo0  13733  elfzonlteqm1  13775  fzo01  13781  fzo0to2pr  13784  fz01pr  13785  fzo0to3tp  13786  ico01fl0  13857  flge0nn0  13858  divfl0  13862  btwnzge0  13866  zmodfz  13931  modid  13934  zmodid2  13937  modmuladdnn0  13956  ltweuz  14002  uzenom  14005  fzennn  14009  cardfz  14011  hashgf1o  14012  f13idfv  14041  seqfn  14054  seq1  14055  seqp1  14057  exp0  14106  bcnn  14353  bcval5  14359  bcpasc  14362  4bc2eq6  14370  hashgadd  14418  hashbc  14495  fz1isolem  14503  hashge2el2dif  14522  fi1uzind  14549  s111  14658  swrdnd  14697  swrds1  14709  repswswrd  14826  cshw0  14836  s2f1o  14958  f1oun2prg  14959  rexfiuz  15404  climz  15605  climaddc1  15691  climmulc2  15693  climsubc1  15694  climsubc2  15695  climlec2  15715  sumss  15780  binomlem  15888  binom  15889  bcxmas  15894  climcndslem1  15908  arisum2  15920  explecnv  15924  geomulcvg  15935  bpoly1  16109  bpolydiflem  16112  bpoly2  16115  bpoly3  16116  bpoly4  16117  ef0lem  16136  efcvgfsum  16144  ege2le3  16148  eftlub  16169  efgt1p2  16174  efgt1p  16175  ruclem4  16294  ruclem6  16295  nthruc  16312  dvds0  16333  0dvds  16338  fsumdvds  16370  odd2np1lem  16402  divalglem6  16460  divalglem7  16461  divalglem8  16462  bitsfzo  16497  bitsmod  16498  0bits  16501  m1bits  16502  sadc0  16516  smup0  16541  gcd0val  16559  gcddvds  16565  gcd0id  16581  gcdid0  16582  gcdaddm  16587  gcdid  16589  bezoutlem1  16601  bezout  16605  dfgcd2  16608  lcm0val  16656  dvdslcm  16660  lcmeq0  16662  lcmgcd  16669  lcmdvds  16670  lcmftp  16698  lcmfunsnlem2  16702  dfphi2  16837  phiprmpw  16839  pc0  16918  pcdvdstr  16940  dvdsprmpweqnn  16949  pcfaclem  16962  prmreclem2  16981  prmreclem4  16983  zgz  16997  igz  16998  4sqlem19  17027  ramz  17089  1259lem1  17195  1259lem4  17198  2503lem2  17202  4001lem1  17205  4001lem3  17207  chnub  18682  gsumws1  18901  mulg0  19144  dfod2  19638  zaddablx  19946  0cyg  19967  srgbinomlem4  20315  zringsub  21614  zring0  21617  pzriprnglem3  21642  pzriprnglem4  21643  pzriprnglem5  21644  pzriprnglem6  21645  pzriprnglem10  21649  pzriprng1ALT  21655  zndvds0  21709  ltbwe  22204  pmatcollpw3fi1  22954  iscmet3lem3  25458  vitalilem1  25776  itgcnlem  25958  dvn0  26092  dvexp3  26146  plyco  26407  0dgr  26411  0dgrb  26412  coefv0  26414  coemulc  26421  plyn0mulidp  26451  vieta1lem2  26481  vieta1  26482  elqaalem1  26489  elqaalem3  26491  0aa  26495  aareccl  26498  aannenlem1  26500  aannenlem2  26501  aalioulem1  26504  taylfval  26531  taylplem1  26535  taylplem2  26536  taylpfval  26537  dvtaylp  26542  dvradcnv  26593  pserulm  26594  pserdvlem2  26600  abelthlem6  26608  abelthlem9  26612  logf1o2  26824  ang180lem3  26985  1cubr  27016  leibpi  27116  fsumharmonic  27185  muf  27313  0sgm  27317  1sgmprm  27372  ppiub  27377  bposlem1  27457  bposlem2  27458  lgslem2  27471  lgsfcl2  27476  lgsval2lem  27480  lgs0  27483  lgsdir2lem3  27500  lgsdirnn0  27517  lgsdinn0  27518  pntrlog2bndlem4  27753  padicabv  27803  ostth2lem2  27807  usgrexmpldifpr  29617  usgrexmplef  29618  wlkv0  30008  spthispth  30082  dfpth2  30087  uhgrwkspthlem2  30112  pthdlem2  30126  clwwlkccatlem  30349  0ewlk  30474  0wlkons1  30481  0pth  30485  0pthon  30487  wlk2v2elem2  30516  ntrl2v2e  30518  fzo0opth  33157  0dp2dp  33237  cycpmrn  33472  elrgspnlem1  33571  constrextdg2  34148  zringnm  34357  qqh0  34383  qqhcn  34390  qqhucn  34391  rrh0  34414  eulerpartlemmf  34774  ballotlem2  34888  ballotlemfc0  34892  ballotlemfcc  34893  signstf0  34964  signsvf0  34976  hgt750lemd  35044  hgt750lem  35047  0nn0m1nnn0  35612  revpfxsfxrev  35615  subfacval2  35687  cvmliftlem4  35788  cvmliftlem5  35789  fz0n  36231  bcneg1  36236  bccolsum  36239  fwddifn0  36664  fwddifnp1  36665  knoppcnlem8  37117  knoppcnlem11  37120  poimirlem24  38323  poimirlem27  38326  poimirlem28  38327  sdclem1  38422  heibor1lem  38488  heiborlem4  38493  bccl2d  42786  aks6d1c1  42911  aks6d1c2lem4  42922  0dvds0  43116  mzpnegmpt  43503  diophrw  43518  vdioph  43538  diophren  43568  irrapxlem1  43577  rmxy0  43678  monotoddzzfi  43697  zindbi  43701  rmyeq0  43708  jm2.18  43743  jm2.15nn0  43758  jm2.16nn0  43759  mpaaeu  43905  nzss  45055  hashnzfz2  45059  dvradcnv2  45085  binomcxplemnn0  45087  binomcxplemrat  45088  binomcxplemnotnn0  45094  halffl  46043  lmbr3v  46487  dvnmul  46685  stoweidlem11  46753  stoweidlem17  46759  stirlinglem7  46822  fourierdlem20  46869  etransclem25  47001  etransclem26  47002  etransclem37  47013  smfmullem4  47536  chnsubseqwl  47623  2ffzoeq  48093  fmtnorec2  48323  0evenALTV  48481  0noddALTV  48482  2exp340mod341  48526  8exp8mod9  48529  nfermltl8rev  48535  gpgusgralem  48849  1odd  48964  0even  49030  2zrngamgm  49038  altgsumbcALT  49161  blen1  49392  blen1b  49396  0dig1  49417  0dig2pr01  49418  nn0sumshdiglem1  49429  itcoval0  49470  ackval0  49488  aacllem  50649