Theorem 0z 12576

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 11180	. 2 ⊢ 0 ∈ ℝ
2		eqid 2761	. . 3 ⊢ 0 = 0
3	2	3mix1i 1346	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12567	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 721	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1096   = wceq 1559   ∈ wcel 2141  ℝcr 11069  0cc0 11070  -cneg 11412  ℕcn 12207  ℤcz 12565

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 11128  ax-addrcl 11131  ax-rnegex 11141  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-neg 11414  df-z 12566

This theorem is referenced by:  0zd  12577  elnn0z  12578  nn0ssz  12588  znegcl  12603  zgt0ge1  12624  nnm1ge0  12638  gtndiv  12647  zeo  12656  nn0ind  12665  fnn0ind  12669  nn0uz  12874  1eluzge0  12878  nn0inf  12928  eqreznegel  12932  fz10  13547  fz01en  13554  fzshftral  13617  fznn0  13621  fz1ssfz0  13625  fz0sn  13629  fz0tp  13630  fz0to3un2pr  13631  fz0to4untppr  13632  fz0to5un2tp  13633  elfz0ubfz0  13634  fz0sn0fz1  13647  1fv  13649  fzo0n  13684  lbfzo0  13702  elfzonlteqm1  13744  fzo01  13750  fzo0to2pr  13753  fz01pr  13754  fzo0to3tp  13755  ico01fl0  13826  flge0nn0  13827  divfl0  13831  btwnzge0  13835  zmodfz  13900  modid  13903  zmodid2  13906  modmuladdnn0  13925  ltweuz  13971  uzenom  13974  fzennn  13978  cardfz  13980  hashgf1o  13981  f13idfv  14010  seqfn  14023  seq1  14024  seqp1  14026  exp0  14075  bcnn  14322  bcval5  14328  bcpasc  14331  4bc2eq6  14339  hashgadd  14387  hashbc  14463  fz1isolem  14471  hashge2el2dif  14490  fi1uzind  14517  s111  14626  swrdnd  14665  swrds1  14677  repswswrd  14794  cshw0  14804  s2f1o  14926  f1oun2prg  14927  rexfiuz  15358  climz  15559  climaddc1  15645  climmulc2  15647  climsubc1  15648  climsubc2  15649  climlec2  15669  sumss  15734  binomlem  15842  binom  15843  bcxmas  15848  climcndslem1  15862  arisum2  15874  explecnv  15878  geomulcvg  15889  risefall0lem  16039  bpoly1  16064  bpolydiflem  16067  bpoly2  16070  bpoly3  16071  bpoly4  16072  ef0lem  16091  efcvgfsum  16099  ege2le3  16103  eftlub  16124  efgt1p2  16129  efgt1p  16130  ruclem4  16249  ruclem6  16250  nthruc  16267  dvds0  16288  0dvds  16293  fsumdvds  16325  odd2np1lem  16357  divalglem6  16415  divalglem7  16416  divalglem8  16417  bitsfzo  16452  bitsmod  16453  0bits  16456  m1bits  16457  sadc0  16471  smup0  16496  gcd0val  16514  gcddvds  16520  gcd0id  16536  gcdid0  16537  gcdaddm  16542  gcdid  16544  bezoutlem1  16556  bezout  16560  dfgcd2  16563  lcm0val  16611  dvdslcm  16615  lcmeq0  16617  lcmgcd  16624  lcmdvds  16625  lcmftp  16653  lcmfunsnlem2  16657  dfphi2  16792  phiprmpw  16794  pc0  16873  pcdvdstr  16895  dvdsprmpweqnn  16904  pcfaclem  16917  prmreclem2  16936  prmreclem4  16938  zgz  16952  igz  16953  4sqlem19  16982  ramz  17044  1259lem1  17150  1259lem4  17153  2503lem2  17157  4001lem1  17160  4001lem3  17162  chnub  18637  gsumws1  18855  mulg0  19099  dfod2  19587  zaddablx  19895  0cyg  19916  srgbinomlem4  20258  zringsub  21487  zring0  21490  pzriprnglem3  21515  pzriprnglem4  21516  pzriprnglem5  21517  pzriprnglem6  21518  pzriprnglem10  21522  pzriprng1ALT  21528  zndvds0  21582  ltbwe  22077  pmatcollpw3fi1  22828  iscmet3lem3  25332  vitalilem1  25650  itgcnlem  25832  dvn0  25966  dvexp3  26020  plyco  26281  0dgr  26285  0dgrb  26286  coefv0  26288  coemulc  26295  vieta1lem2  26352  vieta1  26353  elqaalem1  26360  elqaalem3  26362  aareccl  26367  aannenlem1  26369  aannenlem2  26370  aalioulem1  26373  taylfval  26399  taylplem1  26403  taylplem2  26404  taylpfval  26405  dvtaylp  26410  dvradcnv  26461  pserulm  26462  pserdvlem2  26468  abelthlem6  26476  abelthlem9  26480  logf1o2  26692  ang180lem3  26853  1cubr  26884  leibpi  26984  fsumharmonic  27053  muf  27181  0sgm  27185  1sgmprm  27240  ppiub  27245  bposlem1  27325  bposlem2  27326  lgslem2  27339  lgsfcl2  27344  lgsval2lem  27348  lgs0  27351  lgsdir2lem3  27368  lgsdirnn0  27385  lgsdinn0  27386  pntrlog2bndlem4  27621  padicabv  27671  ostth2lem2  27675  usgrexmpldifpr  29405  usgrexmplef  29406  wlkv0  29796  spthispth  29870  dfpth2  29875  uhgrwkspthlem2  29900  pthdlem2  29914  clwwlkccatlem  30137  0ewlk  30262  0wlkons1  30269  0pth  30273  0pthon  30275  wlk2v2elem2  30304  ntrl2v2e  30306  fzo0opth  32955  0dp2dp  33047  cycpmrn  33284  elrgspnlem1  33384  constrextdg2  34007  zringnm  34216  qqh0  34242  qqhcn  34249  qqhucn  34250  rrh0  34273  eulerpartlemmf  34633  ballotlem2  34747  ballotlemfc0  34751  ballotlemfcc  34752  plymulx0  34805  signstf0  34826  signsvf0  34838  hgt750lemd  34906  hgt750lem  34909  0nn0m1nnn0  35427  revpfxsfxrev  35430  subfacval2  35501  cvmliftlem4  35602  cvmliftlem5  35603  fz0n  36045  bcneg1  36050  bccolsum  36053  fwddifn0  36478  fwddifnp1  36479  knoppcnlem8  36902  knoppcnlem11  36905  poimirlem24  38107  poimirlem27  38110  poimirlem28  38111  sdclem1  38206  heibor1lem  38272  heiborlem4  38277  bccl2d  42572  aks6d1c1  42697  aks6d1c2lem4  42708  0dvds0  42900  mzpnegmpt  43289  diophrw  43304  vdioph  43324  diophren  43354  irrapxlem1  43363  rmxy0  43464  monotoddzzfi  43483  zindbi  43487  rmyeq0  43494  jm2.18  43529  jm2.15nn0  43544  jm2.16nn0  43545  mpaaeu  43691  nzss  44857  hashnzfz2  44861  dvradcnv2  44887  binomcxplemnn0  44889  binomcxplemrat  44890  binomcxplemnotnn0  44896  halffl  45839  lmbr3v  46283  dvnmul  46481  stoweidlem11  46549  stoweidlem17  46555  stirlinglem7  46618  fourierdlem20  46665  etransclem25  46797  etransclem26  46798  etransclem37  46809  smfmullem4  47332  chnsubseqwl  47419  2ffzoeq  47886  fmtnorec2  48116  0evenALTV  48274  0noddALTV  48275  2exp340mod341  48319  8exp8mod9  48322  nfermltl8rev  48328  gpgusgralem  48642  1odd  48757  0even  48823  2zrngamgm  48831  altgsumbcALT  48939  blen1  49170  blen1b  49174  0dig1  49195  0dig2pr01  49196  nn0sumshdiglem1  49207  itcoval0  49248  ackval0  49266  aacllem  50386