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

Theorem 0z 10035
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 8838 . 2  |-  0  e.  RR
2 eqid 2283 . . 3  |-  0  =  0
323mix1i 1127 . 2  |-  ( 0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN )
4 elz 10026 . 2  |-  ( 0  e.  ZZ  <->  ( 0  e.  RR  /\  (
0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN ) ) )
51, 3, 4mpbir2an 886 1  |-  0  e.  ZZ
Colors of variables: wff set class
Syntax hints:    \/ w3o 933    = wceq 1623    e. wcel 1684   RRcr 8736   0cc0 8737   -ucneg 9038   NNcn 9746   ZZcz 10024
This theorem is referenced by:  elnn0z  10036  nn0ssz  10044  znegcl  10055  nn0lt10b  10078  recnz  10087  gtndiv  10089  zeo  10097  nn0ind  10108  fnn0ind  10111  eluzadd  10256  eluzsub  10257  nn0uz  10262  nn0infm  10299  eqreznegel  10303  fz10  10814  fz01en  10818  fznn0  10851  fzctr  10854  fzshftral  10869  lbfzo0  10903  fzosubel3  10910  fzo01  10913  flge0nn0  10948  btwnzge0  10953  zmodfz  10991  modid  10993  ltweuz  11024  uzenom  11027  fzennn  11030  cardfz  11032  hashgf1o  11033  seqfn  11058  seq1  11059  seqp1  11061  exp0  11108  bcnn  11324  bcm1k  11327  bcval5  11330  bcpasc  11333  hashgadd  11359  hashbc  11391  fz1isolem  11399  eqs1  11447  s111  11448  swrds1  11473  fzomaxdiflem  11826  rexfiuz  11831  climz  12023  climaddc1  12108  climmulc2  12110  climsubc1  12111  climsubc2  12112  climlec2  12132  sumss  12197  fsumzcl  12208  binomlem  12287  binom  12288  bcxmas  12294  isumnn0nn  12301  climcndslem1  12308  climcnds  12310  harmonic  12317  arisum2  12319  explecnv  12323  geolim  12326  geolim2  12327  geomulcvg  12332  geoisum  12333  geoisumr  12334  mertenslem1  12340  mertenslem2  12341  mertens  12342  ef0lem  12360  eff  12363  efcvg  12366  efcvgfsum  12367  reefcl  12368  ege2le3  12371  efcj  12373  eftlub  12389  effsumlt  12391  efgt1p2  12394  efgt1p  12395  eflegeo  12401  eirrlem  12482  ruclem4  12512  ruclem6  12513  nthruc  12529  dvds0  12544  0dvds  12549  fsumdvds  12572  dvdsmod  12585  odd2np1lem  12586  divalglem6  12597  divalglem7  12598  divalglem8  12599  bitsfzolem  12625  bitsfzo  12626  bitsmod  12627  0bits  12630  m1bits  12631  bitsinv1lem  12632  sadcf  12644  sadc0  12645  sadadd3  12652  smupf  12669  smup0  12670  gcd0val  12688  gcddvds  12694  gcd0id  12702  gcdid0  12703  gcdaddm  12708  gcdid  12710  bezoutlem1  12717  bezout  12721  alginv  12745  algcvg  12746  algcvga  12749  algfx  12750  eucalgcvga  12756  eucalg  12757  dfphi2  12842  phiprmpw  12844  fermltl  12852  prmdiveq  12854  prmdivdiv  12855  iserodd  12888  pcpre1  12895  pc0  12907  pcdvdstr  12928  pcfaclem  12946  qexpz  12949  prmreclem2  12964  prmreclem4  12966  zgz  12980  igz  12981  4sqlem19  13010  vdwapun  13021  vdwap0  13023  ramz  13072  1259lem1  13129  1259lem4  13132  2503lem2  13136  4001lem1  13139  4001lem3  13141  gsumws1  14462  mulg0  14572  odf1  14875  dfod2  14877  zaddablx  15160  0cyg  15179  psrbaglefi  16118  ltbwe  16214  zndvds0  16504  iscmet3lem3  18716  vitalilem1  18963  iblcnlem1  19142  itgcnlem  19144  dvnff  19272  dvn0  19273  dvexp3  19325  evlslem1  19399  dgrcl  19615  dgrub  19616  dgrlb  19618  plyco  19623  0dgr  19627  0dgrb  19628  coefv0  19629  coemulc  19636  vieta1lem2  19691  vieta1  19692  elqaalem1  19699  elqaalem2  19700  elqaalem3  19701  aareccl  19706  aannenlem1  19708  aannenlem2  19709  aalioulem1  19712  geolim3  19719  taylfval  19738  tayl0  19741  taylplem1  19742  taylplem2  19743  taylpfval  19744  dvtaylp  19749  radcnvlem1  19789  radcnvlem3  19791  radcnv0  19792  radcnvlt2  19795  dvradcnv  19797  pserulm  19798  psercn2  19799  pserdvlem2  19804  pserdv2  19806  abelthlem4  19810  abelthlem5  19811  abelthlem6  19812  abelthlem7  19814  abelthlem8  19815  abelthlem9  19816  cosne0  19892  logf1o2  19997  advlogexp  20002  logtayl  20007  ang180lem3  20109  1cubr  20138  leibpi  20238  leibpisum  20239  log2cnv  20240  log2tlbnd  20241  log2ublem3  20244  fsumharmonic  20305  wilthlem1  20306  basellem3  20320  muf  20378  0sgm  20382  1sgmprm  20438  ppiub  20443  dchrptlem2  20504  bcmono  20516  bposlem1  20523  bposlem2  20524  lgslem2  20536  lgslem4  20538  lgsfcl2  20541  lgsval2lem  20545  lgs0  20548  lgsdir2lem3  20564  lgsne0  20572  lgsdirnn0  20578  lgsdinn0  20579  pntrlog2bndlem4  20729  padicabv  20779  ostth2lem2  20783  gx0  20928  zaddsubgo  21021  ballotlem2  23047  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemfval0  23054  ballotlemodife  23056  subfacval2  23718  cvmliftlem4  23819  cvmliftlem5  23820  eupa0  23898  eupares  23899  zmodid2  24010  relexp0  24025  fz0n  24097  4bc2eq6  24099  bpoly0  24785  bpoly1  24786  bpolydiflem  24789  bpoly2  24792  bpoly3  24793  bpoly4  24794  sdclem1  26453  heibor1lem  26533  heiborlem4  26538  mzpnegmpt  26822  diophrw  26838  vdioph  26859  diophren  26896  irrapxlem1  26907  rmxy0  27008  monotoddzzfi  27027  zindbi  27031  rmyeq0  27040  rmynn  27043  jm2.24nn  27046  jm2.17c  27049  jm2.24  27050  acongrep  27067  acongeq  27070  dvdsabsmod0  27079  jm2.18  27081  jm2.23  27089  jm2.20nn  27090  jm2.15nn0  27096  jm2.16nn0  27097  jm2.27a  27098  jm2.27c  27100  rmydioph  27107  mpaaeu  27355  stoweidlem11  27760  stoweidlem17  27766  stoweidlem26  27775  stoweidlem34  27783  stirlinglem5  27827  stirlinglem7  27829  f1oun2prg  28076  s2f1o  28091  usgraexvlem  28127  usgraexmpldifpr  28132  usgraexmpl  28133
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-i2m1 8805  ax-1ne0 8806  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-neg 9040  df-z 10025
  Copyright terms: Public domain W3C validator