Theorem 0z 12526

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 11137	. 2 ⊢ 0 ∈ ℝ
2		eqid 2737	. . 3 ⊢ 0 = 0
3	2	3mix1i 1335	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12517	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 712	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ℝcr 11028  0cc0 11029  -cneg 11369  ℕcn 12165  ℤcz 12515

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11087  ax-addrcl 11090  ax-rnegex 11100  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-neg 11371  df-z 12516

This theorem is referenced by:  0zd  12527  elnn0z  12528  nn0ssz  12538  znegcl  12553  zgt0ge1  12574  nnm1ge0  12588  gtndiv  12597  zeo  12606  nn0ind  12615  fnn0ind  12619  nn0uz  12817  1eluzge0  12821  nn0inf  12871  eqreznegel  12875  fz10  13490  fz01en  13497  fzshftral  13560  fznn0  13564  fz1ssfz0  13568  fz0sn  13572  fz0tp  13573  fz0to3un2pr  13574  fz0to4untppr  13575  fz0to5un2tp  13576  elfz0ubfz0  13577  fz0sn0fz1  13590  1fv  13592  fzo0n  13627  lbfzo0  13645  elfzonlteqm1  13687  fzo01  13693  fzo0to2pr  13696  fz01pr  13697  fzo0to3tp  13698  ico01fl0  13769  flge0nn0  13770  divfl0  13774  btwnzge0  13778  zmodfz  13843  modid  13846  zmodid2  13849  modmuladdnn0  13868  ltweuz  13914  uzenom  13917  fzennn  13921  cardfz  13923  hashgf1o  13924  f13idfv  13953  seqfn  13966  seq1  13967  seqp1  13969  exp0  14018  bcnn  14265  bcval5  14271  bcpasc  14274  4bc2eq6  14282  hashgadd  14330  hashbc  14406  fz1isolem  14414  hashge2el2dif  14433  fi1uzind  14460  s111  14569  swrdnd  14608  swrds1  14620  repswswrd  14737  cshw0  14747  s2f1o  14869  f1oun2prg  14870  rexfiuz  15301  climz  15502  climaddc1  15588  climmulc2  15590  climsubc1  15591  climsubc2  15592  climlec2  15612  sumss  15677  binomlem  15785  binom  15786  bcxmas  15791  climcndslem1  15805  arisum2  15817  explecnv  15821  geomulcvg  15832  risefall0lem  15982  bpoly1  16007  bpolydiflem  16010  bpoly2  16013  bpoly3  16014  bpoly4  16015  ef0lem  16034  efcvgfsum  16042  ege2le3  16046  eftlub  16067  efgt1p2  16072  efgt1p  16073  ruclem4  16192  ruclem6  16193  nthruc  16210  dvds0  16231  0dvds  16236  fsumdvds  16268  odd2np1lem  16300  divalglem6  16358  divalglem7  16359  divalglem8  16360  bitsfzo  16395  bitsmod  16396  0bits  16399  m1bits  16400  sadc0  16414  smup0  16439  gcd0val  16457  gcddvds  16463  gcd0id  16479  gcdid0  16480  gcdaddm  16485  gcdid  16487  bezoutlem1  16499  bezout  16503  dfgcd2  16506  lcm0val  16554  dvdslcm  16558  lcmeq0  16560  lcmgcd  16567  lcmdvds  16568  lcmftp  16596  lcmfunsnlem2  16600  dfphi2  16735  phiprmpw  16737  pc0  16816  pcdvdstr  16838  dvdsprmpweqnn  16847  pcfaclem  16860  prmreclem2  16879  prmreclem4  16881  zgz  16895  igz  16896  4sqlem19  16925  ramz  16987  1259lem1  17092  1259lem4  17095  2503lem2  17099  4001lem1  17102  4001lem3  17104  chnub  18579  gsumws1  18797  mulg0  19041  dfod2  19530  zaddablx  19838  0cyg  19859  srgbinomlem4  20201  zringsub  21445  zring0  21448  pzriprnglem3  21473  pzriprnglem4  21474  pzriprnglem5  21475  pzriprnglem6  21476  pzriprnglem10  21480  pzriprng1ALT  21486  zndvds0  21540  ltbwe  22032  pmatcollpw3fi1  22763  iscmet3lem3  25267  vitalilem1  25585  itgcnlem  25767  dvn0  25901  dvexp3  25955  plyco  26216  0dgr  26220  0dgrb  26221  coefv0  26223  coemulc  26230  vieta1lem2  26288  vieta1  26289  elqaalem1  26296  elqaalem3  26298  aareccl  26303  aannenlem1  26305  aannenlem2  26306  aalioulem1  26309  taylfval  26335  taylplem1  26339  taylplem2  26340  taylpfval  26341  dvtaylp  26347  dvradcnv  26399  pserulm  26400  pserdvlem2  26406  abelthlem6  26414  abelthlem9  26418  logf1o2  26627  ang180lem3  26788  1cubr  26819  leibpi  26919  fsumharmonic  26989  muf  27117  0sgm  27121  1sgmprm  27176  ppiub  27181  bposlem1  27261  bposlem2  27262  lgslem2  27275  lgsfcl2  27280  lgsval2lem  27284  lgs0  27287  lgsdir2lem3  27304  lgsdirnn0  27321  lgsdinn0  27322  pntrlog2bndlem4  27557  padicabv  27607  ostth2lem2  27611  usgrexmpldifpr  29341  usgrexmplef  29342  wlkv0  29733  spthispth  29807  dfpth2  29812  uhgrwkspthlem2  29837  pthdlem2  29851  clwwlkccatlem  30074  0ewlk  30199  0wlkons1  30206  0pth  30210  0pthon  30212  wlk2v2elem2  30241  ntrl2v2e  30243  fzo0opth  32891  0dp2dp  32983  cycpmrn  33219  elrgspnlem1  33318  constrextdg2  33909  zringnm  34118  qqh0  34144  qqhcn  34151  qqhucn  34152  rrh0  34175  eulerpartlemmf  34535  ballotlem2  34649  ballotlemfc0  34653  ballotlemfcc  34654  plymulx0  34707  signstf0  34728  signsvf0  34740  hgt750lemd  34808  hgt750lem  34811  0nn0m1nnn0  35311  revpfxsfxrev  35314  subfacval2  35385  cvmliftlem4  35486  cvmliftlem5  35487  fz0n  35929  bcneg1  35934  bccolsum  35937  fwddifn0  36362  fwddifnp1  36363  knoppcnlem8  36776  knoppcnlem11  36779  poimirlem24  37979  poimirlem27  37982  poimirlem28  37983  sdclem1  38078  heibor1lem  38144  heiborlem4  38149  bccl2d  42444  aks6d1c1  42569  aks6d1c2lem4  42580  0dvds0  42773  mzpnegmpt  43190  diophrw  43205  vdioph  43225  diophren  43259  irrapxlem1  43268  rmxy0  43369  monotoddzzfi  43388  zindbi  43392  rmyeq0  43399  jm2.18  43434  jm2.15nn0  43449  jm2.16nn0  43450  mpaaeu  43596  nzss  44762  hashnzfz2  44766  dvradcnv2  44792  binomcxplemnn0  44794  binomcxplemrat  44795  binomcxplemnotnn0  44801  halffl  45747  lmbr3v  46191  dvnmul  46389  stoweidlem11  46457  stoweidlem17  46463  stirlinglem7  46526  fourierdlem20  46573  etransclem25  46705  etransclem26  46706  etransclem37  46717  smfmullem4  47240  chnsubseqwl  47325  2ffzoeq  47788  fmtnorec2  48018  0evenALTV  48176  0noddALTV  48177  2exp340mod341  48221  8exp8mod9  48224  nfermltl8rev  48230  gpgusgralem  48544  1odd  48659  0even  48725  2zrngamgm  48733  altgsumbcALT  48841  blen1  49072  blen1b  49076  0dig1  49097  0dig2pr01  49098  nn0sumshdiglem1  49109  itcoval0  49150  ackval0  49168  aacllem  50288