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

Theorem 0z 10644
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 9373 . 2  |-  0  e.  RR
2 eqid 2433 . . 3  |-  0  =  0
323mix1i 1153 . 2  |-  ( 0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN )
4 elz 10635 . 2  |-  ( 0  e.  ZZ  <->  ( 0  e.  RR  /\  (
0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN ) ) )
51, 3, 4mpbir2an 904 1  |-  0  e.  ZZ
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 957    = wceq 1362    e. wcel 1755   RRcr 9268   0cc0 9269   -ucneg 9583   NNcn 10309   ZZcz 10633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-1cn 9327  ax-icn 9328  ax-addcl 9329  ax-addrcl 9330  ax-mulcl 9331  ax-mulrcl 9332  ax-i2m1 9337  ax-1ne0 9338  ax-rnegex 9340  ax-rrecex 9341  ax-cnre 9342
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-neg 9585  df-z 10634
This theorem is referenced by:  0zd  10645  elnn0z  10646  nn0ssz  10654  znegcl  10667  zgt0ge1  10685  nn0lt10b  10693  nnm1ge0  10697  recnz  10704  gtndiv  10706  zeo  10714  nn0ind  10725  fnn0ind  10728  eluzadd  10876  eluzsub  10877  nn0uz  10882  1eluzge0  10886  2eluzge0  10887  nn0infm  10923  eqreznegel  10927  fz10  11456  fz01en  11463  elfzelfzelfz  11470  fz0tp  11497  fznn0  11507  1fv  11515  fzshftral  11530  lbfzo0  11569  fzo01  11595  fzo0to2pr  11597  fzo0to3tp  11598  injresinj  11622  flge0nn0  11649  btwnzge0  11656  zmodfz  11712  modid  11715  zmodid2  11719  ltweuz  11767  uzenom  11770  fzennn  11773  cardfz  11775  hashgf1o  11776  seqfn  11801  seq1  11802  seqp1  11804  exp0  11852  bcnn  12071  bcm1k  12074  bcval5  12077  bcpasc  12080  hashgadd  12123  hashge2el2dif  12167  hashbc  12189  fz1isolem  12197  brfi1uzind  12202  lswccat0lsw  12271  eqs1  12283  s111  12285  swrdlend  12308  swrd0  12310  wrdeqswrdlsw  12326  swrds1  12328  repswswrd  12405  cshw0  12414  s2f1o  12509  f1oun2prg  12510  rexfiuz  12818  climz  13010  climaddc1  13095  climmulc2  13097  climsubc1  13098  climsubc2  13099  climlec2  13119  sumss  13184  binomlem  13274  binom  13275  bcxmas  13280  climcndslem1  13294  arisum2  13305  explecnv  13309  geomulcvg  13318  ef0lem  13346  efcvgfsum  13353  ege2le3  13357  eftlub  13375  efgt1p2  13380  efgt1p  13381  ruclem4  13498  ruclem6  13499  nthruc  13515  dvds0  13530  0dvds  13535  fsumdvds  13558  odd2np1lem  13573  divalglem6  13584  divalglem7  13585  divalglem8  13586  bitsfzo  13613  bitsmod  13614  0bits  13617  m1bits  13618  sadc0  13632  smup0  13657  gcd0val  13675  gcddvds  13681  gcd0id  13689  gcdid0  13690  gcdaddm  13695  gcdid  13697  bezoutlem1  13704  bezout  13708  dfphi2  13831  phiprmpw  13833  prmdiveq  13843  prmdivdiv  13844  pc0  13903  pcdvdstr  13924  pcfaclem  13942  prmreclem2  13960  prmreclem4  13962  zgz  13976  igz  13977  4sqlem19  14006  vdwap0  14019  ramz  14068  1259lem1  14137  1259lem4  14140  2503lem2  14144  4001lem1  14147  4001lem3  14149  gsumws1  15496  mulg0  15611  dfod2  16044  zaddablx  16329  0cyg  16348  psrbaglefi  17374  psrbaglefiOLD  17375  ltbwe  17485  zring0  17734  zrng0  17740  zndvds0  17824  iscmet3lem3  20642  vitalilem1  20929  iblcnlem1  21106  itgcnlem  21108  dvn0  21239  dvexp3  21291  plyco  21593  0dgr  21597  0dgrb  21598  coefv0  21599  coemulc  21606  vieta1lem2  21661  vieta1  21662  elqaalem1  21669  elqaalem3  21671  aareccl  21676  aannenlem1  21678  aannenlem2  21679  aalioulem1  21682  taylfval  21708  taylplem1  21712  taylplem2  21713  taylpfval  21714  dvtaylp  21719  dvradcnv  21770  pserulm  21771  pserdvlem2  21777  abelthlem6  21785  abelthlem9  21789  logf1o2  21979  advlogexp  21984  ang180lem3  22091  1cubr  22121  leibpi  22221  log2ublem3  22227  fsumharmonic  22289  wilthlem1  22290  muf  22362  0sgm  22366  1sgmprm  22422  ppiub  22427  bposlem1  22507  bposlem2  22508  lgslem2  22520  lgsfcl2  22525  lgsval2lem  22529  lgs0  22532  lgsdir2lem3  22548  lgsdirnn0  22562  lgsdinn0  22563  pntrlog2bndlem4  22713  padicabv  22763  ostth2lem2  22767  usgraexvlem  23135  usgraexmpldifpr  23140  usgraexmpl  23141  2trllemD  23278  2trllemG  23279  wlkntrllem2  23281  wlkntrl  23283  0pth  23291  0spth  23292  constr1trl  23309  constr2spthlem1  23315  usgrcyclnl1  23348  usgrcyclnl2  23349  3v3e3cycl1  23352  constr3lem4  23355  constr3trllem3  23360  constr3trllem5  23362  4cycl4v4e  23374  4cycl4dv4e  23376  eupa0  23417  eupares  23418  gx0  23570  zaddsubgo  23663  zringnm  26241  zzsnmOLD  26243  cnzh  26252  qqh0  26266  qqhcn  26273  qqhucn  26274  eulerpartlemmf  26605  ballotlem2  26718  ballotlemfc0  26722  ballotlemfcc  26723  ballotlemodife  26727  plymulx0  26795  signstf0  26816  signsvf0  26828  subfacval2  26922  cvmliftlem4  27024  cvmliftlem5  27025  relexp0  27177  fz0n  27235  4bc2eq6  27237  risefall0lem  27375  binomfallfac  27390  bpoly1  28040  bpolydiflem  28043  bpoly2  28046  bpoly3  28047  bpoly4  28048  sdclem1  28480  heibor1lem  28549  heiborlem4  28554  mzpnegmpt  28922  diophrw  28939  vdioph  28960  diophren  28994  irrapxlem1  29005  rmxy0  29106  monotoddzzfi  29125  zindbi  29129  rmyeq0  29138  jm2.18  29179  jm2.15nn0  29194  jm2.16nn0  29195  mpaaeu  29349  stoweidlem11  29649  stoweidlem17  29655  stoweidlem26  29664  stoweidlem34  29672  stirlinglem7  29718  f13idfv  29991  2ffzoeq  30057  elfzonlteqm1  30068  wlkv0  30134  bj-flbi3  32104
  Copyright terms: Public domain W3C validator