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

Theorem 0z 10758
Description: Zero is an integer. (Contributed by NM, 12-Jan-2002.)
Assertion
Ref Expression
0z  |-  0  e.  ZZ

Proof of Theorem 0z
StepHypRef Expression
1 0re 9487 . 2  |-  0  e.  RR
2 eqid 2451 . . 3  |-  0  =  0
323mix1i 1160 . 2  |-  ( 0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN )
4 elz 10749 . 2  |-  ( 0  e.  ZZ  <->  ( 0  e.  RR  /\  (
0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN ) ) )
51, 3, 4mpbir2an 911 1  |-  0  e.  ZZ
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 964    = wceq 1370    e. wcel 1758   RRcr 9382   0cc0 9383   -ucneg 9697   NNcn 10423   ZZcz 10747
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-i2m1 9451  ax-1ne0 9452  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-ov 6193  df-neg 9699  df-z 10748
This theorem is referenced by:  0zd  10759  elnn0z  10760  nn0ssz  10768  znegcl  10781  zgt0ge1  10799  nn0lt10b  10807  nnm1ge0  10811  recnz  10818  gtndiv  10820  zeo  10828  nn0ind  10839  fnn0ind  10842  eluzadd  10990  eluzsub  10991  nn0uz  10996  1eluzge0  11000  2eluzge0  11001  nn0infm  11037  eqreznegel  11041  fz10  11571  fz01en  11578  elfzelfzelfz  11585  fz0tp  11614  fznn0  11625  1fv  11633  fzshftral  11648  lbfzo0  11687  fzo01  11713  fzo0to2pr  11715  fzo0to3tp  11716  injresinj  11740  flge0nn0  11767  btwnzge0  11774  zmodfz  11830  modid  11833  zmodid2  11837  ltweuz  11885  uzenom  11888  fzennn  11891  cardfz  11893  hashgf1o  11894  seqfn  11919  seq1  11920  seqp1  11922  exp0  11970  bcnn  12189  bcm1k  12192  bcval5  12195  bcpasc  12198  hashgadd  12242  hashge2el2dif  12286  hashbc  12308  fz1isolem  12316  brfi1uzind  12321  lswccat0lsw  12390  eqs1  12402  s111  12404  swrdlend  12427  swrd0  12429  wrdeqswrdlsw  12445  swrds1  12447  repswswrd  12524  cshw0  12533  s2f1o  12628  f1oun2prg  12629  rexfiuz  12937  climz  13129  climaddc1  13214  climmulc2  13216  climsubc1  13217  climsubc2  13218  climlec2  13238  sumss  13303  binomlem  13394  binom  13395  bcxmas  13400  climcndslem1  13414  arisum2  13425  explecnv  13429  geomulcvg  13438  ef0lem  13466  efcvgfsum  13473  ege2le3  13477  eftlub  13495  efgt1p2  13500  efgt1p  13501  ruclem4  13618  ruclem6  13619  nthruc  13635  dvds0  13650  0dvds  13655  fsumdvds  13678  odd2np1lem  13693  divalglem6  13704  divalglem7  13705  divalglem8  13706  bitsfzo  13733  bitsmod  13734  0bits  13737  m1bits  13738  sadc0  13752  smup0  13777  gcd0val  13795  gcddvds  13801  gcd0id  13809  gcdid0  13810  gcdaddm  13815  gcdid  13817  bezoutlem1  13824  bezout  13828  dfphi2  13951  phiprmpw  13953  prmdiveq  13963  prmdivdiv  13964  pc0  14023  pcdvdstr  14044  pcfaclem  14062  prmreclem2  14080  prmreclem4  14082  zgz  14096  igz  14097  4sqlem19  14126  vdwap0  14139  ramz  14188  1259lem1  14257  1259lem4  14260  2503lem2  14264  4001lem1  14267  4001lem3  14269  gsumws1  15619  mulg0  15734  dfod2  16169  zaddablx  16454  0cyg  16473  srgbinomlem4  16747  srgbinom  16749  psrbaglefi  17547  psrbaglefiOLD  17548  ltbwe  17661  zring0  18002  zrng0  18008  zndvds0  18092  iscmet3lem3  20917  vitalilem1  21204  iblcnlem1  21381  itgcnlem  21383  dvn0  21514  dvexp3  21566  plyco  21825  0dgr  21829  0dgrb  21830  coefv0  21831  coemulc  21838  vieta1lem2  21893  vieta1  21894  elqaalem1  21901  elqaalem3  21903  aareccl  21908  aannenlem1  21910  aannenlem2  21911  aalioulem1  21914  taylfval  21940  taylplem1  21944  taylplem2  21945  taylpfval  21946  dvtaylp  21951  dvradcnv  22002  pserulm  22003  pserdvlem2  22009  abelthlem6  22017  abelthlem9  22021  logf1o2  22211  advlogexp  22216  ang180lem3  22323  1cubr  22353  leibpi  22453  log2ublem3  22459  fsumharmonic  22521  wilthlem1  22522  muf  22594  0sgm  22598  1sgmprm  22654  ppiub  22659  bposlem1  22739  bposlem2  22740  lgslem2  22752  lgsfcl2  22757  lgsval2lem  22761  lgs0  22764  lgsdir2lem3  22780  lgsdirnn0  22794  lgsdinn0  22795  pntrlog2bndlem4  22945  padicabv  22995  ostth2lem2  22999  usgraexvlem  23448  usgraexmpldifpr  23453  usgraexmpl  23454  2trllemD  23591  2trllemG  23592  wlkntrllem2  23594  wlkntrl  23596  0pth  23604  0spth  23605  constr1trl  23622  constr2spthlem1  23628  usgrcyclnl1  23661  usgrcyclnl2  23662  3v3e3cycl1  23665  constr3lem4  23668  constr3trllem3  23673  constr3trllem5  23675  4cycl4v4e  23687  4cycl4dv4e  23689  eupa0  23730  eupares  23731  gx0  23883  zaddsubgo  23976  zringnm  26522  zzsnmOLD  26524  cnzh  26533  qqh0  26547  qqhcn  26554  qqhucn  26555  eulerpartlemmf  26892  ballotlem2  27005  ballotlemfc0  27009  ballotlemfcc  27010  ballotlemodife  27014  plymulx0  27082  signstf0  27103  signsvf0  27115  subfacval2  27209  cvmliftlem4  27311  cvmliftlem5  27312  relexp0  27465  fz0n  27523  4bc2eq6  27525  risefall0lem  27663  binomfallfac  27678  bpoly1  28328  bpolydiflem  28331  bpoly2  28334  bpoly3  28335  bpoly4  28336  sdclem1  28777  heibor1lem  28846  heiborlem4  28851  mzpnegmpt  29218  diophrw  29235  vdioph  29256  diophren  29290  irrapxlem1  29301  rmxy0  29402  monotoddzzfi  29421  zindbi  29425  rmyeq0  29434  jm2.18  29475  jm2.15nn0  29490  jm2.16nn0  29491  mpaaeu  29645  stoweidlem11  29944  stoweidlem17  29950  stoweidlem26  29959  stoweidlem34  29967  stirlinglem7  30013  f13idfv  30286  2ffzoeq  30352  elfzonlteqm1  30363  wlkv0  30429  altgsumbcALT  30888  pmatcollpw4fi1lem1  31242  pmatcollpw4fi1  31244  bj-flbi3  32833
  Copyright terms: Public domain W3C validator