Theorem 0z 12707

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 11313	. 2 ⊢ 0 ∈ ℝ
2		eqid 2760	. . 3 ⊢ 0 = 0
3	2	3mix1i 1352	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12698	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 724	1 ⊢ 0 ∈ ℤ

This proof depends on syntax axioms:   ∨ w3o 1102   = wceq 1569   ∈ wcel 2144  ℝcr 11202  0cc0 11203   -cneg 11545  ℕcn 12338  ℤcz 12696

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11261  ax-addrcl 11264  ax-rnegex 11274  ax-cnre 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-neg 11547  df-z 12697

This theorem is used by:  0zd  12708  elnn0z  12709  nn0ssz  12719  znegcl  12734  zgt0ge1  12755  0nn0m1nnn0  12756  nnm1ge0  12770  gtndiv  12779  zeo  12788  nn0ind  12797  fnn0ind  12801  nn0uz  13006  1eluzge0  13010  nn0inf  13060  eqreznegel  13064  fz10  13681  fz00m1  13682  fz01en  13689  fzshftral  13752  fznn0  13756  fz1ssfz0  13760  fz0sn  13764  fz0tp  13765  fz0to3un2pr  13766  fz0to4untppr  13767  fz0to5un2tp  13768  elfz0ubfz0  13769  fz0sn0fz1  13782  1fv  13784  fzo0n  13819  lbfzo0  13837  elfzonlteqm1  13879  fzo01  13885  fzo0to2pr  13888  fz01pr  13889  fzo0to3tp  13890  ico01fl0  13962  flge0nn0  13963  divfl0  13967  btwnzge0  13971  zmodfz  14036  modid  14039  zmodid2  14042  modmuladdnn0  14061  ltweuz  14107  uzenom  14110  fzennn  14114  cardfz  14116  hashgf1o  14117  f13idfv  14146  seqfn  14159  seq1  14160  seqp1  14162  exp0  14211  bcnn  14459  bcval5  14465  bcpasc  14468  4bc2eq6  14476  hashgadd  14524  hashbc  14601  fz1isolem  14609  hashge2el2dif  14628  fi1uzind  14655  s111  14767  swrdnd  14808  swrds1  14820  revpfxsfxrev  14921  repswswrd  14939  cshw0  14949  s2f1o  15072  f1oun2prg  15073  rexfiuz  15520  climz  15721  climaddc1  15807  climmulc2  15809  climsubc1  15810  climsubc2  15811  climlec2  15831  sumss  15895  binomlem  16003  binom  16004  bcxmas  16009  climcndslem1  16023  explecnv  16039  geomulcvg  16050  bpoly1  16222  bpolydiflem  16225  bpoly2  16228  bpoly3  16229  bpoly4  16230  ef0lem  16249  efcvgfsum  16257  ege2le3  16261  eftlub  16282  efgt1p2  16287  efgt1p  16288  ruclem4  16407  ruclem6  16408  nthruc  16425  dvds0  16446  0dvds  16451  fsumdvds  16483  odd2np1lem  16515  divalglem6  16573  divalglem7  16574  divalglem8  16575  bitsfzo  16610  bitsmod  16611  0bits  16614  m1bits  16615  sadc0  16629  smup0  16654  gcd0val  16672  gcddvds  16678  gcd0id  16696  gcdid0  16697  gcdaddm  16702  gcdid  16704  bezoutlem1  16717  bezout  16721  dfgcd2  16724  lcm0val  16774  dvdslcm  16778  lcmeq0  16780  lcmgcd  16787  lcmdvds  16788  lcmftp  16816  lcmfunsnlem2  16820  dfphi2  16956  phiprmpw  16958  pc0  17037  pcdvdstr  17059  dvdsprmpweqnn  17068  pcfaclem  17081  prmreclem4  17102  zgz  17116  igz  17117  4sqlem19  17146  ramz  17208  1259lem1  17314  1259lem4  17317  2503lem2  17321  4001lem1  17324  4001lem3  17326  chnub  18801  gsumws1  19039  mulg0  19289  dfod2  19783  zaddablx  20091  0cyg  20112  srgbinomlem4  20460  zringsub  21766  zring0  21769  pzriprnglem3  21794  pzriprnglem4  21795  pzriprnglem5  21796  pzriprnglem6  21797  pzriprnglem10  21801  pzriprng1ALT  21807  zndvds0  21861  ltbwe  22358  pmatcollpw3fi1  23111  iscmet3lem3  25616  ehl1eudis  25746  vitalilem1  25934  itgcnlem  26115  dvn0  26249  dvexp3  26303  plyco  26565  0dgr  26569  0dgrb  26570  coefv0  26572  coemulc  26579  plyn0mulidp  26607  vieta1lem2  26639  vieta1  26640  elqaalem1  26647  elqaalem3  26649  0aa  26654  aareccl  26658  aannenlem1  26660  aannenlem2  26661  aalioulem1  26664  taylfval  26691  taylplem1  26695  taylplem2  26696  taylpfval  26697  dvtaylp  26702  dvradcnv  26753  pserulm  26754  pserdvlem2  26760  abelthlem6  26768  abelthlem9  26772  logf1o2  26983  ang180lem3  27144  1cubr  27175  leibpi  27275  fsumharmonic  27344  muf  27472  0sgm  27476  1sgmprm  27531  ppiub  27536  bposlem1  27616  bposlem2  27617  lgslem2  27630  lgsfcl2  27635  lgsval2lem  27639  lgs0  27642  lgsdir2lem3  27659  lgsdirnn0  27676  lgsdinn0  27677  pntrlog2bndlem4  27912  padicabv  27962  ostth2lem2  27966  usgrexmpldifpr  29844  usgrexmplef  29845  wlkv0  30235  spthispth  30314  dfpth2  30319  uhgrwkspthlem2  30345  pthdlem2  30359  clwwlkccatlem  30585  0ewlk  30710  0wlkons1  30717  0pth  30721  0pthon  30723  wlk2v2elem2  30762  ntrl2v2e  30764  fzo0opth  33441  0dp2dp  33521  cycpmrn  33750  elrgspnlem1  33849  constrextdg2  34427  zringnm  34636  qqh0  34662  qqhcn  34669  qqhucn  34670  rrh0  34693  eulerpartlemmf  35053  ballotlem2  35167  ballotlemfc0  35171  ballotlemfcc  35172  signstf0  35243  signsvf0  35255  hgt750lemd  35323  hgt750lem  35326  subfacval2  36038  cvmliftlem4  36139  cvmliftlem5  36140  fz0n  36588  bcneg1  36593  bccolsum  36596  fwddifn0  37021  fwddifnp1  37022  knoppcnlem8  37458  knoppcnlem11  37461  poimirlem24  38655  poimirlem27  38658  poimirlem28  38659  sdclem1  38770  heibor1lem  38836  heiborlem4  38841  bccl2d  43134  aks6d1c1  43259  aks6d1c2lem4  43270  0dvds0  43477  omexcn  43794  mzpnegmpt  43848  diophrw  43863  vdioph  43883  diophren  43913  irrapxlem1  43922  rmxy0  44023  monotoddzzfi  44042  zindbi  44046  rmyeq0  44053  jm2.18  44088  jm2.15nn0  44103  jm2.16nn0  44104  mpaaeu  44245  k0004val0  45247  nzss  45394  hashnzfz2  45398  dvradcnv2  45424  binomcxplemnn0  45426  binomcxplemrat  45427  binomcxplemnotnn0  45433  halffl  46405  lmbr3v  46848  dvnmul  47046  stoweidlem11  47114  stoweidlem17  47120  stirlinglem7  47183  fourierdlem20  47230  etransclem25  47362  etransclem26  47363  etransclem37  47374  smfmullem4  47897  chnsubseqwl  47982  2ffzoeq  48491  fmtnorec2  48721  0evenALTV  48879  0noddALTV  48880  2exp340mod341  48924  8exp8mod9  48927  nfermltl8rev  48933  gpgusgralem  49247  1odd  49361  0even  49427  2zrngamgm  49435  altgsumbcALT  49558  blen1  49789  blen1b  49793  0dig1  49814  0dig2pr01  49815  nn0sumshdiglem1  49826  itcoval0  49867  ackval0  49885  aacllem  51107