Theorem 0z 12731

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

This proof depends on syntax axioms:   ∨ w3o 1102   = wceq 1570   ∈ wcel 2147  ℝcr 11226  0cc0 11227   -cneg 11569  ℕcn 12362  ℤcz 12720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11285  ax-addrcl 11288  ax-rnegex 11298  ax-cnre 11300

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-neg 11571  df-z 12721

This theorem is used by:  0zd  12732  elnn0z  12733  nn0ssz  12743  znegcl  12758  zgt0ge1  12779  0nn0m1nnn0  12780  nnm1ge0  12794  gtndiv  12803  zeo  12812  nn0ind  12821  fnn0ind  12825  nn0uz  13030  1eluzge0  13034  nn0inf  13084  eqreznegel  13088  fz10  13705  fz00m1  13706  fz01en  13713  fzshftral  13776  fznn0  13780  fz1ssfz0  13784  fz0sn  13788  fz0tp  13789  fz0to3un2pr  13790  fz0to4untppr  13791  fz0to5un2tp  13792  elfz0ubfz0  13793  fz0sn0fz1  13806  1fv  13808  fzo0n  13843  lbfzo0  13861  elfzonlteqm1  13903  fzo01  13909  fzo0to2pr  13912  fz01pr  13913  fzo0to3tp  13914  ico01fl0  13986  flge0nn0  13987  divfl0  13991  btwnzge0  13995  zmodfz  14060  modid  14063  zmodid2  14066  modmuladdnn0  14085  ltweuz  14131  uzenom  14134  fzennn  14138  cardfz  14140  hashgf1o  14141  f13idfv  14170  seqfn  14183  seq1  14184  seqp1  14186  exp0  14235  bcnn  14483  bcval5  14489  bcpasc  14492  4bc2eq6  14500  hashgadd  14548  hashbc  14625  fz1isolem  14633  hashge2el2dif  14652  fi1uzind  14679  s111  14791  swrdnd  14832  swrds1  14844  revpfxsfxrev  14945  repswswrd  14963  cshw0  14973  s2f1o  15096  f1oun2prg  15097  rexfiuz  15544  climz  15745  climaddc1  15831  climmulc2  15833  climsubc1  15834  climsubc2  15835  climlec2  15855  sumss  15919  binomlem  16027  binom  16028  bcxmas  16033  climcndslem1  16047  explecnv  16063  geomulcvg  16074  bpoly1  16246  bpolydiflem  16249  bpoly2  16252  bpoly3  16253  bpoly4  16254  ef0lem  16273  efcvgfsum  16281  ege2le3  16285  eftlub  16306  efgt1p2  16311  efgt1p  16312  ruclem4  16431  ruclem6  16432  nthruc  16449  dvds0  16470  0dvds  16475  fsumdvds  16507  odd2np1lem  16539  divalglem6  16597  divalglem7  16598  divalglem8  16599  bitsfzo  16634  bitsmod  16635  0bits  16638  m1bits  16639  sadc0  16653  smup0  16678  gcd0val  16696  gcddvds  16702  gcd0id  16720  gcdid0  16721  gcdaddm  16726  gcdid  16728  bezoutlem1  16741  bezout  16745  dfgcd2  16748  lcm0val  16798  dvdslcm  16802  lcmeq0  16804  lcmgcd  16811  lcmdvds  16812  lcmftp  16840  lcmfunsnlem2  16844  dfphi2  16980  phiprmpw  16982  pc0  17061  pcdvdstr  17083  dvdsprmpweqnn  17092  pcfaclem  17105  prmreclem4  17126  zgz  17140  igz  17141  4sqlem19  17170  ramz  17232  1259lem1  17338  1259lem4  17341  2503lem2  17345  4001lem1  17348  4001lem3  17350  chnub  18825  gsumws1  19063  mulg0  19313  dfod2  19808  zaddablx  20116  0cyg  20137  srgbinomlem4  20485  zringsub  21791  zring0  21794  pzriprnglem3  21819  pzriprnglem4  21820  pzriprnglem5  21821  pzriprnglem6  21822  pzriprnglem10  21826  pzriprng1ALT  21832  zndvds0  21886  ltbwe  22383  pmatcollpw3fi1  23136  iscmet3lem3  25641  ehl1eudis  25771  vitalilem1  25959  itgcnlem  26140  dvn0  26274  dvexp3  26328  plyco  26590  0dgr  26594  0dgrb  26595  coefv0  26597  coemulc  26604  plyn0mulidp  26632  vieta1lem2  26664  vieta1  26665  elqaalem1  26672  elqaalem3  26674  0aa  26679  aareccl  26683  aannenlem1  26685  aannenlem2  26686  aalioulem1  26689  taylfval  26716  taylplem1  26720  taylplem2  26721  taylpfval  26722  dvtaylp  26727  dvradcnv  26778  pserulm  26779  pserdvlem2  26785  abelthlem6  26793  abelthlem9  26797  logf1o2  27008  ang180lem3  27169  1cubr  27200  leibpi  27300  fsumharmonic  27369  muf  27497  0sgm  27501  1sgmprm  27556  ppiub  27561  bposlem1  27641  bposlem2  27642  lgslem2  27655  lgsfcl2  27660  lgsval2lem  27664  lgs0  27667  lgsdir2lem3  27684  lgsdirnn0  27701  lgsdinn0  27702  pntrlog2bndlem4  27937  padicabv  27987  ostth2lem2  27991  usgrexmpldifpr  29869  usgrexmplef  29870  wlkv0  30260  spthispth  30339  dfpth2  30344  uhgrwkspthlem2  30370  pthdlem2  30384  clwwlkccatlem  30610  0ewlk  30735  0wlkons1  30742  0pth  30746  0pthon  30748  wlk2v2elem2  30787  ntrl2v2e  30789  fzo0opth  33465  0dp2dp  33545  cycpmrn  33774  elrgspnlem1  33873  constrextdg2  34451  zringnm  34660  qqh0  34686  qqhcn  34693  qqhucn  34694  rrh0  34717  eulerpartlemmf  35077  ballotlem2  35191  ballotlemfc0  35195  ballotlemfcc  35196  signstf0  35267  signsvf0  35279  hgt750lemd  35347  hgt750lem  35350  subfacval2  36119  cvmliftlem4  36220  cvmliftlem5  36221  fz0n  36674  bcneg1  36679  bccolsum  36682  fwddifn0  37107  fwddifnp1  37108  knoppcnlem8  37544  knoppcnlem11  37547  poimirlem24  38754  poimirlem27  38757  poimirlem28  38758  sdclem1  38869  heibor1lem  38935  heiborlem4  38940  bccl2d  43233  aks6d1c1  43358  aks6d1c2lem4  43369  0dvds0  43577  omexcn  43894  mzpnegmpt  43948  diophrw  43963  vdioph  43983  diophren  44013  irrapxlem1  44022  rmxy0  44123  monotoddzzfi  44142  zindbi  44146  rmyeq0  44153  jm2.18  44188  jm2.15nn0  44203  jm2.16nn0  44204  mpaaeu  44344  k0004val0  45346  nzss  45493  hashnzfz2  45497  dvradcnv2  45523  binomcxplemnn0  45525  binomcxplemrat  45526  binomcxplemnotnn0  45532  halffl  46517  lmbr3v  46960  dvnmul  47158  stoweidlem11  47226  stoweidlem17  47232  stirlinglem7  47295  fourierdlem20  47342  etransclem25  47474  etransclem26  47475  etransclem37  47486  smfmullem4  48009  chnsubseqwl  48094  2ffzoeq  48603  fmtnorec2  48833  0evenALTV  48991  0noddALTV  48992  2exp340mod341  49036  8exp8mod9  49039  nfermltl8rev  49045  gpgusgralem  49359  1odd  49473  0even  49539  2zrngamgm  49547  altgsumbcALT  49670  blen1  49901  blen1b  49905  0dig1  49926  0dig2pr01  49927  nn0sumshdiglem1  49938  itcoval0  49979  ackval0  49997  aacllem  51219