Theorem 0z 12535

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

Syntax hints:   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ℝcr 11037  0cc0 11038  -cneg 11378  ℕcn 12174  ℤcz 12524

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 2708  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111

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 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525

This theorem is referenced by:  0zd  12536  elnn0z  12537  nn0ssz  12547  znegcl  12562  zgt0ge1  12583  nnm1ge0  12597  gtndiv  12606  zeo  12615  nn0ind  12624  fnn0ind  12628  nn0uz  12826  1eluzge0  12830  nn0inf  12880  eqreznegel  12884  fz10  13499  fz01en  13506  fzshftral  13569  fznn0  13573  fz1ssfz0  13577  fz0sn  13581  fz0tp  13582  fz0to3un2pr  13583  fz0to4untppr  13584  fz0to5un2tp  13585  elfz0ubfz0  13586  fz0sn0fz1  13599  1fv  13601  fzo0n  13636  lbfzo0  13654  elfzonlteqm1  13696  fzo01  13702  fzo0to2pr  13705  fz01pr  13706  fzo0to3tp  13707  ico01fl0  13778  flge0nn0  13779  divfl0  13783  btwnzge0  13787  zmodfz  13852  modid  13855  zmodid2  13858  modmuladdnn0  13877  ltweuz  13923  uzenom  13926  fzennn  13930  cardfz  13932  hashgf1o  13933  f13idfv  13962  seqfn  13975  seq1  13976  seqp1  13978  exp0  14027  bcnn  14274  bcval5  14280  bcpasc  14283  4bc2eq6  14291  hashgadd  14339  hashbc  14415  fz1isolem  14423  hashge2el2dif  14442  fi1uzind  14469  s111  14578  swrdnd  14617  swrds1  14629  repswswrd  14746  cshw0  14756  s2f1o  14878  f1oun2prg  14879  rexfiuz  15310  climz  15511  climaddc1  15597  climmulc2  15599  climsubc1  15600  climsubc2  15601  climlec2  15621  sumss  15686  binomlem  15794  binom  15795  bcxmas  15800  climcndslem1  15814  arisum2  15826  explecnv  15830  geomulcvg  15841  risefall0lem  15991  bpoly1  16016  bpolydiflem  16019  bpoly2  16022  bpoly3  16023  bpoly4  16024  ef0lem  16043  efcvgfsum  16051  ege2le3  16055  eftlub  16076  efgt1p2  16081  efgt1p  16082  ruclem4  16201  ruclem6  16202  nthruc  16219  dvds0  16240  0dvds  16245  fsumdvds  16277  odd2np1lem  16309  divalglem6  16367  divalglem7  16368  divalglem8  16369  bitsfzo  16404  bitsmod  16405  0bits  16408  m1bits  16409  sadc0  16423  smup0  16448  gcd0val  16466  gcddvds  16472  gcd0id  16488  gcdid0  16489  gcdaddm  16494  gcdid  16496  bezoutlem1  16508  bezout  16512  dfgcd2  16515  lcm0val  16563  dvdslcm  16567  lcmeq0  16569  lcmgcd  16576  lcmdvds  16577  lcmftp  16605  lcmfunsnlem2  16609  dfphi2  16744  phiprmpw  16746  pc0  16825  pcdvdstr  16847  dvdsprmpweqnn  16856  pcfaclem  16869  prmreclem2  16888  prmreclem4  16890  zgz  16904  igz  16905  4sqlem19  16934  ramz  16996  1259lem1  17101  1259lem4  17104  2503lem2  17108  4001lem1  17111  4001lem3  17113  chnub  18588  gsumws1  18806  mulg0  19050  dfod2  19539  zaddablx  19847  0cyg  19868  srgbinomlem4  20210  zringsub  21435  zring0  21438  pzriprnglem3  21463  pzriprnglem4  21464  pzriprnglem5  21465  pzriprnglem6  21466  pzriprnglem10  21470  pzriprng1ALT  21476  zndvds0  21530  ltbwe  22022  pmatcollpw3fi1  22753  iscmet3lem3  25257  vitalilem1  25575  itgcnlem  25757  dvn0  25891  dvexp3  25945  plyco  26206  0dgr  26210  0dgrb  26211  coefv0  26213  coemulc  26220  vieta1lem2  26277  vieta1  26278  elqaalem1  26285  elqaalem3  26287  aareccl  26292  aannenlem1  26294  aannenlem2  26295  aalioulem1  26298  taylfval  26324  taylplem1  26328  taylplem2  26329  taylpfval  26330  dvtaylp  26335  dvradcnv  26386  pserulm  26387  pserdvlem2  26393  abelthlem6  26401  abelthlem9  26405  logf1o2  26614  ang180lem3  26775  1cubr  26806  leibpi  26906  fsumharmonic  26975  muf  27103  0sgm  27107  1sgmprm  27162  ppiub  27167  bposlem1  27247  bposlem2  27248  lgslem2  27261  lgsfcl2  27266  lgsval2lem  27270  lgs0  27273  lgsdir2lem3  27290  lgsdirnn0  27307  lgsdinn0  27308  pntrlog2bndlem4  27543  padicabv  27593  ostth2lem2  27597  usgrexmpldifpr  29327  usgrexmplef  29328  wlkv0  29718  spthispth  29792  dfpth2  29797  uhgrwkspthlem2  29822  pthdlem2  29836  clwwlkccatlem  30059  0ewlk  30184  0wlkons1  30191  0pth  30195  0pthon  30197  wlk2v2elem2  30226  ntrl2v2e  30228  fzo0opth  32876  0dp2dp  32968  cycpmrn  33204  elrgspnlem1  33303  constrextdg2  33893  zringnm  34102  qqh0  34128  qqhcn  34135  qqhucn  34136  rrh0  34159  eulerpartlemmf  34519  ballotlem2  34633  ballotlemfc0  34637  ballotlemfcc  34638  plymulx0  34691  signstf0  34712  signsvf0  34724  hgt750lemd  34792  hgt750lem  34795  0nn0m1nnn0  35295  revpfxsfxrev  35298  subfacval2  35369  cvmliftlem4  35470  cvmliftlem5  35471  fz0n  35913  bcneg1  35918  bccolsum  35921  fwddifn0  36346  fwddifnp1  36347  knoppcnlem8  36760  knoppcnlem11  36763  poimirlem24  37965  poimirlem27  37968  poimirlem28  37969  sdclem1  38064  heibor1lem  38130  heiborlem4  38135  bccl2d  42430  aks6d1c1  42555  aks6d1c2lem4  42566  0dvds0  42759  mzpnegmpt  43176  diophrw  43191  vdioph  43211  diophren  43241  irrapxlem1  43250  rmxy0  43351  monotoddzzfi  43370  zindbi  43374  rmyeq0  43381  jm2.18  43416  jm2.15nn0  43431  jm2.16nn0  43432  mpaaeu  43578  nzss  44744  hashnzfz2  44748  dvradcnv2  44774  binomcxplemnn0  44776  binomcxplemrat  44777  binomcxplemnotnn0  44783  halffl  45729  lmbr3v  46173  dvnmul  46371  stoweidlem11  46439  stoweidlem17  46445  stirlinglem7  46508  fourierdlem20  46555  etransclem25  46687  etransclem26  46688  etransclem37  46699  smfmullem4  47222  chnsubseqwl  47309  2ffzoeq  47776  fmtnorec2  48006  0evenALTV  48164  0noddALTV  48165  2exp340mod341  48209  8exp8mod9  48212  nfermltl8rev  48218  gpgusgralem  48532  1odd  48647  0even  48713  2zrngamgm  48721  altgsumbcALT  48829  blen1  49060  blen1b  49064  0dig1  49085  0dig2pr01  49086  nn0sumshdiglem1  49097  itcoval0  49138  ackval0  49156  aacllem  50276