Theorem 0z 12608

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

Syntax hints:   ∨ w3o 1085   = wceq 1539   ∈ wcel 2107  ℝcr 11137  0cc0 11138  -cneg 11476  ℕcn 12249  ℤcz 12597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-1cn 11196  ax-addrcl 11199  ax-rnegex 11209  ax-cnre 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rex 3060  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-iota 6495  df-fv 6550  df-ov 7417  df-neg 11478  df-z 12598

This theorem is referenced by:  0zd  12609  elnn0z  12610  nn0ssz  12620  znegcl  12636  zgt0ge1  12656  nnm1ge0  12670  gtndiv  12679  zeo  12688  nn0ind  12697  fnn0ind  12701  eluzaddOLD  12896  eluzsubOLD  12897  nn0uz  12903  1eluzge0  12917  nn0inf  12955  eqreznegel  12959  fz10  13568  fz01en  13575  fzshftral  13638  fznn0  13642  fz1ssfz0  13646  fz0sn  13650  fz0tp  13651  fz0to3un2pr  13652  fz0to4untppr  13653  fz0to5un2tp  13654  elfz0ubfz0  13655  fz0sn0fz1  13668  1fv  13670  fzo0n  13704  lbfzo0  13722  elfzonlteqm1  13763  fzo01  13769  fzo0to2pr  13772  fz01pr  13773  fzo0to3tp  13774  ico01fl0  13842  flge0nn0  13843  divfl0  13847  btwnzge0  13851  zmodfz  13916  modid  13919  zmodid2  13922  modmuladdnn0  13939  ltweuz  13985  uzenom  13988  fzennn  13992  cardfz  13994  hashgf1o  13995  f13idfv  14024  seqfn  14037  seq1  14038  seqp1  14040  exp0  14089  bcnn  14334  bcval5  14340  bcpasc  14343  4bc2eq6  14351  hashgadd  14399  hashbc  14475  fz1isolem  14483  hashge2el2dif  14502  fi1uzind  14529  s111  14636  swrdnd  14675  swrds1  14687  repswswrd  14805  cshw0  14815  s2f1o  14938  f1oun2prg  14939  rexfiuz  15369  climz  15568  climaddc1  15654  climmulc2  15656  climsubc1  15657  climsubc2  15658  climlec2  15678  sumss  15743  binomlem  15848  binom  15849  bcxmas  15854  climcndslem1  15868  arisum2  15880  explecnv  15884  geomulcvg  15895  risefall0lem  16045  bpoly1  16070  bpolydiflem  16073  bpoly2  16076  bpoly3  16077  bpoly4  16078  ef0lem  16097  efcvgfsum  16105  ege2le3  16109  eftlub  16128  efgt1p2  16133  efgt1p  16134  ruclem4  16253  ruclem6  16254  nthruc  16271  dvds0  16292  0dvds  16297  fsumdvds  16328  odd2np1lem  16360  divalglem6  16418  divalglem7  16419  divalglem8  16420  bitsfzo  16455  bitsmod  16456  0bits  16459  m1bits  16460  sadc0  16474  smup0  16499  gcd0val  16517  gcddvds  16523  gcd0id  16539  gcdid0  16540  gcdaddm  16545  gcdid  16547  bezoutlem1  16559  bezout  16563  dfgcd2  16566  lcm0val  16614  dvdslcm  16618  lcmeq0  16620  lcmgcd  16627  lcmdvds  16628  lcmftp  16656  lcmfunsnlem2  16660  dfphi2  16794  phiprmpw  16796  pc0  16875  pcdvdstr  16897  dvdsprmpweqnn  16906  pcfaclem  16919  prmreclem2  16938  prmreclem4  16940  zgz  16954  igz  16955  4sqlem19  16984  ramz  17046  1259lem1  17151  1259lem4  17154  2503lem2  17158  4001lem1  17161  4001lem3  17163  gsumws1  18825  mulg0  19066  dfod2  19555  zaddablx  19863  0cyg  19884  srgbinomlem4  20199  zringsub  21433  zring0  21436  pzriprnglem3  21461  pzriprnglem4  21462  pzriprnglem5  21463  pzriprnglem6  21464  pzriprnglem10  21468  pzriprng1ALT  21474  zndvds0  21536  ltbwe  22029  pmatcollpw3fi1  22761  iscmet3lem3  25279  vitalilem1  25598  itgcnlem  25780  dvn0  25915  dvexp3  25971  plyco  26235  0dgr  26239  0dgrb  26240  coefv0  26242  coemulc  26249  vieta1lem2  26308  vieta1  26309  elqaalem1  26316  elqaalem3  26318  aareccl  26323  aannenlem1  26325  aannenlem2  26326  aalioulem1  26329  taylfval  26355  taylplem1  26359  taylplem2  26360  taylpfval  26361  dvtaylp  26367  dvradcnv  26419  pserulm  26420  pserdvlem2  26427  abelthlem6  26435  abelthlem9  26439  logf1o2  26647  ang180lem3  26809  1cubr  26840  leibpi  26940  fsumharmonic  27010  muf  27138  0sgm  27142  1sgmprm  27198  ppiub  27203  bposlem1  27283  bposlem2  27284  lgslem2  27297  lgsfcl2  27302  lgsval2lem  27306  lgs0  27309  lgsdir2lem3  27326  lgsdirnn0  27343  lgsdinn0  27344  pntrlog2bndlem4  27579  padicabv  27629  ostth2lem2  27633  usgrexmpldifpr  29222  usgrexmplef  29223  wlkv0  29616  spthispth  29691  dfpth2  29696  uhgrwkspthlem2  29721  pthdlem2  29735  clwwlkccatlem  29955  0ewlk  30080  0wlkons1  30087  0pth  30091  0pthon  30093  wlk2v2elem2  30122  ntrl2v2e  30124  fzo0opth  32754  0dp2dp  32838  chnub  32948  cycpmrn  33109  elrgspnlem1  33192  constrextdg2  33731  zringnm  33898  qqh0  33926  qqhcn  33933  qqhucn  33934  rrh0  33957  eulerpartlemmf  34318  ballotlem2  34432  ballotlemfc0  34436  ballotlemfcc  34437  plymulx0  34503  signstf0  34524  signsvf0  34536  hgt750lemd  34604  hgt750lem  34607  0nn0m1nnn0  35059  revpfxsfxrev  35062  subfacval2  35133  cvmliftlem4  35234  cvmliftlem5  35235  fz0n  35672  bcneg1  35677  bccolsum  35680  fwddifn0  36106  fwddifnp1  36107  knoppcnlem8  36442  knoppcnlem11  36445  poimirlem24  37592  poimirlem27  37595  poimirlem28  37596  sdclem1  37691  heibor1lem  37757  heiborlem4  37762  bccl2d  41933  aks6d1c1  42058  aks6d1c2lem4  42069  0dvds0  42307  mzpnegmpt  42700  diophrw  42715  vdioph  42735  diophren  42769  irrapxlem1  42778  rmxy0  42880  monotoddzzfi  42899  zindbi  42903  rmyeq0  42910  jm2.18  42945  jm2.15nn0  42960  jm2.16nn0  42961  mpaaeu  43107  nzss  44281  hashnzfz2  44285  dvradcnv2  44311  binomcxplemnn0  44313  binomcxplemrat  44314  binomcxplemnotnn0  44320  halffl  45253  lmbr3v  45705  dvnmul  45903  stoweidlem11  45971  stoweidlem17  45977  stirlinglem7  46040  fourierdlem20  46087  etransclem25  46219  etransclem26  46220  etransclem37  46231  smfmullem4  46754  upwordnul  46840  tworepnotupword  46846  2ffzoeq  47285  fmtnorec2  47476  0evenALTV  47621  0noddALTV  47622  2exp340mod341  47666  8exp8mod9  47669  nfermltl8rev  47675  gpgusgralem  47957  1odd  48033  0even  48099  2zrngamgm  48107  altgsumbcALT  48215  blen1  48451  blen1b  48455  0dig1  48476  0dig2pr01  48477  nn0sumshdiglem1  48488  itcoval0  48529  ackval0  48547  aacllem  49316