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

Theorem 0z 10876
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 9594 . 2  |-  0  e.  RR
2 eqid 2441 . . 3  |-  0  =  0
323mix1i 1167 . 2  |-  ( 0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN )
4 elz 10867 . 2  |-  ( 0  e.  ZZ  <->  ( 0  e.  RR  /\  (
0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN ) ) )
51, 3, 4mpbir2an 918 1  |-  0  e.  ZZ
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 971    = wceq 1381    e. wcel 1802   RRcr 9489   0cc0 9490   -ucneg 9806   NNcn 10537   ZZcz 10865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-i2m1 9558  ax-1ne0 9559  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-iota 5537  df-fv 5582  df-ov 6280  df-neg 9808  df-z 10866
This theorem is referenced by:  0zd  10877  elnn0z  10878  nn0ssz  10886  znegcl  10900  zgt0ge1  10918  nn0lt10bOLD  10926  nnm1ge0  10932  gtndiv  10941  zeo  10949  nn0ind  10960  fnn0ind  10963  eluzadd  11113  eluzsub  11114  nn0uz  11119  1eluzge0  11128  2eluzge0OLD  11129  nn0infm  11167  eqreznegel  11171  fz10  11710  fz01en  11717  fzshftral  11769  fznn0  11773  fz0tp  11780  elfz0ubfz0  11781  1fv  11795  lbfzo0  11836  elfzonlteqm1  11865  fzo01  11871  fzo0to2pr  11873  fzo0to3tp  11874  flge0nn0  11928  btwnzge0  11935  zmodfz  11991  modid  11994  zmodid2  11998  ltweuz  12046  uzenom  12049  fzennn  12052  cardfz  12054  hashgf1o  12055  f13idfv  12080  seqfn  12093  seq1  12094  seqp1  12096  exp0  12144  bcnn  12364  bcm1k  12367  bcval5  12370  bcpasc  12373  hashgadd  12419  hashbc  12476  fz1isolem  12484  hashge2el2dif  12495  brfi1uzind  12506  lswccat0lsw  12582  eqs1  12595  s111  12597  swrdlend  12630  swrd0  12632  wrdeqswrdlsw  12648  swrds1  12650  repswswrd  12730  cshw0  12739  s2f1o  12838  f1oun2prg  12839  rexfiuz  13154  climz  13346  climaddc1  13431  climmulc2  13433  climsubc1  13434  climsubc2  13435  climlec2  13455  sumss  13520  binomlem  13615  binom  13616  bcxmas  13621  climcndslem1  13635  arisum2  13646  explecnv  13650  geomulcvg  13659  ef0lem  13687  efcvgfsum  13694  ege2le3  13698  eftlub  13716  efgt1p2  13721  efgt1p  13722  ruclem4  13839  ruclem6  13840  nthruc  13856  dvds0  13871  0dvds  13876  fsumdvds  13901  odd2np1lem  13917  divalglem6  13928  divalglem7  13929  divalglem8  13930  bitsfzo  13957  bitsmod  13958  0bits  13961  m1bits  13962  sadc0  13976  smup0  14001  gcd0val  14019  gcddvds  14025  gcd0id  14033  gcdid0  14034  gcdaddm  14039  gcdid  14041  bezoutlem1  14048  bezout  14052  dfphi2  14176  phiprmpw  14178  prmdiveq  14188  prmdivdiv  14189  pc0  14250  pcdvdstr  14271  pcfaclem  14289  prmreclem2  14307  prmreclem4  14309  zgz  14323  igz  14324  4sqlem19  14353  vdwap0  14366  ramz  14415  1259lem1  14485  1259lem4  14488  2503lem2  14492  4001lem1  14495  4001lem3  14497  gsumws1  15876  mulg0  16016  dfod2  16455  zaddablx  16745  0cyg  16764  srgbinomlem4  17062  srgbinom  17064  psrbaglefi  17891  psrbaglefiOLD  17892  ltbwe  18005  zring0  18366  zrng0  18372  zndvds0  18456  pmatcollpw3fi1lem1  19154  pmatcollpw3fi1  19156  iscmet3lem3  21595  vitalilem1  21883  iblcnlem1  22060  itgcnlem  22062  dvn0  22193  dvexp3  22245  plyco  22504  0dgr  22508  0dgrb  22509  coefv0  22510  coemulc  22517  vieta1lem2  22572  vieta1  22573  elqaalem1  22580  elqaalem3  22582  aareccl  22587  aannenlem1  22589  aannenlem2  22590  aalioulem1  22593  taylfval  22619  taylplem1  22623  taylplem2  22624  taylpfval  22625  dvtaylp  22630  dvradcnv  22681  pserulm  22682  pserdvlem2  22688  abelthlem6  22696  abelthlem9  22700  logf1o2  22896  advlogexp  22901  ang180lem3  23008  1cubr  23038  leibpi  23138  log2ublem3  23144  fsumharmonic  23206  wilthlem1  23207  muf  23279  0sgm  23283  1sgmprm  23339  ppiub  23344  bposlem1  23424  bposlem2  23425  lgslem2  23437  lgsfcl2  23442  lgsval2lem  23446  lgs0  23449  lgsdir2lem3  23465  lgsdirnn0  23479  lgsdinn0  23480  pntrlog2bndlem4  23630  padicabv  23680  ostth2lem2  23684  usgraexvlem  24260  usgraexmpldifpr  24265  usgraexmpl  24266  2trllemD  24424  2trllemG  24425  wlkntrllem2  24427  wlkntrl  24429  0pth  24437  0spth  24438  constr1trl  24455  constr2spthlem1  24461  usgrcyclnl1  24505  3v3e3cycl1  24509  constr3lem4  24512  constr3trllem3  24517  constr3trllem5  24519  wlkv0  24625  eupa0  24839  eupares  24840  gx0  25128  zaddsubgo  25221  zringnm  27806  zzsnmOLD  27808  qqh0  27831  qqhcn  27838  qqhucn  27839  eulerpartlemmf  28180  ballotlem2  28293  ballotlemfc0  28297  ballotlemfcc  28298  ballotlemodife  28302  plymulx0  28370  signstf0  28391  signsvf0  28403  subfacval2  28497  cvmliftlem4  28599  cvmliftlem5  28600  relexp0  28918  fz0n  28976  4bc2eq6  28978  risefall0lem  29116  binomfallfac  29131  bpoly1  29781  bpolydiflem  29784  bpoly2  29787  bpoly3  29788  bpoly4  29789  sdclem1  30204  heibor1lem  30273  heiborlem4  30278  mzpnegmpt  30644  diophrw  30660  vdioph  30681  diophren  30715  irrapxlem1  30726  rmxy0  30827  monotoddzzfi  30846  zindbi  30850  rmyeq0  30859  jm2.18  30898  jm2.15nn0  30913  jm2.16nn0  30914  mpaaeu  31068  lcm0val  31169  dvdslcm  31173  lcmeq0  31175  lcmgcd  31182  lcmdvds  31183  nzss  31191  hashnzfz2  31195  halffl  31438  stoweidlem11  31678  stoweidlem17  31684  stoweidlem26  31693  stoweidlem34  31701  stirlinglem7  31747  fourierdlem20  31794  2ffzoeq  32175  1odd  32332  0even  32437  2zrngamgm  32445  altgsumbcALT  32650  bj-flbi3  34310
  Copyright terms: Public domain W3C validator