Theorem 0z 12260

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 10908	. 2 ⊢ 0 ∈ ℝ
2		eqid 2738	. . 3 ⊢ 0 = 0
3	2	3mix1i 1331	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12251	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 707	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1084   = wceq 1539   ∈ wcel 2108  ℝcr 10801  0cc0 10802  -cneg 11136  ℕcn 11903  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-addrcl 10863  ax-rnegex 10873  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250

This theorem is referenced by:  0zd  12261  elnn0z  12262  nn0ssz  12271  znegcl  12285  zgt0ge1  12304  nnm1ge0  12318  gtndiv  12327  zeo  12336  nn0ind  12345  fnn0ind  12349  eluzadd  12542  eluzsub  12543  nn0uz  12549  1eluzge0  12561  nn0inf  12599  eqreznegel  12603  fz10  13206  fz01en  13213  fzshftral  13273  fznn0  13277  fz1ssfz0  13281  fz0sn  13285  fz0tp  13286  fz0to3un2pr  13287  fz0to4untppr  13288  elfz0ubfz0  13289  fz0sn0fz1  13302  1fv  13304  fzo0n  13337  lbfzo0  13355  elfzonlteqm1  13391  fzo01  13397  fzo0to2pr  13400  fzo0to3tp  13401  ico01fl0  13467  flge0nn0  13468  divfl0  13472  btwnzge0  13476  zmodfz  13541  modid  13544  zmodid2  13547  modmuladdnn0  13563  ltweuz  13609  uzenom  13612  fzennn  13616  cardfz  13618  hashgf1o  13619  f13idfv  13648  seqfn  13661  seq1  13662  seqp1  13664  exp0  13714  bcnn  13954  bcval5  13960  bcpasc  13963  4bc2eq6  13971  hashgadd  14020  hashbc  14093  fz1isolem  14103  hashge2el2dif  14122  fi1uzind  14139  s111  14248  swrdnd  14295  swrds1  14307  repswswrd  14425  cshw0  14435  s2f1o  14557  f1oun2prg  14558  rexfiuz  14987  climz  15186  climaddc1  15272  climmulc2  15274  climsubc1  15275  climsubc2  15276  climlec2  15298  sumss  15364  binomlem  15469  binom  15470  bcxmas  15475  climcndslem1  15489  arisum2  15501  explecnv  15505  geomulcvg  15516  risefall0lem  15664  bpoly1  15689  bpolydiflem  15692  bpoly2  15695  bpoly3  15696  bpoly4  15697  ef0lem  15716  efcvgfsum  15723  ege2le3  15727  eftlub  15746  efgt1p2  15751  efgt1p  15752  ruclem4  15871  ruclem6  15872  nthruc  15889  dvds0  15909  0dvds  15914  fsumdvds  15945  odd2np1lem  15977  divalglem6  16035  divalglem7  16036  divalglem8  16037  bitsfzo  16070  bitsmod  16071  0bits  16074  m1bits  16075  sadc0  16089  smup0  16114  gcd0val  16132  gcddvds  16138  gcd0id  16154  gcdid0  16155  gcdaddm  16160  gcdid  16162  bezoutlem1  16175  bezout  16179  dfgcd2  16182  lcm0val  16227  dvdslcm  16231  lcmeq0  16233  lcmgcd  16240  lcmdvds  16241  lcmftp  16269  lcmfunsnlem2  16273  dfphi2  16403  phiprmpw  16405  pc0  16483  pcdvdstr  16505  dvdsprmpweqnn  16514  pcfaclem  16527  prmreclem2  16546  prmreclem4  16548  zgz  16562  igz  16563  4sqlem19  16592  ramz  16654  1259lem1  16760  1259lem4  16763  2503lem2  16767  4001lem1  16770  4001lem3  16772  gsumws1  18391  mulg0  18622  dfod2  19086  zaddablx  19388  0cyg  19409  srgbinomlem4  19694  zring0  20592  zndvds0  20670  ltbwe  21155  pmatcollpw3fi1  21845  iscmet3lem3  24359  vitalilem1  24677  itgcnlem  24859  dvn0  24993  dvexp3  25047  plyco  25307  0dgr  25311  0dgrb  25312  coefv0  25314  coemulc  25321  vieta1lem2  25376  vieta1  25377  elqaalem1  25384  elqaalem3  25386  aareccl  25391  aannenlem1  25393  aannenlem2  25394  aalioulem1  25397  taylfval  25423  taylplem1  25427  taylplem2  25428  taylpfval  25429  dvtaylp  25434  dvradcnv  25485  pserulm  25486  pserdvlem2  25492  abelthlem6  25500  abelthlem9  25504  logf1o2  25710  ang180lem3  25866  1cubr  25897  leibpi  25997  fsumharmonic  26066  muf  26194  0sgm  26198  1sgmprm  26252  ppiub  26257  bposlem1  26337  bposlem2  26338  lgslem2  26351  lgsfcl2  26356  lgsval2lem  26360  lgs0  26363  lgsdir2lem3  26380  lgsdirnn0  26397  lgsdinn0  26398  pntrlog2bndlem4  26633  padicabv  26683  ostth2lem2  26687  usgrexmpldifpr  27528  usgrexmplef  27529  wlkv0  27920  spthispth  27995  uhgrwkspthlem2  28023  pthdlem2  28037  clwwlkccatlem  28254  0ewlk  28379  0wlkons1  28386  0pth  28390  0pthon  28392  wlk2v2elem2  28421  ntrl2v2e  28423  0dp2dp  31085  cycpmrn  31312  zringnm  31810  qqh0  31834  qqhcn  31841  qqhucn  31842  rrh0  31865  eulerpartlemmf  32242  ballotlem2  32355  ballotlemfc0  32359  ballotlemfcc  32360  plymulx0  32426  signstf0  32447  signsvf0  32459  hgt750lemd  32528  hgt750lem  32531  0nn0m1nnn0  32971  revpfxsfxrev  32977  subfacval2  33049  cvmliftlem4  33150  cvmliftlem5  33151  fz0n  33602  bcneg1  33608  bccolsum  33611  fwddifn0  34393  fwddifnp1  34394  knoppcnlem8  34607  knoppcnlem11  34610  poimirlem24  35728  poimirlem27  35731  poimirlem28  35732  sdclem1  35828  heibor1lem  35894  heiborlem4  35899  bccl2d  39928  0dvds0  40247  mzpnegmpt  40482  diophrw  40497  vdioph  40517  diophren  40551  irrapxlem1  40560  rmxy0  40661  monotoddzzfi  40680  zindbi  40684  rmyeq0  40691  jm2.18  40726  jm2.15nn0  40741  jm2.16nn0  40742  mpaaeu  40891  nzss  41824  hashnzfz2  41828  dvradcnv2  41854  binomcxplemnn0  41856  binomcxplemrat  41857  binomcxplemnotnn0  41863  halffl  42725  lmbr3v  43176  dvnmul  43374  stoweidlem11  43442  stoweidlem17  43448  stirlinglem7  43511  fourierdlem20  43558  etransclem25  43690  etransclem26  43691  etransclem37  43702  smfmullem4  44215  2ffzoeq  44708  fmtnorec2  44883  0evenALTV  45028  0noddALTV  45029  2exp340mod341  45073  8exp8mod9  45076  nfermltl8rev  45082  1odd  45253  0even  45377  2zrngamgm  45385  altgsumbcALT  45577  blen1  45818  blen1b  45822  0dig1  45843  0dig2pr01  45844  nn0sumshdiglem1  45855  itcoval0  45896  ackval0  45914  aacllem  46391