Theorem 0z 12565

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

Syntax hints:   ∨ w3o 1086   = wceq 1541   ∈ wcel 2106  ℝcr 11105  0cc0 11106  -cneg 11441  ℕcn 12208  ℤcz 12554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11164  ax-addrcl 11167  ax-rnegex 11177  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-neg 11443  df-z 12555

This theorem is referenced by:  0zd  12566  elnn0z  12567  nn0ssz  12577  znegcl  12593  zgt0ge1  12612  nnm1ge0  12626  gtndiv  12635  zeo  12644  nn0ind  12653  fnn0ind  12657  eluzaddOLD  12853  eluzsubOLD  12854  nn0uz  12860  1eluzge0  12872  nn0inf  12910  eqreznegel  12914  fz10  13518  fz01en  13525  fzshftral  13585  fznn0  13589  fz1ssfz0  13593  fz0sn  13597  fz0tp  13598  fz0to3un2pr  13599  fz0to4untppr  13600  elfz0ubfz0  13601  fz0sn0fz1  13614  1fv  13616  fzo0n  13650  lbfzo0  13668  elfzonlteqm1  13704  fzo01  13710  fzo0to2pr  13713  fzo0to3tp  13714  ico01fl0  13780  flge0nn0  13781  divfl0  13785  btwnzge0  13789  zmodfz  13854  modid  13857  zmodid2  13860  modmuladdnn0  13876  ltweuz  13922  uzenom  13925  fzennn  13929  cardfz  13931  hashgf1o  13932  f13idfv  13961  seqfn  13974  seq1  13975  seqp1  13977  exp0  14027  bcnn  14268  bcval5  14274  bcpasc  14277  4bc2eq6  14285  hashgadd  14333  hashbc  14408  fz1isolem  14418  hashge2el2dif  14437  fi1uzind  14454  s111  14561  swrdnd  14600  swrds1  14612  repswswrd  14730  cshw0  14740  s2f1o  14863  f1oun2prg  14864  rexfiuz  15290  climz  15489  climaddc1  15575  climmulc2  15577  climsubc1  15578  climsubc2  15579  climlec2  15601  sumss  15666  binomlem  15771  binom  15772  bcxmas  15777  climcndslem1  15791  arisum2  15803  explecnv  15807  geomulcvg  15818  risefall0lem  15966  bpoly1  15991  bpolydiflem  15994  bpoly2  15997  bpoly3  15998  bpoly4  15999  ef0lem  16018  efcvgfsum  16025  ege2le3  16029  eftlub  16048  efgt1p2  16053  efgt1p  16054  ruclem4  16173  ruclem6  16174  nthruc  16191  dvds0  16211  0dvds  16216  fsumdvds  16247  odd2np1lem  16279  divalglem6  16337  divalglem7  16338  divalglem8  16339  bitsfzo  16372  bitsmod  16373  0bits  16376  m1bits  16377  sadc0  16391  smup0  16416  gcd0val  16434  gcddvds  16440  gcd0id  16456  gcdid0  16457  gcdaddm  16462  gcdid  16464  bezoutlem1  16477  bezout  16481  dfgcd2  16484  lcm0val  16527  dvdslcm  16531  lcmeq0  16533  lcmgcd  16540  lcmdvds  16541  lcmftp  16569  lcmfunsnlem2  16573  dfphi2  16703  phiprmpw  16705  pc0  16783  pcdvdstr  16805  dvdsprmpweqnn  16814  pcfaclem  16827  prmreclem2  16846  prmreclem4  16848  zgz  16862  igz  16863  4sqlem19  16892  ramz  16954  1259lem1  17060  1259lem4  17063  2503lem2  17067  4001lem1  17070  4001lem3  17072  gsumws1  18715  mulg0  18951  dfod2  19426  zaddablx  19734  0cyg  19755  srgbinomlem4  20045  zring0  21019  zndvds0  21097  ltbwe  21590  pmatcollpw3fi1  22281  iscmet3lem3  24798  vitalilem1  25116  itgcnlem  25298  dvn0  25432  dvexp3  25486  plyco  25746  0dgr  25750  0dgrb  25751  coefv0  25753  coemulc  25760  vieta1lem2  25815  vieta1  25816  elqaalem1  25823  elqaalem3  25825  aareccl  25830  aannenlem1  25832  aannenlem2  25833  aalioulem1  25836  taylfval  25862  taylplem1  25866  taylplem2  25867  taylpfval  25868  dvtaylp  25873  dvradcnv  25924  pserulm  25925  pserdvlem2  25931  abelthlem6  25939  abelthlem9  25943  logf1o2  26149  ang180lem3  26305  1cubr  26336  leibpi  26436  fsumharmonic  26505  muf  26633  0sgm  26637  1sgmprm  26691  ppiub  26696  bposlem1  26776  bposlem2  26777  lgslem2  26790  lgsfcl2  26795  lgsval2lem  26799  lgs0  26802  lgsdir2lem3  26819  lgsdirnn0  26836  lgsdinn0  26837  pntrlog2bndlem4  27072  padicabv  27122  ostth2lem2  27126  usgrexmpldifpr  28504  usgrexmplef  28505  wlkv0  28897  spthispth  28972  uhgrwkspthlem2  29000  pthdlem2  29014  clwwlkccatlem  29231  0ewlk  29356  0wlkons1  29363  0pth  29367  0pthon  29369  wlk2v2elem2  29398  ntrl2v2e  29400  0dp2dp  32062  cycpmrn  32289  zringnm  32926  qqh0  32952  qqhcn  32959  qqhucn  32960  rrh0  32983  eulerpartlemmf  33362  ballotlem2  33475  ballotlemfc0  33479  ballotlemfcc  33480  plymulx0  33546  signstf0  33567  signsvf0  33579  hgt750lemd  33648  hgt750lem  33651  0nn0m1nnn0  34090  revpfxsfxrev  34094  subfacval2  34166  cvmliftlem4  34267  cvmliftlem5  34268  fz0n  34688  bcneg1  34694  bccolsum  34697  fwddifn0  35124  fwddifnp1  35125  knoppcnlem8  35364  knoppcnlem11  35367  poimirlem24  36500  poimirlem27  36503  poimirlem28  36504  sdclem1  36599  heibor1lem  36665  heiborlem4  36670  bccl2d  40845  0dvds0  41212  mzpnegmpt  41467  diophrw  41482  vdioph  41502  diophren  41536  irrapxlem1  41545  rmxy0  41647  monotoddzzfi  41666  zindbi  41670  rmyeq0  41677  jm2.18  41712  jm2.15nn0  41727  jm2.16nn0  41728  mpaaeu  41877  nzss  43061  hashnzfz2  43065  dvradcnv2  43091  binomcxplemnn0  43093  binomcxplemrat  43094  binomcxplemnotnn0  43100  halffl  43992  lmbr3v  44447  dvnmul  44645  stoweidlem11  44713  stoweidlem17  44719  stirlinglem7  44782  fourierdlem20  44829  etransclem25  44961  etransclem26  44962  etransclem37  44973  smfmullem4  45496  upwordnul  45580  tworepnotupword  45586  2ffzoeq  46022  fmtnorec2  46197  0evenALTV  46342  0noddALTV  46343  2exp340mod341  46387  8exp8mod9  46390  nfermltl8rev  46396  1odd  46567  0even  46782  2zrngamgm  46790  altgsumbcALT  46982  blen1  47223  blen1b  47227  0dig1  47248  0dig2pr01  47249  nn0sumshdiglem1  47260  itcoval0  47301  ackval0  47319  aacllem  47801