Theorem 0z 12499

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

Syntax hints:   ∨ w3o 1085   = wceq 1541   ∈ wcel 2113  ℝcr 11025  0cc0 11026  -cneg 11365  ℕcn 12145  ℤcz 12488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addrcl 11087  ax-rnegex 11097  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489

This theorem is referenced by:  0zd  12500  elnn0z  12501  nn0ssz  12511  znegcl  12526  zgt0ge1  12546  nnm1ge0  12560  gtndiv  12569  zeo  12578  nn0ind  12587  fnn0ind  12591  nn0uz  12789  1eluzge0  12793  nn0inf  12843  eqreznegel  12847  fz10  13461  fz01en  13468  fzshftral  13531  fznn0  13535  fz1ssfz0  13539  fz0sn  13543  fz0tp  13544  fz0to3un2pr  13545  fz0to4untppr  13546  fz0to5un2tp  13547  elfz0ubfz0  13548  fz0sn0fz1  13561  1fv  13563  fzo0n  13597  lbfzo0  13615  elfzonlteqm1  13657  fzo01  13663  fzo0to2pr  13666  fz01pr  13667  fzo0to3tp  13668  ico01fl0  13739  flge0nn0  13740  divfl0  13744  btwnzge0  13748  zmodfz  13813  modid  13816  zmodid2  13819  modmuladdnn0  13838  ltweuz  13884  uzenom  13887  fzennn  13891  cardfz  13893  hashgf1o  13894  f13idfv  13923  seqfn  13936  seq1  13937  seqp1  13939  exp0  13988  bcnn  14235  bcval5  14241  bcpasc  14244  4bc2eq6  14252  hashgadd  14300  hashbc  14376  fz1isolem  14384  hashge2el2dif  14403  fi1uzind  14430  s111  14539  swrdnd  14578  swrds1  14590  repswswrd  14707  cshw0  14717  s2f1o  14839  f1oun2prg  14840  rexfiuz  15271  climz  15472  climaddc1  15558  climmulc2  15560  climsubc1  15561  climsubc2  15562  climlec2  15582  sumss  15647  binomlem  15752  binom  15753  bcxmas  15758  climcndslem1  15772  arisum2  15784  explecnv  15788  geomulcvg  15799  risefall0lem  15949  bpoly1  15974  bpolydiflem  15977  bpoly2  15980  bpoly3  15981  bpoly4  15982  ef0lem  16001  efcvgfsum  16009  ege2le3  16013  eftlub  16034  efgt1p2  16039  efgt1p  16040  ruclem4  16159  ruclem6  16160  nthruc  16177  dvds0  16198  0dvds  16203  fsumdvds  16235  odd2np1lem  16267  divalglem6  16325  divalglem7  16326  divalglem8  16327  bitsfzo  16362  bitsmod  16363  0bits  16366  m1bits  16367  sadc0  16381  smup0  16406  gcd0val  16424  gcddvds  16430  gcd0id  16446  gcdid0  16447  gcdaddm  16452  gcdid  16454  bezoutlem1  16466  bezout  16470  dfgcd2  16473  lcm0val  16521  dvdslcm  16525  lcmeq0  16527  lcmgcd  16534  lcmdvds  16535  lcmftp  16563  lcmfunsnlem2  16567  dfphi2  16701  phiprmpw  16703  pc0  16782  pcdvdstr  16804  dvdsprmpweqnn  16813  pcfaclem  16826  prmreclem2  16845  prmreclem4  16847  zgz  16861  igz  16862  4sqlem19  16891  ramz  16953  1259lem1  17058  1259lem4  17061  2503lem2  17065  4001lem1  17068  4001lem3  17070  chnub  18545  gsumws1  18763  mulg0  19004  dfod2  19493  zaddablx  19801  0cyg  19822  srgbinomlem4  20164  zringsub  21410  zring0  21413  pzriprnglem3  21438  pzriprnglem4  21439  pzriprnglem5  21440  pzriprnglem6  21441  pzriprnglem10  21445  pzriprng1ALT  21451  zndvds0  21505  ltbwe  21999  pmatcollpw3fi1  22732  iscmet3lem3  25246  vitalilem1  25565  itgcnlem  25747  dvn0  25882  dvexp3  25938  plyco  26202  0dgr  26206  0dgrb  26207  coefv0  26209  coemulc  26216  vieta1lem2  26275  vieta1  26276  elqaalem1  26283  elqaalem3  26285  aareccl  26290  aannenlem1  26292  aannenlem2  26293  aalioulem1  26296  taylfval  26322  taylplem1  26326  taylplem2  26327  taylpfval  26328  dvtaylp  26334  dvradcnv  26386  pserulm  26387  pserdvlem2  26394  abelthlem6  26402  abelthlem9  26406  logf1o2  26615  ang180lem3  26777  1cubr  26808  leibpi  26908  fsumharmonic  26978  muf  27106  0sgm  27110  1sgmprm  27166  ppiub  27171  bposlem1  27251  bposlem2  27252  lgslem2  27265  lgsfcl2  27270  lgsval2lem  27274  lgs0  27277  lgsdir2lem3  27294  lgsdirnn0  27311  lgsdinn0  27312  pntrlog2bndlem4  27547  padicabv  27597  ostth2lem2  27601  usgrexmpldifpr  29331  usgrexmplef  29332  wlkv0  29723  spthispth  29797  dfpth2  29802  uhgrwkspthlem2  29827  pthdlem2  29841  clwwlkccatlem  30064  0ewlk  30189  0wlkons1  30196  0pth  30200  0pthon  30202  wlk2v2elem2  30231  ntrl2v2e  30233  fzo0opth  32883  0dp2dp  32990  cycpmrn  33225  elrgspnlem1  33324  constrextdg2  33906  zringnm  34115  qqh0  34141  qqhcn  34148  qqhucn  34149  rrh0  34172  eulerpartlemmf  34532  ballotlem2  34646  ballotlemfc0  34650  ballotlemfcc  34651  plymulx0  34704  signstf0  34725  signsvf0  34737  hgt750lemd  34805  hgt750lem  34808  0nn0m1nnn0  35307  revpfxsfxrev  35310  subfacval2  35381  cvmliftlem4  35482  cvmliftlem5  35483  fz0n  35925  bcneg1  35930  bccolsum  35933  fwddifn0  36358  fwddifnp1  36359  knoppcnlem8  36700  knoppcnlem11  36703  poimirlem24  37841  poimirlem27  37844  poimirlem28  37845  sdclem1  37940  heibor1lem  38006  heiborlem4  38011  bccl2d  42241  aks6d1c1  42366  aks6d1c2lem4  42377  0dvds0  42578  mzpnegmpt  42982  diophrw  42997  vdioph  43017  diophren  43051  irrapxlem1  43060  rmxy0  43161  monotoddzzfi  43180  zindbi  43184  rmyeq0  43191  jm2.18  43226  jm2.15nn0  43241  jm2.16nn0  43242  mpaaeu  43388  nzss  44554  hashnzfz2  44558  dvradcnv2  44584  binomcxplemnn0  44586  binomcxplemrat  44587  binomcxplemnotnn0  44593  halffl  45540  lmbr3v  45985  dvnmul  46183  stoweidlem11  46251  stoweidlem17  46257  stirlinglem7  46320  fourierdlem20  46367  etransclem25  46499  etransclem26  46500  etransclem37  46511  smfmullem4  47034  chnsubseqwl  47119  2ffzoeq  47569  fmtnorec2  47785  0evenALTV  47930  0noddALTV  47931  2exp340mod341  47975  8exp8mod9  47978  nfermltl8rev  47984  gpgusgralem  48298  1odd  48413  0even  48479  2zrngamgm  48487  altgsumbcALT  48595  blen1  48826  blen1b  48830  0dig1  48851  0dig2pr01  48852  nn0sumshdiglem1  48863  itcoval0  48904  ackval0  48922  aacllem  50042