Theorem 0z 12339

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 10986	. 2 ⊢ 0 ∈ ℝ
2		eqid 2739	. . 3 ⊢ 0 = 0
3	2	3mix1i 1332	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12330	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 708	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1085   = wceq 1539   ∈ wcel 2107  ℝcr 10879  0cc0 10880  -cneg 11215  ℕcn 11982  ℤcz 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-1cn 10938  ax-addrcl 10941  ax-rnegex 10951  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-neg 11217  df-z 12329

This theorem is referenced by:  0zd  12340  elnn0z  12341  nn0ssz  12350  znegcl  12364  zgt0ge1  12383  nnm1ge0  12397  gtndiv  12406  zeo  12415  nn0ind  12424  fnn0ind  12428  eluzadd  12622  eluzsub  12623  nn0uz  12629  1eluzge0  12641  nn0inf  12679  eqreznegel  12683  fz10  13286  fz01en  13293  fzshftral  13353  fznn0  13357  fz1ssfz0  13361  fz0sn  13365  fz0tp  13366  fz0to3un2pr  13367  fz0to4untppr  13368  elfz0ubfz0  13369  fz0sn0fz1  13382  1fv  13384  fzo0n  13418  lbfzo0  13436  elfzonlteqm1  13472  fzo01  13478  fzo0to2pr  13481  fzo0to3tp  13482  ico01fl0  13548  flge0nn0  13549  divfl0  13553  btwnzge0  13557  zmodfz  13622  modid  13625  zmodid2  13628  modmuladdnn0  13644  ltweuz  13690  uzenom  13693  fzennn  13697  cardfz  13699  hashgf1o  13700  f13idfv  13729  seqfn  13742  seq1  13743  seqp1  13745  exp0  13795  bcnn  14035  bcval5  14041  bcpasc  14044  4bc2eq6  14052  hashgadd  14101  hashbc  14174  fz1isolem  14184  hashge2el2dif  14203  fi1uzind  14220  s111  14329  swrdnd  14376  swrds1  14388  repswswrd  14506  cshw0  14516  s2f1o  14638  f1oun2prg  14639  rexfiuz  15068  climz  15267  climaddc1  15353  climmulc2  15355  climsubc1  15356  climsubc2  15357  climlec2  15379  sumss  15445  binomlem  15550  binom  15551  bcxmas  15556  climcndslem1  15570  arisum2  15582  explecnv  15586  geomulcvg  15597  risefall0lem  15745  bpoly1  15770  bpolydiflem  15773  bpoly2  15776  bpoly3  15777  bpoly4  15778  ef0lem  15797  efcvgfsum  15804  ege2le3  15808  eftlub  15827  efgt1p2  15832  efgt1p  15833  ruclem4  15952  ruclem6  15953  nthruc  15970  dvds0  15990  0dvds  15995  fsumdvds  16026  odd2np1lem  16058  divalglem6  16116  divalglem7  16117  divalglem8  16118  bitsfzo  16151  bitsmod  16152  0bits  16155  m1bits  16156  sadc0  16170  smup0  16195  gcd0val  16213  gcddvds  16219  gcd0id  16235  gcdid0  16236  gcdaddm  16241  gcdid  16243  bezoutlem1  16256  bezout  16260  dfgcd2  16263  lcm0val  16308  dvdslcm  16312  lcmeq0  16314  lcmgcd  16321  lcmdvds  16322  lcmftp  16350  lcmfunsnlem2  16354  dfphi2  16484  phiprmpw  16486  pc0  16564  pcdvdstr  16586  dvdsprmpweqnn  16595  pcfaclem  16608  prmreclem2  16627  prmreclem4  16629  zgz  16643  igz  16644  4sqlem19  16673  ramz  16735  1259lem1  16841  1259lem4  16844  2503lem2  16848  4001lem1  16851  4001lem3  16853  gsumws1  18485  mulg0  18716  dfod2  19180  zaddablx  19482  0cyg  19503  srgbinomlem4  19788  zring0  20689  zndvds0  20767  ltbwe  21254  pmatcollpw3fi1  21946  iscmet3lem3  24463  vitalilem1  24781  itgcnlem  24963  dvn0  25097  dvexp3  25151  plyco  25411  0dgr  25415  0dgrb  25416  coefv0  25418  coemulc  25425  vieta1lem2  25480  vieta1  25481  elqaalem1  25488  elqaalem3  25490  aareccl  25495  aannenlem1  25497  aannenlem2  25498  aalioulem1  25501  taylfval  25527  taylplem1  25531  taylplem2  25532  taylpfval  25533  dvtaylp  25538  dvradcnv  25589  pserulm  25590  pserdvlem2  25596  abelthlem6  25604  abelthlem9  25608  logf1o2  25814  ang180lem3  25970  1cubr  26001  leibpi  26101  fsumharmonic  26170  muf  26298  0sgm  26302  1sgmprm  26356  ppiub  26361  bposlem1  26441  bposlem2  26442  lgslem2  26455  lgsfcl2  26460  lgsval2lem  26464  lgs0  26467  lgsdir2lem3  26484  lgsdirnn0  26501  lgsdinn0  26502  pntrlog2bndlem4  26737  padicabv  26787  ostth2lem2  26791  usgrexmpldifpr  27634  usgrexmplef  27635  wlkv0  28027  spthispth  28103  uhgrwkspthlem2  28131  pthdlem2  28145  clwwlkccatlem  28362  0ewlk  28487  0wlkons1  28494  0pth  28498  0pthon  28500  wlk2v2elem2  28529  ntrl2v2e  28531  0dp2dp  31192  cycpmrn  31419  zringnm  31917  qqh0  31943  qqhcn  31950  qqhucn  31951  rrh0  31974  eulerpartlemmf  32351  ballotlem2  32464  ballotlemfc0  32468  ballotlemfcc  32469  plymulx0  32535  signstf0  32556  signsvf0  32568  hgt750lemd  32637  hgt750lem  32640  0nn0m1nnn0  33080  revpfxsfxrev  33086  subfacval2  33158  cvmliftlem4  33259  cvmliftlem5  33260  fz0n  33705  bcneg1  33711  bccolsum  33714  fwddifn0  34475  fwddifnp1  34476  knoppcnlem8  34689  knoppcnlem11  34692  poimirlem24  35810  poimirlem27  35813  poimirlem28  35814  sdclem1  35910  heibor1lem  35976  heiborlem4  35981  bccl2d  40007  0dvds0  40333  mzpnegmpt  40573  diophrw  40588  vdioph  40608  diophren  40642  irrapxlem1  40651  rmxy0  40752  monotoddzzfi  40771  zindbi  40775  rmyeq0  40782  jm2.18  40817  jm2.15nn0  40832  jm2.16nn0  40833  mpaaeu  40982  nzss  41942  hashnzfz2  41946  dvradcnv2  41972  binomcxplemnn0  41974  binomcxplemrat  41975  binomcxplemnotnn0  41981  halffl  42842  lmbr3v  43293  dvnmul  43491  stoweidlem11  43559  stoweidlem17  43565  stirlinglem7  43628  fourierdlem20  43675  etransclem25  43807  etransclem26  43808  etransclem37  43819  smfmullem4  44339  2ffzoeq  44831  fmtnorec2  45006  0evenALTV  45151  0noddALTV  45152  2exp340mod341  45196  8exp8mod9  45199  nfermltl8rev  45205  1odd  45376  0even  45500  2zrngamgm  45508  altgsumbcALT  45700  blen1  45941  blen1b  45945  0dig1  45966  0dig2pr01  45967  nn0sumshdiglem1  45978  itcoval0  46019  ackval0  46037  aacllem  46516  upwordnul  46526  tworepnotupword  46532