Theorem 0z 12571

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

Syntax hints:   ∨ w3o 1086   = wceq 1541   ∈ wcel 2106  ℝcr 11111  0cc0 11112  -cneg 11447  ℕcn 12214  ℤcz 12560

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 11170  ax-addrcl 11173  ax-rnegex 11183  ax-cnre 11185

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-neg 11449  df-z 12561

This theorem is referenced by:  0zd  12572  elnn0z  12573  nn0ssz  12583  znegcl  12599  zgt0ge1  12618  nnm1ge0  12632  gtndiv  12641  zeo  12650  nn0ind  12659  fnn0ind  12663  eluzaddOLD  12859  eluzsubOLD  12860  nn0uz  12866  1eluzge0  12878  nn0inf  12916  eqreznegel  12920  fz10  13524  fz01en  13531  fzshftral  13591  fznn0  13595  fz1ssfz0  13599  fz0sn  13603  fz0tp  13604  fz0to3un2pr  13605  fz0to4untppr  13606  elfz0ubfz0  13607  fz0sn0fz1  13620  1fv  13622  fzo0n  13656  lbfzo0  13674  elfzonlteqm1  13710  fzo01  13716  fzo0to2pr  13719  fzo0to3tp  13720  ico01fl0  13786  flge0nn0  13787  divfl0  13791  btwnzge0  13795  zmodfz  13860  modid  13863  zmodid2  13866  modmuladdnn0  13882  ltweuz  13928  uzenom  13931  fzennn  13935  cardfz  13937  hashgf1o  13938  f13idfv  13967  seqfn  13980  seq1  13981  seqp1  13983  exp0  14033  bcnn  14274  bcval5  14280  bcpasc  14283  4bc2eq6  14291  hashgadd  14339  hashbc  14414  fz1isolem  14424  hashge2el2dif  14443  fi1uzind  14460  s111  14567  swrdnd  14606  swrds1  14618  repswswrd  14736  cshw0  14746  s2f1o  14869  f1oun2prg  14870  rexfiuz  15296  climz  15495  climaddc1  15581  climmulc2  15583  climsubc1  15584  climsubc2  15585  climlec2  15607  sumss  15672  binomlem  15777  binom  15778  bcxmas  15783  climcndslem1  15797  arisum2  15809  explecnv  15813  geomulcvg  15824  risefall0lem  15972  bpoly1  15997  bpolydiflem  16000  bpoly2  16003  bpoly3  16004  bpoly4  16005  ef0lem  16024  efcvgfsum  16031  ege2le3  16035  eftlub  16054  efgt1p2  16059  efgt1p  16060  ruclem4  16179  ruclem6  16180  nthruc  16197  dvds0  16217  0dvds  16222  fsumdvds  16253  odd2np1lem  16285  divalglem6  16343  divalglem7  16344  divalglem8  16345  bitsfzo  16378  bitsmod  16379  0bits  16382  m1bits  16383  sadc0  16397  smup0  16422  gcd0val  16440  gcddvds  16446  gcd0id  16462  gcdid0  16463  gcdaddm  16468  gcdid  16470  bezoutlem1  16483  bezout  16487  dfgcd2  16490  lcm0val  16533  dvdslcm  16537  lcmeq0  16539  lcmgcd  16546  lcmdvds  16547  lcmftp  16575  lcmfunsnlem2  16579  dfphi2  16709  phiprmpw  16711  pc0  16789  pcdvdstr  16811  dvdsprmpweqnn  16820  pcfaclem  16833  prmreclem2  16852  prmreclem4  16854  zgz  16868  igz  16869  4sqlem19  16898  ramz  16960  1259lem1  17066  1259lem4  17069  2503lem2  17073  4001lem1  17076  4001lem3  17078  gsumws1  18721  mulg0  18959  dfod2  19434  zaddablx  19742  0cyg  19763  srgbinomlem4  20054  zringsub  21031  zring0  21034  zndvds0  21112  ltbwe  21605  pmatcollpw3fi1  22297  iscmet3lem3  24814  vitalilem1  25132  itgcnlem  25314  dvn0  25448  dvexp3  25502  plyco  25762  0dgr  25766  0dgrb  25767  coefv0  25769  coemulc  25776  vieta1lem2  25831  vieta1  25832  elqaalem1  25839  elqaalem3  25841  aareccl  25846  aannenlem1  25848  aannenlem2  25849  aalioulem1  25852  taylfval  25878  taylplem1  25882  taylplem2  25883  taylpfval  25884  dvtaylp  25889  dvradcnv  25940  pserulm  25941  pserdvlem2  25947  abelthlem6  25955  abelthlem9  25959  logf1o2  26165  ang180lem3  26323  1cubr  26354  leibpi  26454  fsumharmonic  26523  muf  26651  0sgm  26655  1sgmprm  26709  ppiub  26714  bposlem1  26794  bposlem2  26795  lgslem2  26808  lgsfcl2  26813  lgsval2lem  26817  lgs0  26820  lgsdir2lem3  26837  lgsdirnn0  26854  lgsdinn0  26855  pntrlog2bndlem4  27090  padicabv  27140  ostth2lem2  27144  usgrexmpldifpr  28553  usgrexmplef  28554  wlkv0  28946  spthispth  29021  uhgrwkspthlem2  29049  pthdlem2  29063  clwwlkccatlem  29280  0ewlk  29405  0wlkons1  29412  0pth  29416  0pthon  29418  wlk2v2elem2  29447  ntrl2v2e  29449  0dp2dp  32113  cycpmrn  32343  zringnm  33007  qqh0  33033  qqhcn  33040  qqhucn  33041  rrh0  33064  eulerpartlemmf  33443  ballotlem2  33556  ballotlemfc0  33560  ballotlemfcc  33561  plymulx0  33627  signstf0  33648  signsvf0  33660  hgt750lemd  33729  hgt750lem  33732  0nn0m1nnn0  34171  revpfxsfxrev  34175  subfacval2  34247  cvmliftlem4  34348  cvmliftlem5  34349  fz0n  34775  bcneg1  34781  bccolsum  34784  fwddifn0  35211  fwddifnp1  35212  knoppcnlem8  35468  knoppcnlem11  35471  poimirlem24  36604  poimirlem27  36607  poimirlem28  36608  sdclem1  36703  heibor1lem  36769  heiborlem4  36774  bccl2d  40949  0dvds0  41305  mzpnegmpt  41570  diophrw  41585  vdioph  41605  diophren  41639  irrapxlem1  41648  rmxy0  41750  monotoddzzfi  41769  zindbi  41773  rmyeq0  41780  jm2.18  41815  jm2.15nn0  41830  jm2.16nn0  41831  mpaaeu  41980  nzss  43164  hashnzfz2  43168  dvradcnv2  43194  binomcxplemnn0  43196  binomcxplemrat  43197  binomcxplemnotnn0  43203  halffl  44091  lmbr3v  44546  dvnmul  44744  stoweidlem11  44812  stoweidlem17  44818  stirlinglem7  44881  fourierdlem20  44928  etransclem25  45060  etransclem26  45061  etransclem37  45072  smfmullem4  45595  upwordnul  45679  tworepnotupword  45685  2ffzoeq  46121  fmtnorec2  46296  0evenALTV  46441  0noddALTV  46442  2exp340mod341  46486  8exp8mod9  46489  nfermltl8rev  46495  1odd  46666  pzriprnglem3  46892  pzriprnglem4  46893  pzriprnglem5  46894  pzriprnglem6  46895  pzriprnglem10  46899  pzriprng1ALT  46905  0even  46914  2zrngamgm  46922  altgsumbcALT  47114  blen1  47354  blen1b  47358  0dig1  47379  0dig2pr01  47380  nn0sumshdiglem1  47391  itcoval0  47432  ackval0  47450  aacllem  47932