Theorem 0z 11802

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 10439	. 2 ⊢ 0 ∈ ℝ
2		eqid 2771	. . 3 ⊢ 0 = 0
3	2	3mix1i 1314	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 11793	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 699	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1068   = wceq 1508   ∈ wcel 2051  ℝcr 10332  0cc0 10333  -cneg 10669  ℕcn 11437  ℤcz 11791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743  ax-1cn 10391  ax-addrcl 10394  ax-rnegex 10404  ax-cnre 10406

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ral 3086  df-rex 3087  df-rab 3090  df-v 3410  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-iota 6149  df-fv 6193  df-ov 6977  df-neg 10671  df-z 11792

This theorem is referenced by:  0zd  11803  elnn0z  11804  nn0ssz  11814  znegcl  11828  zgt0ge1  11847  nnm1ge0  11861  gtndiv  11870  zeo  11879  nn0ind  11888  fnn0ind  11892  eluzadd  12085  eluzsub  12086  nn0uz  12092  1eluzge0  12104  nn0inf  12142  eqreznegel  12146  fz10  12742  fz01en  12749  fzshftral  12809  fznn0  12813  fz1ssfz0  12817  fz0sn  12821  fz0tp  12822  fz0to3un2pr  12823  fz0to4untppr  12824  elfz0ubfz0  12825  fz0sn0fz1  12838  1fv  12840  fzo0n  12872  lbfzo0  12890  elfzonlteqm1  12926  fzo01  12932  fzo0to2pr  12935  fzo0to3tp  12936  ico01fl0  13002  flge0nn0  13003  divfl0  13007  btwnzge0  13011  zmodfz  13074  modid  13077  zmodid2  13080  modmuladdnn0  13096  ltweuz  13142  uzenom  13145  fzennn  13149  cardfz  13151  hashgf1o  13152  f13idfv  13181  seqfn  13194  seq1  13195  seqp1  13197  exp0  13246  bcnn  13485  bcval5  13491  bcpasc  13494  4bc2eq6  13502  hashgadd  13549  hashbc  13622  fz1isolem  13630  hashge2el2dif  13647  fi1uzind  13664  s111  13776  swrdnd  13820  swrds1  13842  repswswrd  14001  cshw0  14016  s2f1o  14138  f1oun2prg  14139  rexfiuz  14566  climz  14765  climaddc1  14850  climmulc2  14852  climsubc1  14853  climsubc2  14854  climlec2  14874  sumss  14939  binomlem  15042  binom  15043  bcxmas  15048  climcndslem1  15062  arisum2  15074  explecnv  15078  geomulcvg  15090  risefall0lem  15238  bpoly1  15263  bpolydiflem  15266  bpoly2  15269  bpoly3  15270  bpoly4  15271  ef0lem  15290  efcvgfsum  15297  ege2le3  15301  eftlub  15320  efgt1p2  15325  efgt1p  15326  ruclem4  15445  ruclem6  15446  nthruc  15463  dvds0  15483  0dvds  15488  fsumdvds  15516  odd2np1lem  15547  divalglem6  15607  divalglem7  15608  divalglem8  15609  bitsfzo  15642  bitsmod  15643  0bits  15646  m1bits  15647  sadc0  15661  smup0  15686  gcd0val  15704  gcddvds  15710  gcd0id  15725  gcdid0  15726  gcdaddm  15731  gcdid  15733  bezoutlem1  15741  bezout  15745  dfgcd2  15748  lcm0val  15792  dvdslcm  15796  lcmeq0  15798  lcmgcd  15805  lcmdvds  15806  lcmftp  15834  lcmfunsnlem2  15838  dfphi2  15965  phiprmpw  15967  pc0  16045  pcdvdstr  16066  dvdsprmpweqnn  16075  pcfaclem  16088  prmreclem2  16107  prmreclem4  16109  zgz  16123  igz  16124  4sqlem19  16153  ramz  16215  1259lem1  16318  1259lem4  16321  2503lem2  16325  4001lem1  16328  4001lem3  16330  gsumws1  17856  mulg0  18030  dfod2  18464  zaddablx  18760  0cyg  18779  srgbinomlem4  19028  ltbwe  19978  zring0  20344  zndvds0  20414  pmatcollpw3fi1  21115  iscmet3lem3  23611  vitalilem1  23927  itgcnlem  24108  dvn0  24239  dvexp3  24293  plyco  24549  0dgr  24553  0dgrb  24554  coefv0  24556  coemulc  24563  vieta1lem2  24618  vieta1  24619  elqaalem1  24626  elqaalem3  24628  aareccl  24633  aannenlem1  24635  aannenlem2  24636  aalioulem1  24639  taylfval  24665  taylplem1  24669  taylplem2  24670  taylpfval  24671  dvtaylp  24676  dvradcnv  24727  pserulm  24728  pserdvlem2  24734  abelthlem6  24742  abelthlem9  24746  logf1o2  24949  ang180lem3  25105  1cubr  25136  leibpi  25237  fsumharmonic  25306  muf  25434  0sgm  25438  1sgmprm  25492  ppiub  25497  bposlem1  25577  bposlem2  25578  lgslem2  25591  lgsfcl2  25596  lgsval2lem  25600  lgs0  25603  lgsdir2lem3  25620  lgsdirnn0  25637  lgsdinn0  25638  pntrlog2bndlem4  25873  padicabv  25923  ostth2lem2  25927  usgrexmpldifpr  26758  usgrexmplef  26759  wlkv0  27150  spthispth  27230  uhgrwkspthlem2  27258  pthdlem2  27272  clwwlkccatlem  27510  0ewlk  27658  0wlkons1  27665  0pth  27669  0pthon  27671  wlk2v2elem2  27700  ntrl2v2e  27702  0dp2dp  30355  zringnm  30877  qqh0  30901  qqhcn  30908  qqhucn  30909  rrh0  30932  eulerpartlemmf  31310  ballotlem2  31424  ballotlemfc0  31428  ballotlemfcc  31429  plymulx0  31495  signstf0  31516  signsvf0  31530  hgt750lemd  31599  hgt750lem  31602  subfacval2  32056  cvmliftlem4  32157  cvmliftlem5  32158  fz0n  32519  bcneg1  32525  bccolsum  32528  fwddifn0  33183  fwddifnp1  33184  knoppcnlem8  33396  knoppcnlem11  33399  poimirlem24  34394  poimirlem27  34397  poimirlem28  34398  sdclem1  34497  heibor1lem  34566  heiborlem4  34571  mzpnegmpt  38774  diophrw  38789  vdioph  38810  diophren  38844  irrapxlem1  38853  rmxy0  38954  monotoddzzfi  38973  zindbi  38977  rmyeq0  38984  jm2.18  39019  jm2.15nn0  39034  jm2.16nn0  39035  mpaaeu  39184  nzss  40103  hashnzfz2  40107  dvradcnv2  40133  binomcxplemnn0  40135  binomcxplemrat  40136  binomcxplemnotnn0  40142  halffl  41024  lmbr3v  41489  dvnmul  41690  stoweidlem11  41759  stoweidlem17  41765  stirlinglem7  41828  fourierdlem20  41875  etransclem25  42007  etransclem26  42008  etransclem37  42019  smfmullem4  42532  2ffzoeq  42966  fmtnorec2  43105  0evenALTV  43253  0noddALTV  43254  2exp340mod341  43298  8exp8mod9  43301  nfermltl8rev  43307  1odd  43478  0even  43598  2zrngamgm  43606  altgsumbcALT  43797  blen1  44044  blen1b  44048  0dig1  44069  0dig2pr01  44070  nn0sumshdiglem1  44081  aacllem  44301