Theorem 0z 12593

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

Syntax hints:   ∨ w3o 1100   = wceq 1563   ∈ wcel 2145  ℝcr 11087  0cc0 11088  -cneg 11430  ℕcn 12224  ℤcz 12582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-1cn 11146  ax-addrcl 11149  ax-rnegex 11159  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-neg 11432  df-z 12583

This theorem is referenced by:  0zd  12594  elnn0z  12595  nn0ssz  12605  znegcl  12620  zgt0ge1  12641  nnm1ge0  12655  gtndiv  12664  zeo  12673  nn0ind  12682  fnn0ind  12686  nn0uz  12891  1eluzge0  12895  nn0inf  12945  eqreznegel  12949  fz10  13564  fz01en  13571  fzshftral  13634  fznn0  13638  fz1ssfz0  13642  fz0sn  13646  fz0tp  13647  fz0to3un2pr  13648  fz0to4untppr  13649  fz0to5un2tp  13650  elfz0ubfz0  13651  fz0sn0fz1  13664  1fv  13666  fzo0n  13701  lbfzo0  13719  elfzonlteqm1  13761  fzo01  13767  fzo0to2pr  13770  fz01pr  13771  fzo0to3tp  13772  ico01fl0  13843  flge0nn0  13844  divfl0  13848  btwnzge0  13852  zmodfz  13917  modid  13920  zmodid2  13923  modmuladdnn0  13942  ltweuz  13988  uzenom  13991  fzennn  13995  cardfz  13997  hashgf1o  13998  f13idfv  14027  seqfn  14040  seq1  14041  seqp1  14043  exp0  14092  bcnn  14339  bcval5  14345  bcpasc  14348  4bc2eq6  14356  hashgadd  14404  hashbc  14480  fz1isolem  14488  hashge2el2dif  14507  fi1uzind  14534  s111  14643  swrdnd  14682  swrds1  14694  repswswrd  14811  cshw0  14821  s2f1o  14943  f1oun2prg  14944  rexfiuz  15389  climz  15590  climaddc1  15676  climmulc2  15678  climsubc1  15679  climsubc2  15680  climlec2  15700  sumss  15765  binomlem  15873  binom  15874  bcxmas  15879  climcndslem1  15893  arisum2  15905  explecnv  15909  geomulcvg  15920  risefall0lem  16070  bpoly1  16095  bpolydiflem  16098  bpoly2  16101  bpoly3  16102  bpoly4  16103  ef0lem  16122  efcvgfsum  16130  ege2le3  16134  eftlub  16155  efgt1p2  16160  efgt1p  16161  ruclem4  16280  ruclem6  16281  nthruc  16298  dvds0  16319  0dvds  16324  fsumdvds  16356  odd2np1lem  16388  divalglem6  16446  divalglem7  16447  divalglem8  16448  bitsfzo  16483  bitsmod  16484  0bits  16487  m1bits  16488  sadc0  16502  smup0  16527  gcd0val  16545  gcddvds  16551  gcd0id  16567  gcdid0  16568  gcdaddm  16573  gcdid  16575  bezoutlem1  16587  bezout  16591  dfgcd2  16594  lcm0val  16642  dvdslcm  16646  lcmeq0  16648  lcmgcd  16655  lcmdvds  16656  lcmftp  16684  lcmfunsnlem2  16688  dfphi2  16823  phiprmpw  16825  pc0  16904  pcdvdstr  16926  dvdsprmpweqnn  16935  pcfaclem  16948  prmreclem2  16967  prmreclem4  16969  zgz  16983  igz  16984  4sqlem19  17013  ramz  17075  1259lem1  17181  1259lem4  17184  2503lem2  17188  4001lem1  17191  4001lem3  17193  chnub  18668  gsumws1  18887  mulg0  19131  dfod2  19625  zaddablx  19933  0cyg  19954  srgbinomlem4  20302  zringsub  21565  zring0  21568  pzriprnglem3  21593  pzriprnglem4  21594  pzriprnglem5  21595  pzriprnglem6  21596  pzriprnglem10  21600  pzriprng1ALT  21606  zndvds0  21660  ltbwe  22155  pmatcollpw3fi1  22906  iscmet3lem3  25410  vitalilem1  25728  itgcnlem  25910  dvn0  26044  dvexp3  26098  plyco  26359  0dgr  26363  0dgrb  26364  coefv0  26366  coemulc  26373  plyn0mulidp  26403  vieta1lem2  26433  vieta1  26434  elqaalem1  26441  elqaalem3  26443  aareccl  26448  aannenlem1  26450  aannenlem2  26451  aalioulem1  26454  taylfval  26480  taylplem1  26484  taylplem2  26485  taylpfval  26486  dvtaylp  26491  dvradcnv  26542  pserulm  26543  pserdvlem2  26549  abelthlem6  26557  abelthlem9  26561  logf1o2  26773  ang180lem3  26934  1cubr  26965  leibpi  27065  fsumharmonic  27134  muf  27262  0sgm  27266  1sgmprm  27321  ppiub  27326  bposlem1  27406  bposlem2  27407  lgslem2  27420  lgsfcl2  27425  lgsval2lem  27429  lgs0  27432  lgsdir2lem3  27449  lgsdirnn0  27466  lgsdinn0  27467  pntrlog2bndlem4  27702  padicabv  27752  ostth2lem2  27756  usgrexmpldifpr  29517  usgrexmplef  29518  wlkv0  29908  spthispth  29982  dfpth2  29987  uhgrwkspthlem2  30012  pthdlem2  30026  clwwlkccatlem  30249  0ewlk  30374  0wlkons1  30381  0pth  30385  0pthon  30387  wlk2v2elem2  30416  ntrl2v2e  30418  fzo0opth  33060  0dp2dp  33141  cycpmrn  33376  elrgspnlem1  33475  constrextdg2  34056  zringnm  34265  qqh0  34291  qqhcn  34298  qqhucn  34299  rrh0  34322  eulerpartlemmf  34682  ballotlem2  34796  ballotlemfc0  34800  ballotlemfcc  34801  signstf0  34872  signsvf0  34884  hgt750lemd  34952  hgt750lem  34955  0nn0m1nnn0  35475  revpfxsfxrev  35478  subfacval2  35550  cvmliftlem4  35651  cvmliftlem5  35652  fz0n  36094  bcneg1  36099  bccolsum  36102  fwddifn0  36527  fwddifnp1  36528  knoppcnlem8  36951  knoppcnlem11  36954  poimirlem24  38155  poimirlem27  38158  poimirlem28  38159  sdclem1  38254  heibor1lem  38320  heiborlem4  38325  bccl2d  42620  aks6d1c1  42745  aks6d1c2lem4  42756  0dvds0  42948  mzpnegmpt  43337  diophrw  43352  vdioph  43372  diophren  43402  irrapxlem1  43411  rmxy0  43512  monotoddzzfi  43531  zindbi  43535  rmyeq0  43542  jm2.18  43577  jm2.15nn0  43592  jm2.16nn0  43593  mpaaeu  43739  nzss  44891  hashnzfz2  44895  dvradcnv2  44921  binomcxplemnn0  44923  binomcxplemrat  44924  binomcxplemnotnn0  44930  halffl  45873  lmbr3v  46317  dvnmul  46515  stoweidlem11  46583  stoweidlem17  46589  stirlinglem7  46652  fourierdlem20  46699  etransclem25  46831  etransclem26  46832  etransclem37  46843  smfmullem4  47366  chnsubseqwl  47453  2ffzoeq  47920  fmtnorec2  48150  0evenALTV  48308  0noddALTV  48309  2exp340mod341  48353  8exp8mod9  48356  nfermltl8rev  48362  gpgusgralem  48676  1odd  48791  0even  48857  2zrngamgm  48865  altgsumbcALT  48984  blen1  49215  blen1b  49219  0dig1  49240  0dig2pr01  49241  nn0sumshdiglem1  49252  itcoval0  49293  ackval0  49311  aacllem  50430