Theorem 0z 12486

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 11121	. 2 ⊢ 0 ∈ ℝ
2		eqid 2733	. . 3 ⊢ 0 = 0
3	2	3mix1i 1334	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12477	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 711	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1085   = wceq 1541   ∈ wcel 2113  ℝcr 11012  0cc0 11013  -cneg 11352  ℕcn 12132  ℤcz 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-1cn 11071  ax-addrcl 11074  ax-rnegex 11084  ax-cnre 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-neg 11354  df-z 12476

This theorem is referenced by:  0zd  12487  elnn0z  12488  nn0ssz  12498  znegcl  12513  zgt0ge1  12533  nnm1ge0  12547  gtndiv  12556  zeo  12565  nn0ind  12574  fnn0ind  12578  nn0uz  12776  1eluzge0  12780  nn0inf  12830  eqreznegel  12834  fz10  13447  fz01en  13454  fzshftral  13517  fznn0  13521  fz1ssfz0  13525  fz0sn  13529  fz0tp  13530  fz0to3un2pr  13531  fz0to4untppr  13532  fz0to5un2tp  13533  elfz0ubfz0  13534  fz0sn0fz1  13547  1fv  13549  fzo0n  13583  lbfzo0  13601  elfzonlteqm1  13643  fzo01  13649  fzo0to2pr  13652  fz01pr  13653  fzo0to3tp  13654  ico01fl0  13725  flge0nn0  13726  divfl0  13730  btwnzge0  13734  zmodfz  13799  modid  13802  zmodid2  13805  modmuladdnn0  13824  ltweuz  13870  uzenom  13873  fzennn  13877  cardfz  13879  hashgf1o  13880  f13idfv  13909  seqfn  13922  seq1  13923  seqp1  13925  exp0  13974  bcnn  14221  bcval5  14227  bcpasc  14230  4bc2eq6  14238  hashgadd  14286  hashbc  14362  fz1isolem  14370  hashge2el2dif  14389  fi1uzind  14416  s111  14525  swrdnd  14564  swrds1  14576  repswswrd  14693  cshw0  14703  s2f1o  14825  f1oun2prg  14826  rexfiuz  15257  climz  15458  climaddc1  15544  climmulc2  15546  climsubc1  15547  climsubc2  15548  climlec2  15568  sumss  15633  binomlem  15738  binom  15739  bcxmas  15744  climcndslem1  15758  arisum2  15770  explecnv  15774  geomulcvg  15785  risefall0lem  15935  bpoly1  15960  bpolydiflem  15963  bpoly2  15966  bpoly3  15967  bpoly4  15968  ef0lem  15987  efcvgfsum  15995  ege2le3  15999  eftlub  16020  efgt1p2  16025  efgt1p  16026  ruclem4  16145  ruclem6  16146  nthruc  16163  dvds0  16184  0dvds  16189  fsumdvds  16221  odd2np1lem  16253  divalglem6  16311  divalglem7  16312  divalglem8  16313  bitsfzo  16348  bitsmod  16349  0bits  16352  m1bits  16353  sadc0  16367  smup0  16392  gcd0val  16410  gcddvds  16416  gcd0id  16432  gcdid0  16433  gcdaddm  16438  gcdid  16440  bezoutlem1  16452  bezout  16456  dfgcd2  16459  lcm0val  16507  dvdslcm  16511  lcmeq0  16513  lcmgcd  16520  lcmdvds  16521  lcmftp  16549  lcmfunsnlem2  16553  dfphi2  16687  phiprmpw  16689  pc0  16768  pcdvdstr  16790  dvdsprmpweqnn  16799  pcfaclem  16812  prmreclem2  16831  prmreclem4  16833  zgz  16847  igz  16848  4sqlem19  16877  ramz  16939  1259lem1  17044  1259lem4  17047  2503lem2  17051  4001lem1  17054  4001lem3  17056  chnub  18530  gsumws1  18748  mulg0  18989  dfod2  19478  zaddablx  19786  0cyg  19807  srgbinomlem4  20149  zringsub  21394  zring0  21397  pzriprnglem3  21422  pzriprnglem4  21423  pzriprnglem5  21424  pzriprnglem6  21425  pzriprnglem10  21429  pzriprng1ALT  21435  zndvds0  21489  ltbwe  21980  pmatcollpw3fi1  22704  iscmet3lem3  25218  vitalilem1  25537  itgcnlem  25719  dvn0  25854  dvexp3  25910  plyco  26174  0dgr  26178  0dgrb  26179  coefv0  26181  coemulc  26188  vieta1lem2  26247  vieta1  26248  elqaalem1  26255  elqaalem3  26257  aareccl  26262  aannenlem1  26264  aannenlem2  26265  aalioulem1  26268  taylfval  26294  taylplem1  26298  taylplem2  26299  taylpfval  26300  dvtaylp  26306  dvradcnv  26358  pserulm  26359  pserdvlem2  26366  abelthlem6  26374  abelthlem9  26378  logf1o2  26587  ang180lem3  26749  1cubr  26780  leibpi  26880  fsumharmonic  26950  muf  27078  0sgm  27082  1sgmprm  27138  ppiub  27143  bposlem1  27223  bposlem2  27224  lgslem2  27237  lgsfcl2  27242  lgsval2lem  27246  lgs0  27249  lgsdir2lem3  27266  lgsdirnn0  27283  lgsdinn0  27284  pntrlog2bndlem4  27519  padicabv  27569  ostth2lem2  27573  usgrexmpldifpr  29238  usgrexmplef  29239  wlkv0  29630  spthispth  29704  dfpth2  29709  uhgrwkspthlem2  29734  pthdlem2  29748  clwwlkccatlem  29971  0ewlk  30096  0wlkons1  30103  0pth  30107  0pthon  30109  wlk2v2elem2  30138  ntrl2v2e  30140  fzo0opth  32790  0dp2dp  32896  cycpmrn  33119  elrgspnlem1  33216  constrextdg2  33783  zringnm  33992  qqh0  34018  qqhcn  34025  qqhucn  34026  rrh0  34049  eulerpartlemmf  34409  ballotlem2  34523  ballotlemfc0  34527  ballotlemfcc  34528  plymulx0  34581  signstf0  34602  signsvf0  34614  hgt750lemd  34682  hgt750lem  34685  0nn0m1nnn0  35178  revpfxsfxrev  35181  subfacval2  35252  cvmliftlem4  35353  cvmliftlem5  35354  fz0n  35796  bcneg1  35801  bccolsum  35804  fwddifn0  36229  fwddifnp1  36230  knoppcnlem8  36565  knoppcnlem11  36568  poimirlem24  37704  poimirlem27  37707  poimirlem28  37708  sdclem1  37803  heibor1lem  37869  heiborlem4  37874  bccl2d  42104  aks6d1c1  42229  aks6d1c2lem4  42240  0dvds0  42445  mzpnegmpt  42861  diophrw  42876  vdioph  42896  diophren  42930  irrapxlem1  42939  rmxy0  43040  monotoddzzfi  43059  zindbi  43063  rmyeq0  43070  jm2.18  43105  jm2.15nn0  43120  jm2.16nn0  43121  mpaaeu  43267  nzss  44434  hashnzfz2  44438  dvradcnv2  44464  binomcxplemnn0  44466  binomcxplemrat  44467  binomcxplemnotnn0  44473  halffl  45421  lmbr3v  45867  dvnmul  46065  stoweidlem11  46133  stoweidlem17  46139  stirlinglem7  46202  fourierdlem20  46249  etransclem25  46381  etransclem26  46382  etransclem37  46393  smfmullem4  46916  chnsubseqwl  47001  2ffzoeq  47451  fmtnorec2  47667  0evenALTV  47812  0noddALTV  47813  2exp340mod341  47857  8exp8mod9  47860  nfermltl8rev  47866  gpgusgralem  48180  1odd  48295  0even  48361  2zrngamgm  48369  altgsumbcALT  48477  blen1  48709  blen1b  48713  0dig1  48734  0dig2pr01  48735  nn0sumshdiglem1  48746  itcoval0  48787  ackval0  48805  aacllem  49926