MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0z Structured version   Visualization version   GIF version

Theorem 0z 11426
Description: Zero is an integer. (Contributed by NM, 12-Jan-2002.)
Assertion
Ref Expression
0z 0 ∈ ℤ

Proof of Theorem 0z
StepHypRef Expression
1 0re 10078 . 2 0 ∈ ℝ
2 eqid 2651 . . 3 0 = 0
323mix1i 1253 . 2 (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4 elz 11417 . 2 (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
51, 3, 4mpbir2an 975 1 0 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  w3o 1053   = wceq 1523  wcel 2030  cr 9973  0cc0 9974  -cneg 10305  cn 11058  cz 11415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-neg 10307  df-z 11416
This theorem is referenced by:  0zd  11427  elnn0z  11428  nn0ssz  11436  znegcl  11450  zgt0ge1  11469  nnm1ge0  11483  gtndiv  11492  zeo  11501  nn0ind  11510  fnn0ind  11514  eluzadd  11754  eluzsub  11755  nn0uz  11760  1eluzge0  11770  nn0inf  11808  eqreznegel  11812  fz10  12400  fz01en  12407  fzshftral  12466  fznn0  12470  fz1ssfz0  12474  fz0sn  12478  fz0tp  12479  fz0to3un2pr  12480  fz0to4untppr  12481  elfz0ubfz0  12482  fz0sn0fz1  12495  1fv  12497  fzo0n  12529  lbfzo0  12547  elfzonlteqm1  12583  fzo01  12590  fzo0to2pr  12593  fzo0to3tp  12594  ico01fl0  12660  flge0nn0  12661  divfl0  12665  btwnzge0  12669  zmodfz  12732  modid  12735  zmodid2  12738  modmuladdnn0  12754  ltweuz  12800  uzenom  12803  fzennn  12807  cardfz  12809  hashgf1o  12810  f13idfv  12840  seqfn  12853  seq1  12854  seqp1  12856  exp0  12904  bcnn  13139  bcval5  13145  bcpasc  13148  4bc2eq6  13156  hashgadd  13204  hashbc  13275  fz1isolem  13283  hashge2el2dif  13300  fi1uzind  13317  s111  13432  swrdnd  13478  swrds1  13497  repswswrd  13577  cshw0  13586  s2f1o  13707  f1oun2prg  13708  rexfiuz  14131  climz  14324  climaddc1  14409  climmulc2  14411  climsubc1  14412  climsubc2  14413  climlec2  14433  sumss  14499  binomlem  14605  binom  14606  bcxmas  14611  climcndslem1  14625  arisum2  14637  explecnv  14641  geomulcvg  14651  risefall0lem  14801  binomfallfac  14816  bpoly1  14826  bpolydiflem  14829  bpoly2  14832  bpoly3  14833  bpoly4  14834  ef0lem  14853  efcvgfsum  14860  ege2le3  14864  eftlub  14883  efgt1p2  14888  efgt1p  14889  ruclem4  15007  ruclem6  15008  nthruc  15025  dvds0  15044  0dvds  15049  fsumdvds  15077  odd2np1lem  15111  divalglem6  15168  divalglem7  15169  divalglem8  15170  bitsfzo  15204  bitsmod  15205  0bits  15208  m1bits  15209  sadc0  15223  smup0  15248  gcd0val  15266  gcddvds  15272  gcd0id  15287  gcdid0  15288  gcdaddm  15293  gcdid  15295  bezoutlem1  15303  bezout  15307  dfgcd2  15310  lcm0val  15354  dvdslcm  15358  lcmeq0  15360  lcmgcd  15367  lcmdvds  15368  lcmftp  15396  lcmfunsnlem2  15400  dfphi2  15526  phiprmpw  15528  pc0  15606  pcdvdstr  15627  dvdsprmpweqnn  15636  pcfaclem  15649  prmreclem2  15668  prmreclem4  15670  zgz  15684  igz  15685  4sqlem19  15714  vdwap0  15727  ramz  15776  1259lem1  15885  1259lem4  15888  2503lem2  15892  4001lem1  15895  4001lem3  15897  gsumws1  17423  mulg0  17593  dfod2  18027  zaddablx  18321  0cyg  18340  srgbinomlem4  18589  srgbinom  18591  ltbwe  19520  zring0  19876  zndvds0  19947  pmatcollpw3fi1lem1  20639  pmatcollpw3fi1  20641  iscmet3lem3  23134  vitalilem1  23422  iblcnlem1  23599  itgcnlem  23601  dvn0  23732  dvexp3  23786  plyco  24042  0dgr  24046  0dgrb  24047  coefv0  24049  coemulc  24056  vieta1lem2  24111  vieta1  24112  elqaalem1  24119  elqaalem3  24121  aareccl  24126  aannenlem1  24128  aannenlem2  24129  aalioulem1  24132  taylfval  24158  taylplem1  24162  taylplem2  24163  taylpfval  24164  dvtaylp  24169  dvradcnv  24220  pserulm  24221  pserdvlem2  24227  abelthlem6  24235  abelthlem9  24239  logf1o2  24441  ang180lem3  24586  1cubr  24614  leibpi  24714  fsumharmonic  24783  muf  24911  0sgm  24915  1sgmprm  24969  ppiub  24974  bposlem1  25054  bposlem2  25055  lgslem2  25068  lgsfcl2  25073  lgsval2lem  25077  lgs0  25080  lgsdir2lem3  25097  lgsdirnn0  25114  lgsdinn0  25115  pntrlog2bndlem4  25314  padicabv  25364  ostth2lem2  25368  usgrexmpldifpr  26195  usgrexmplef  26196  wlkv0  26603  spthispth  26678  uhgrwkspthlem2  26706  pthdlem2  26720  0ewlk  27092  0wlkons1  27099  0pth  27103  0pthon  27105  wlk2v2elem2  27134  ntrl2v2e  27136  clwwlkccatlem  27331  0dp2dp  29745  zringnm  30132  qqh0  30156  qqhcn  30163  qqhucn  30164  rrh0  30187  eulerpartlemmf  30565  ballotlem2  30678  ballotlemfc0  30682  ballotlemfcc  30683  plymulx0  30752  signstf0  30773  signsvf0  30785  hgt750lemd  30854  hgt750lem  30857  subfacval2  31295  cvmliftlem4  31396  cvmliftlem5  31397  fz0n  31742  bcneg1  31748  bccolsum  31751  fwddifn0  32396  fwddifnp1  32397  knoppcnlem8  32615  knoppcnlem11  32618  poimirlem24  33563  poimirlem27  33566  poimirlem28  33567  sdclem1  33669  heibor1lem  33738  heiborlem4  33743  mzpnegmpt  37624  diophrw  37639  vdioph  37660  diophren  37694  irrapxlem1  37703  rmxy0  37805  monotoddzzfi  37824  zindbi  37828  rmyeq0  37837  jm2.18  37872  jm2.15nn0  37887  jm2.16nn0  37888  mpaaeu  38037  nzss  38833  hashnzfz2  38837  dvradcnv2  38863  binomcxplemnn0  38865  binomcxplemrat  38866  binomcxplemnotnn0  38872  halffl  39824  lmbr3v  40295  dvnmul  40476  stoweidlem11  40546  stoweidlem17  40552  stirlinglem7  40615  fourierdlem20  40662  etransclem25  40794  etransclem26  40795  etransclem37  40806  smfmullem4  41322  2ffzoeq  41663  fmtnorec2  41780  0evenALTV  41924  0noddALTV  41925  1odd  42136  0even  42256  2zrngamgm  42264  altgsumbcALT  42456  blen1  42703  blen1b  42707  0dig1  42728  0dig2pr01  42729  nn0sumshdiglem1  42740  aacllem  42875
  Copyright terms: Public domain W3C validator