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

Theorem 0z 10649
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 9378 . 2  |-  0  e.  RR
2 eqid 2438 . . 3  |-  0  =  0
323mix1i 1160 . 2  |-  ( 0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN )
4 elz 10640 . 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 1369    e. wcel 1756   RRcr 9273   0cc0 9274   -ucneg 9588   NNcn 10314   ZZcz 10638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-neg 9590  df-z 10639
This theorem is referenced by:  0zd  10650  elnn0z  10651  nn0ssz  10659  znegcl  10672  zgt0ge1  10690  nn0lt10b  10698  nnm1ge0  10702  recnz  10709  gtndiv  10711  zeo  10719  nn0ind  10730  fnn0ind  10733  eluzadd  10881  eluzsub  10882  nn0uz  10887  1eluzge0  10891  2eluzge0  10892  nn0infm  10928  eqreznegel  10932  fz10  11462  fz01en  11469  elfzelfzelfz  11476  fz0tp  11505  fznn0  11516  1fv  11524  fzshftral  11539  lbfzo0  11578  fzo01  11604  fzo0to2pr  11606  fzo0to3tp  11607  injresinj  11631  flge0nn0  11658  btwnzge0  11665  zmodfz  11721  modid  11724  zmodid2  11728  ltweuz  11776  uzenom  11779  fzennn  11782  cardfz  11784  hashgf1o  11785  seqfn  11810  seq1  11811  seqp1  11813  exp0  11861  bcnn  12080  bcm1k  12083  bcval5  12086  bcpasc  12089  hashgadd  12132  hashge2el2dif  12176  hashbc  12198  fz1isolem  12206  brfi1uzind  12211  lswccat0lsw  12280  eqs1  12292  s111  12294  swrdlend  12317  swrd0  12319  wrdeqswrdlsw  12335  swrds1  12337  repswswrd  12414  cshw0  12423  s2f1o  12518  f1oun2prg  12519  rexfiuz  12827  climz  13019  climaddc1  13104  climmulc2  13106  climsubc1  13107  climsubc2  13108  climlec2  13128  sumss  13193  binomlem  13284  binom  13285  bcxmas  13290  climcndslem1  13304  arisum2  13315  explecnv  13319  geomulcvg  13328  ef0lem  13356  efcvgfsum  13363  ege2le3  13367  eftlub  13385  efgt1p2  13390  efgt1p  13391  ruclem4  13508  ruclem6  13509  nthruc  13525  dvds0  13540  0dvds  13545  fsumdvds  13568  odd2np1lem  13583  divalglem6  13594  divalglem7  13595  divalglem8  13596  bitsfzo  13623  bitsmod  13624  0bits  13627  m1bits  13628  sadc0  13642  smup0  13667  gcd0val  13685  gcddvds  13691  gcd0id  13699  gcdid0  13700  gcdaddm  13705  gcdid  13707  bezoutlem1  13714  bezout  13718  dfphi2  13841  phiprmpw  13843  prmdiveq  13853  prmdivdiv  13854  pc0  13913  pcdvdstr  13934  pcfaclem  13952  prmreclem2  13970  prmreclem4  13972  zgz  13986  igz  13987  4sqlem19  14016  vdwap0  14029  ramz  14078  1259lem1  14147  1259lem4  14150  2503lem2  14154  4001lem1  14157  4001lem3  14159  gsumws1  15508  mulg0  15623  dfod2  16056  zaddablx  16341  0cyg  16360  srgbinomlem4  16631  srgbinom  16633  psrbaglefi  17421  psrbaglefiOLD  17422  ltbwe  17534  zring0  17873  zrng0  17879  zndvds0  17963  iscmet3lem3  20781  vitalilem1  21068  iblcnlem1  21245  itgcnlem  21247  dvn0  21378  dvexp3  21430  plyco  21689  0dgr  21693  0dgrb  21694  coefv0  21695  coemulc  21702  vieta1lem2  21757  vieta1  21758  elqaalem1  21765  elqaalem3  21767  aareccl  21772  aannenlem1  21774  aannenlem2  21775  aalioulem1  21778  taylfval  21804  taylplem1  21808  taylplem2  21809  taylpfval  21810  dvtaylp  21815  dvradcnv  21866  pserulm  21867  pserdvlem2  21873  abelthlem6  21881  abelthlem9  21885  logf1o2  22075  advlogexp  22080  ang180lem3  22187  1cubr  22217  leibpi  22317  log2ublem3  22323  fsumharmonic  22385  wilthlem1  22386  muf  22458  0sgm  22462  1sgmprm  22518  ppiub  22523  bposlem1  22603  bposlem2  22604  lgslem2  22616  lgsfcl2  22621  lgsval2lem  22625  lgs0  22628  lgsdir2lem3  22644  lgsdirnn0  22658  lgsdinn0  22659  pntrlog2bndlem4  22809  padicabv  22859  ostth2lem2  22863  usgraexvlem  23281  usgraexmpldifpr  23286  usgraexmpl  23287  2trllemD  23424  2trllemG  23425  wlkntrllem2  23427  wlkntrl  23429  0pth  23437  0spth  23438  constr1trl  23455  constr2spthlem1  23461  usgrcyclnl1  23494  usgrcyclnl2  23495  3v3e3cycl1  23498  constr3lem4  23501  constr3trllem3  23506  constr3trllem5  23508  4cycl4v4e  23520  4cycl4dv4e  23522  eupa0  23563  eupares  23564  gx0  23716  zaddsubgo  23809  zringnm  26357  zzsnmOLD  26359  cnzh  26368  qqh0  26382  qqhcn  26389  qqhucn  26390  eulerpartlemmf  26727  ballotlem2  26840  ballotlemfc0  26844  ballotlemfcc  26845  ballotlemodife  26849  plymulx0  26917  signstf0  26938  signsvf0  26950  subfacval2  27044  cvmliftlem4  27146  cvmliftlem5  27147  relexp0  27300  fz0n  27358  4bc2eq6  27360  risefall0lem  27498  binomfallfac  27513  bpoly1  28163  bpolydiflem  28166  bpoly2  28169  bpoly3  28170  bpoly4  28171  sdclem1  28610  heibor1lem  28679  heiborlem4  28684  mzpnegmpt  29051  diophrw  29068  vdioph  29089  diophren  29123  irrapxlem1  29134  rmxy0  29235  monotoddzzfi  29254  zindbi  29258  rmyeq0  29267  jm2.18  29308  jm2.15nn0  29323  jm2.16nn0  29324  mpaaeu  29478  stoweidlem11  29777  stoweidlem17  29783  stoweidlem26  29792  stoweidlem34  29800  stirlinglem7  29846  f13idfv  30119  2ffzoeq  30185  elfzonlteqm1  30196  wlkv0  30262  altgsumbcALT  30719  bj-flbi3  32427
  Copyright terms: Public domain W3C validator