Theorem 0z 12613

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 11255	. 2 ⊢ 0 ∈ ℝ
2		eqid 2726	. . 3 ⊢ 0 = 0
3	2	3mix1i 1330	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12604	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 709	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1083   = wceq 1534   ∈ wcel 2099  ℝcr 11146  0cc0 11147  -cneg 11484  ℕcn 12256  ℤcz 12602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-1cn 11205  ax-addrcl 11208  ax-rnegex 11218  ax-cnre 11220

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rex 3061  df-rab 3421  df-v 3465  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4324  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4907  df-br 5145  df-iota 6496  df-fv 6552  df-ov 7417  df-neg 11486  df-z 12603

This theorem is referenced by:  0zd  12614  elnn0z  12615  nn0ssz  12625  znegcl  12641  zgt0ge1  12660  nnm1ge0  12674  gtndiv  12683  zeo  12692  nn0ind  12701  fnn0ind  12705  eluzaddOLD  12901  eluzsubOLD  12902  nn0uz  12908  1eluzge0  12920  nn0inf  12958  eqreznegel  12962  fz10  13568  fz01en  13575  fzshftral  13635  fznn0  13639  fz1ssfz0  13643  fz0sn  13647  fz0tp  13648  fz0to3un2pr  13649  fz0to4untppr  13650  elfz0ubfz0  13651  fz0sn0fz1  13664  1fv  13666  fzo0n  13700  lbfzo0  13718  elfzonlteqm1  13754  fzo01  13760  fzo0to2pr  13763  fzo0to3tp  13764  ico01fl0  13831  flge0nn0  13832  divfl0  13836  btwnzge0  13840  zmodfz  13905  modid  13908  zmodid2  13911  modmuladdnn0  13927  ltweuz  13973  uzenom  13976  fzennn  13980  cardfz  13982  hashgf1o  13983  f13idfv  14012  seqfn  14025  seq1  14026  seqp1  14028  exp0  14077  bcnn  14322  bcval5  14328  bcpasc  14331  4bc2eq6  14339  hashgadd  14387  hashbc  14463  fz1isolem  14473  hashge2el2dif  14492  fi1uzind  14509  s111  14616  swrdnd  14655  swrds1  14667  repswswrd  14785  cshw0  14795  s2f1o  14918  f1oun2prg  14919  rexfiuz  15345  climz  15544  climaddc1  15630  climmulc2  15632  climsubc1  15633  climsubc2  15634  climlec2  15656  sumss  15721  binomlem  15826  binom  15827  bcxmas  15832  climcndslem1  15846  arisum2  15858  explecnv  15862  geomulcvg  15873  risefall0lem  16021  bpoly1  16046  bpolydiflem  16049  bpoly2  16052  bpoly3  16053  bpoly4  16054  ef0lem  16073  efcvgfsum  16081  ege2le3  16085  eftlub  16104  efgt1p2  16109  efgt1p  16110  ruclem4  16229  ruclem6  16230  nthruc  16247  dvds0  16267  0dvds  16272  fsumdvds  16303  odd2np1lem  16335  divalglem6  16393  divalglem7  16394  divalglem8  16395  bitsfzo  16428  bitsmod  16429  0bits  16432  m1bits  16433  sadc0  16447  smup0  16472  gcd0val  16490  gcddvds  16496  gcd0id  16512  gcdid0  16513  gcdaddm  16518  gcdid  16520  bezoutlem1  16533  bezout  16537  dfgcd2  16540  lcm0val  16588  dvdslcm  16592  lcmeq0  16594  lcmgcd  16601  lcmdvds  16602  lcmftp  16630  lcmfunsnlem2  16634  dfphi2  16769  phiprmpw  16771  pc0  16849  pcdvdstr  16871  dvdsprmpweqnn  16880  pcfaclem  16893  prmreclem2  16912  prmreclem4  16914  zgz  16928  igz  16929  4sqlem19  16958  ramz  17020  1259lem1  17126  1259lem4  17129  2503lem2  17133  4001lem1  17136  4001lem3  17138  gsumws1  18821  mulg0  19062  dfod2  19556  zaddablx  19864  0cyg  19885  srgbinomlem4  20206  zringsub  21439  zring0  21442  pzriprnglem3  21467  pzriprnglem4  21468  pzriprnglem5  21469  pzriprnglem6  21470  pzriprnglem10  21474  pzriprng1ALT  21480  zndvds0  21542  ltbwe  22045  pmatcollpw3fi1  22776  iscmet3lem3  25304  vitalilem1  25623  itgcnlem  25805  dvn0  25940  dvexp3  25996  plyco  26263  0dgr  26267  0dgrb  26268  coefv0  26270  coemulc  26277  vieta1lem2  26334  vieta1  26335  elqaalem1  26342  elqaalem3  26344  aareccl  26349  aannenlem1  26351  aannenlem2  26352  aalioulem1  26355  taylfval  26381  taylplem1  26385  taylplem2  26386  taylpfval  26387  dvtaylp  26393  dvradcnv  26445  pserulm  26446  pserdvlem2  26453  abelthlem6  26461  abelthlem9  26465  logf1o2  26672  ang180lem3  26834  1cubr  26865  leibpi  26965  fsumharmonic  27035  muf  27163  0sgm  27167  1sgmprm  27223  ppiub  27228  bposlem1  27308  bposlem2  27309  lgslem2  27322  lgsfcl2  27327  lgsval2lem  27331  lgs0  27334  lgsdir2lem3  27351  lgsdirnn0  27368  lgsdinn0  27369  pntrlog2bndlem4  27604  padicabv  27654  ostth2lem2  27658  usgrexmpldifpr  29189  usgrexmplef  29190  wlkv0  29583  spthispth  29658  uhgrwkspthlem2  29686  pthdlem2  29700  clwwlkccatlem  29917  0ewlk  30042  0wlkons1  30049  0pth  30053  0pthon  30055  wlk2v2elem2  30084  ntrl2v2e  30086  fzo0opth  32708  0dp2dp  32771  chnub  32882  cycpmrn  33023  zringnm  33784  qqh0  33810  qqhcn  33817  qqhucn  33818  rrh0  33841  eulerpartlemmf  34220  ballotlem2  34333  ballotlemfc0  34337  ballotlemfcc  34338  plymulx0  34404  signstf0  34425  signsvf0  34437  hgt750lemd  34505  hgt750lem  34508  0nn0m1nnn0  34951  revpfxsfxrev  34954  subfacval2  35026  cvmliftlem4  35127  cvmliftlem5  35128  fz0n  35564  bcneg1  35569  bccolsum  35572  fwddifn0  35999  fwddifnp1  36000  knoppcnlem8  36214  knoppcnlem11  36217  poimirlem24  37356  poimirlem27  37359  poimirlem28  37360  sdclem1  37455  heibor1lem  37521  heiborlem4  37526  bccl2d  41701  aks6d1c1  41826  aks6d1c2lem4  41837  0dvds0  42051  mzpnegmpt  42436  diophrw  42451  vdioph  42471  diophren  42505  irrapxlem1  42514  rmxy0  42616  monotoddzzfi  42635  zindbi  42639  rmyeq0  42646  jm2.18  42681  jm2.15nn0  42696  jm2.16nn0  42697  mpaaeu  42846  nzss  44026  hashnzfz2  44030  dvradcnv2  44056  binomcxplemnn0  44058  binomcxplemrat  44059  binomcxplemnotnn0  44065  halffl  44945  lmbr3v  45400  dvnmul  45598  stoweidlem11  45666  stoweidlem17  45672  stirlinglem7  45735  fourierdlem20  45782  etransclem25  45914  etransclem26  45915  etransclem37  45926  smfmullem4  46449  upwordnul  46533  tworepnotupword  46539  2ffzoeq  46974  fmtnorec2  47149  0evenALTV  47294  0noddALTV  47295  2exp340mod341  47339  8exp8mod9  47342  nfermltl8rev  47348  1odd  47582  0even  47648  2zrngamgm  47656  altgsumbcALT  47766  blen1  48006  blen1b  48010  0dig1  48031  0dig2pr01  48032  nn0sumshdiglem1  48043  itcoval0  48084  ackval0  48102  aacllem  48583