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

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

Proof of Theorem 0z
StepHypRef Expression
1 0re 10323 . 2 0 ∈ ℝ
2 eqid 2806 . . 3 0 = 0
323mix1i 1425 . 2 (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4 elz 11641 . 2 (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
51, 3, 4mpbir2an 693 1 0 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  w3o 1099   = wceq 1637  wcel 2156  cr 10216  0cc0 10217  -cneg 10548  cn 11301  cz 11639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-i2m1 10285  ax-1ne0 10286  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-iota 6060  df-fv 6105  df-ov 6873  df-neg 10550  df-z 11640
This theorem is referenced by:  0zd  11651  elnn0z  11652  nn0ssz  11660  znegcl  11674  zgt0ge1  11693  nnm1ge0  11707  gtndiv  11716  zeo  11725  nn0ind  11734  fnn0ind  11738  eluzadd  11929  eluzsub  11930  nn0uz  11936  1eluzge0  11946  nn0inf  11985  eqreznegel  11989  fz10  12581  fz01en  12588  fzshftral  12647  fznn0  12651  fz1ssfz0  12655  fz0sn  12659  fz0tp  12660  fz0to3un2pr  12661  fz0to4untppr  12662  elfz0ubfz0  12663  fz0sn0fz1  12676  1fv  12678  fzo0n  12710  lbfzo0  12728  elfzonlteqm1  12764  fzo01  12770  fzo0to2pr  12773  fzo0to3tp  12774  ico01fl0  12840  flge0nn0  12841  divfl0  12845  btwnzge0  12849  zmodfz  12912  modid  12915  zmodid2  12918  modmuladdnn0  12934  ltweuz  12980  uzenom  12983  fzennn  12987  cardfz  12989  hashgf1o  12990  f13idfv  13019  seqfn  13032  seq1  13033  seqp1  13035  exp0  13083  bcnn  13315  bcval5  13321  bcpasc  13324  4bc2eq6  13332  hashgadd  13380  hashbc  13450  fz1isolem  13458  hashge2el2dif  13475  fi1uzind  13492  s111  13606  swrdnd  13652  swrds1  13671  repswswrd  13751  cshw0  13760  s2f1o  13881  f1oun2prg  13882  rexfiuz  14306  climz  14499  climaddc1  14584  climmulc2  14586  climsubc1  14587  climsubc2  14588  climlec2  14608  sumss  14674  binomlem  14779  binom  14780  bcxmas  14785  climcndslem1  14799  arisum2  14811  explecnv  14815  geomulcvg  14825  risefall0lem  14973  binomfallfac  14988  bpoly1  14998  bpolydiflem  15001  bpoly2  15004  bpoly3  15005  bpoly4  15006  ef0lem  15025  efcvgfsum  15032  ege2le3  15036  eftlub  15055  efgt1p2  15060  efgt1p  15061  ruclem4  15179  ruclem6  15180  nthruc  15197  dvds0  15216  0dvds  15221  fsumdvds  15249  odd2np1lem  15280  divalglem6  15337  divalglem7  15338  divalglem8  15339  bitsfzo  15372  bitsmod  15373  0bits  15376  m1bits  15377  sadc0  15391  smup0  15416  gcd0val  15434  gcddvds  15440  gcd0id  15455  gcdid0  15456  gcdaddm  15461  gcdid  15463  bezoutlem1  15471  bezout  15475  dfgcd2  15478  lcm0val  15522  dvdslcm  15526  lcmeq0  15528  lcmgcd  15535  lcmdvds  15536  lcmftp  15564  lcmfunsnlem2  15568  dfphi2  15692  phiprmpw  15694  pc0  15772  pcdvdstr  15793  dvdsprmpweqnn  15802  pcfaclem  15815  prmreclem2  15834  prmreclem4  15836  zgz  15850  igz  15851  4sqlem19  15880  vdwap0  15893  ramz  15942  1259lem1  16045  1259lem4  16048  2503lem2  16052  4001lem1  16055  4001lem3  16057  gsumws1  17577  mulg0  17747  dfod2  18178  zaddablx  18472  0cyg  18491  srgbinomlem4  18741  srgbinom  18743  ltbwe  19677  zring0  20032  zndvds0  20102  pmatcollpw3fi1lem1  20800  pmatcollpw3fi1  20802  iscmet3lem3  23296  vitalilem1  23585  iblcnlem1  23764  itgcnlem  23766  dvn0  23897  dvexp3  23951  plyco  24207  0dgr  24211  0dgrb  24212  coefv0  24214  coemulc  24221  vieta1lem2  24276  vieta1  24277  elqaalem1  24284  elqaalem3  24286  aareccl  24291  aannenlem1  24293  aannenlem2  24294  aalioulem1  24297  taylfval  24323  taylplem1  24327  taylplem2  24328  taylpfval  24329  dvtaylp  24334  dvradcnv  24385  pserulm  24386  pserdvlem2  24392  abelthlem6  24400  abelthlem9  24404  logf1o2  24606  ang180lem3  24751  1cubr  24779  leibpi  24879  fsumharmonic  24948  muf  25076  0sgm  25080  1sgmprm  25134  ppiub  25139  bposlem1  25219  bposlem2  25220  lgslem2  25233  lgsfcl2  25238  lgsval2lem  25242  lgs0  25245  lgsdir2lem3  25262  lgsdirnn0  25279  lgsdinn0  25280  pntrlog2bndlem4  25479  padicabv  25529  ostth2lem2  25533  usgrexmpldifpr  26362  usgrexmplef  26363  wlkv0  26771  spthispth  26846  uhgrwkspthlem2  26874  pthdlem2  26888  clwwlkccatlem  27128  0ewlk  27283  0wlkons1  27290  0pth  27294  0pthon  27296  wlk2v2elem2  27325  ntrl2v2e  27327  0dp2dp  29938  zringnm  30325  qqh0  30349  qqhcn  30356  qqhucn  30357  rrh0  30380  eulerpartlemmf  30758  ballotlem2  30871  ballotlemfc0  30875  ballotlemfcc  30876  plymulx0  30945  signstf0  30966  signsvf0  30978  hgt750lemd  31047  hgt750lem  31050  subfacval2  31487  cvmliftlem4  31588  cvmliftlem5  31589  fz0n  31933  bcneg1  31939  bccolsum  31942  fwddifn0  32587  fwddifnp1  32588  knoppcnlem8  32802  knoppcnlem11  32805  poimirlem24  33741  poimirlem27  33744  poimirlem28  33745  sdclem1  33845  heibor1lem  33914  heiborlem4  33919  mzpnegmpt  37803  diophrw  37818  vdioph  37839  diophren  37873  irrapxlem1  37882  rmxy0  37983  monotoddzzfi  38002  zindbi  38006  rmyeq0  38015  jm2.18  38050  jm2.15nn0  38065  jm2.16nn0  38066  mpaaeu  38215  nzss  39010  hashnzfz2  39014  dvradcnv2  39040  binomcxplemnn0  39042  binomcxplemrat  39043  binomcxplemnotnn0  39049  halffl  39985  lmbr3v  40451  dvnmul  40632  stoweidlem11  40701  stoweidlem17  40707  stirlinglem7  40770  fourierdlem20  40817  etransclem25  40949  etransclem26  40950  etransclem37  40961  smfmullem4  41477  2ffzoeq  41907  fmtnorec2  42024  0evenALTV  42168  0noddALTV  42169  1odd  42373  0even  42493  2zrngamgm  42501  altgsumbcALT  42693  blen1  42940  blen1b  42944  0dig1  42965  0dig2pr01  42966  nn0sumshdiglem1  42977  aacllem  43112
  Copyright terms: Public domain W3C validator