Theorem 0z 12603

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 11211	. 2 ⊢ 0 ∈ ℝ
2		eqid 2763	. . 3 ⊢ 0 = 0
3	2	3mix1i 1352	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12594	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 723	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1102   = wceq 1570   ∈ wcel 2143  ℝcr 11100  0cc0 11101  -cneg 11443  ℕcn 12234  ℤcz 12592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11159  ax-addrcl 11162  ax-rnegex 11172  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-neg 11445  df-z 12593

This theorem is referenced by:  0zd  12604  elnn0z  12605  nn0ssz  12615  znegcl  12630  zgt0ge1  12651  nnm1ge0  12665  gtndiv  12674  zeo  12683  nn0ind  12692  fnn0ind  12696  nn0uz  12901  1eluzge0  12905  nn0inf  12955  eqreznegel  12959  fz10  13574  fz00m1  13575  fz01en  13582  fzshftral  13645  fznn0  13649  fz1ssfz0  13653  fz0sn  13657  fz0tp  13658  fz0to3un2pr  13659  fz0to4untppr  13660  fz0to5un2tp  13661  elfz0ubfz0  13662  fz0sn0fz1  13675  1fv  13677  fzo0n  13712  lbfzo0  13730  elfzonlteqm1  13772  fzo01  13778  fzo0to2pr  13781  fz01pr  13782  fzo0to3tp  13783  ico01fl0  13854  flge0nn0  13855  divfl0  13859  btwnzge0  13863  zmodfz  13928  modid  13931  zmodid2  13934  modmuladdnn0  13953  ltweuz  13999  uzenom  14002  fzennn  14006  cardfz  14008  hashgf1o  14009  f13idfv  14038  seqfn  14051  seq1  14052  seqp1  14054  exp0  14103  bcnn  14350  bcval5  14356  bcpasc  14359  4bc2eq6  14367  hashgadd  14415  hashbc  14492  fz1isolem  14500  hashge2el2dif  14519  fi1uzind  14546  s111  14655  swrdnd  14694  swrds1  14706  repswswrd  14823  cshw0  14833  s2f1o  14955  f1oun2prg  14956  rexfiuz  15401  climz  15602  climaddc1  15688  climmulc2  15690  climsubc1  15691  climsubc2  15692  climlec2  15712  sumss  15777  binomlem  15885  binom  15886  bcxmas  15891  climcndslem1  15905  arisum2  15917  explecnv  15921  geomulcvg  15932  bpoly1  16106  bpolydiflem  16109  bpoly2  16112  bpoly3  16113  bpoly4  16114  ef0lem  16133  efcvgfsum  16141  ege2le3  16145  eftlub  16166  efgt1p2  16171  efgt1p  16172  ruclem4  16291  ruclem6  16292  nthruc  16309  dvds0  16330  0dvds  16335  fsumdvds  16367  odd2np1lem  16399  divalglem6  16457  divalglem7  16458  divalglem8  16459  bitsfzo  16494  bitsmod  16495  0bits  16498  m1bits  16499  sadc0  16513  smup0  16538  gcd0val  16556  gcddvds  16562  gcd0id  16578  gcdid0  16579  gcdaddm  16584  gcdid  16586  bezoutlem1  16598  bezout  16602  dfgcd2  16605  lcm0val  16653  dvdslcm  16657  lcmeq0  16659  lcmgcd  16666  lcmdvds  16667  lcmftp  16695  lcmfunsnlem2  16699  dfphi2  16834  phiprmpw  16836  pc0  16915  pcdvdstr  16937  dvdsprmpweqnn  16946  pcfaclem  16959  prmreclem2  16978  prmreclem4  16980  zgz  16994  igz  16995  4sqlem19  17024  ramz  17086  1259lem1  17192  1259lem4  17195  2503lem2  17199  4001lem1  17202  4001lem3  17204  chnub  18679  gsumws1  18898  mulg0  19141  dfod2  19635  zaddablx  19943  0cyg  19964  srgbinomlem4  20312  zringsub  21586  zring0  21589  pzriprnglem3  21614  pzriprnglem4  21615  pzriprnglem5  21616  pzriprnglem6  21617  pzriprnglem10  21621  pzriprng1ALT  21627  zndvds0  21681  ltbwe  22176  pmatcollpw3fi1  22926  iscmet3lem3  25430  vitalilem1  25748  itgcnlem  25930  dvn0  26064  dvexp3  26118  plyco  26379  0dgr  26383  0dgrb  26384  coefv0  26386  coemulc  26393  plyn0mulidp  26423  vieta1lem2  26453  vieta1  26454  elqaalem1  26461  elqaalem3  26463  aareccl  26468  aannenlem1  26470  aannenlem2  26471  aalioulem1  26474  taylfval  26500  taylplem1  26504  taylplem2  26505  taylpfval  26506  dvtaylp  26511  dvradcnv  26562  pserulm  26563  pserdvlem2  26569  abelthlem6  26577  abelthlem9  26581  logf1o2  26793  ang180lem3  26954  1cubr  26985  leibpi  27085  fsumharmonic  27154  muf  27282  0sgm  27286  1sgmprm  27341  ppiub  27346  bposlem1  27426  bposlem2  27427  lgslem2  27440  lgsfcl2  27445  lgsval2lem  27449  lgs0  27452  lgsdir2lem3  27469  lgsdirnn0  27486  lgsdinn0  27487  pntrlog2bndlem4  27722  padicabv  27772  ostth2lem2  27776  usgrexmpldifpr  29586  usgrexmplef  29587  wlkv0  29977  spthispth  30051  dfpth2  30056  uhgrwkspthlem2  30081  pthdlem2  30095  clwwlkccatlem  30318  0ewlk  30443  0wlkons1  30450  0pth  30454  0pthon  30456  wlk2v2elem2  30485  ntrl2v2e  30487  fzo0opth  33126  0dp2dp  33206  cycpmrn  33441  elrgspnlem1  33540  constrextdg2  34117  zringnm  34326  qqh0  34352  qqhcn  34359  qqhucn  34360  rrh0  34383  eulerpartlemmf  34743  ballotlem2  34857  ballotlemfc0  34861  ballotlemfcc  34862  signstf0  34933  signsvf0  34945  hgt750lemd  35013  hgt750lem  35016  0nn0m1nnn0  35582  revpfxsfxrev  35585  subfacval2  35657  cvmliftlem4  35758  cvmliftlem5  35759  fz0n  36201  bcneg1  36206  bccolsum  36209  fwddifn0  36634  fwddifnp1  36635  knoppcnlem8  37067  knoppcnlem11  37070  poimirlem24  38273  poimirlem27  38276  poimirlem28  38277  sdclem1  38372  heibor1lem  38438  heiborlem4  38443  bccl2d  42736  aks6d1c1  42861  aks6d1c2lem4  42872  0dvds0  43066  mzpnegmpt  43455  diophrw  43470  vdioph  43490  diophren  43520  irrapxlem1  43529  rmxy0  43630  monotoddzzfi  43649  zindbi  43653  rmyeq0  43660  jm2.18  43695  jm2.15nn0  43710  jm2.16nn0  43711  mpaaeu  43857  nzss  45007  hashnzfz2  45011  dvradcnv2  45037  binomcxplemnn0  45039  binomcxplemrat  45040  binomcxplemnotnn0  45046  halffl  45995  lmbr3v  46439  dvnmul  46637  stoweidlem11  46705  stoweidlem17  46711  stirlinglem7  46774  fourierdlem20  46821  etransclem25  46953  etransclem26  46954  etransclem37  46965  smfmullem4  47488  chnsubseqwl  47575  2ffzoeq  48042  fmtnorec2  48272  0evenALTV  48430  0noddALTV  48431  2exp340mod341  48475  8exp8mod9  48478  nfermltl8rev  48484  gpgusgralem  48798  1odd  48913  0even  48979  2zrngamgm  48987  altgsumbcALT  49110  blen1  49341  blen1b  49345  0dig1  49366  0dig2pr01  49367  nn0sumshdiglem1  49378  itcoval0  49419  ackval0  49437  aacllem  50578