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

Theorem 0z 10051
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 8854 . 2  |-  0  e.  RR
2 eqid 2296 . . 3  |-  0  =  0
323mix1i 1127 . 2  |-  ( 0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN )
4 elz 10042 . 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 1632    e. wcel 1696   RRcr 8752   0cc0 8753   -ucneg 9054   NNcn 9762   ZZcz 10040
This theorem is referenced by:  elnn0z  10052  nn0ssz  10060  znegcl  10071  nn0lt10b  10094  recnz  10103  gtndiv  10105  zeo  10113  nn0ind  10124  fnn0ind  10127  eluzadd  10272  eluzsub  10273  nn0uz  10278  nn0infm  10315  eqreznegel  10319  fz10  10830  fz01en  10834  fznn0  10867  fzctr  10870  fzshftral  10885  lbfzo0  10919  fzosubel3  10926  fzo01  10929  flge0nn0  10964  btwnzge0  10969  zmodfz  11007  modid  11009  ltweuz  11040  uzenom  11043  fzennn  11046  cardfz  11048  hashgf1o  11049  seqfn  11074  seq1  11075  seqp1  11077  exp0  11124  bcnn  11340  bcm1k  11343  bcval5  11346  bcpasc  11349  hashgadd  11375  hashbc  11407  fz1isolem  11415  eqs1  11463  s111  11464  swrds1  11489  fzomaxdiflem  11842  rexfiuz  11847  climz  12039  climaddc1  12124  climmulc2  12126  climsubc1  12127  climsubc2  12128  climlec2  12148  sumss  12213  fsumzcl  12224  binomlem  12303  binom  12304  bcxmas  12310  isumnn0nn  12317  climcndslem1  12324  climcnds  12326  harmonic  12333  arisum2  12335  explecnv  12339  geolim  12342  geolim2  12343  geomulcvg  12348  geoisum  12349  geoisumr  12350  mertenslem1  12356  mertenslem2  12357  mertens  12358  ef0lem  12376  eff  12379  efcvg  12382  efcvgfsum  12383  reefcl  12384  ege2le3  12387  efcj  12389  eftlub  12405  effsumlt  12407  efgt1p2  12410  efgt1p  12411  eflegeo  12417  eirrlem  12498  ruclem4  12528  ruclem6  12529  nthruc  12545  dvds0  12560  0dvds  12565  fsumdvds  12588  dvdsmod  12601  odd2np1lem  12602  divalglem6  12613  divalglem7  12614  divalglem8  12615  bitsfzolem  12641  bitsfzo  12642  bitsmod  12643  0bits  12646  m1bits  12647  bitsinv1lem  12648  sadcf  12660  sadc0  12661  sadadd3  12668  smupf  12685  smup0  12686  gcd0val  12704  gcddvds  12710  gcd0id  12718  gcdid0  12719  gcdaddm  12724  gcdid  12726  bezoutlem1  12733  bezout  12737  alginv  12761  algcvg  12762  algcvga  12765  algfx  12766  eucalgcvga  12772  eucalg  12773  dfphi2  12858  phiprmpw  12860  fermltl  12868  prmdiveq  12870  prmdivdiv  12871  iserodd  12904  pcpre1  12911  pc0  12923  pcdvdstr  12944  pcfaclem  12962  qexpz  12965  prmreclem2  12980  prmreclem4  12982  zgz  12996  igz  12997  4sqlem19  13026  vdwapun  13037  vdwap0  13039  ramz  13088  1259lem1  13145  1259lem4  13148  2503lem2  13152  4001lem1  13155  4001lem3  13157  gsumws1  14478  mulg0  14588  odf1  14891  dfod2  14893  zaddablx  15176  0cyg  15195  psrbaglefi  16134  ltbwe  16230  zndvds0  16520  iscmet3lem3  18732  vitalilem1  18979  iblcnlem1  19158  itgcnlem  19160  dvnff  19288  dvn0  19289  dvexp3  19341  evlslem1  19415  dgrcl  19631  dgrub  19632  dgrlb  19634  plyco  19639  0dgr  19643  0dgrb  19644  coefv0  19645  coemulc  19652  vieta1lem2  19707  vieta1  19708  elqaalem1  19715  elqaalem2  19716  elqaalem3  19717  aareccl  19722  aannenlem1  19724  aannenlem2  19725  aalioulem1  19728  geolim3  19735  taylfval  19754  tayl0  19757  taylplem1  19758  taylplem2  19759  taylpfval  19760  dvtaylp  19765  radcnvlem1  19805  radcnvlem3  19807  radcnv0  19808  radcnvlt2  19811  dvradcnv  19813  pserulm  19814  psercn2  19815  pserdvlem2  19820  pserdv2  19822  abelthlem4  19826  abelthlem5  19827  abelthlem6  19828  abelthlem7  19830  abelthlem8  19831  abelthlem9  19832  cosne0  19908  logf1o2  20013  advlogexp  20018  logtayl  20023  ang180lem3  20125  1cubr  20154  leibpi  20254  leibpisum  20255  log2cnv  20256  log2tlbnd  20257  log2ublem3  20260  fsumharmonic  20321  wilthlem1  20322  basellem3  20336  muf  20394  0sgm  20398  1sgmprm  20454  ppiub  20459  dchrptlem2  20520  bcmono  20532  bposlem1  20539  bposlem2  20540  lgslem2  20552  lgslem4  20554  lgsfcl2  20557  lgsval2lem  20561  lgs0  20564  lgsdir2lem3  20580  lgsne0  20588  lgsdirnn0  20594  lgsdinn0  20595  pntrlog2bndlem4  20745  padicabv  20795  ostth2lem2  20799  gx0  20944  zaddsubgo  21037  ballotlem2  23063  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemfval0  23070  ballotlemodife  23072  subfacval2  23733  cvmliftlem4  23834  cvmliftlem5  23835  eupa0  23913  eupares  23914  zmodid2  24025  relexp0  24040  fz0n  24112  4bc2eq6  24114  bpoly0  24857  bpoly1  24858  bpolydiflem  24861  bpoly2  24864  bpoly3  24865  bpoly4  24866  itg2addnclem2  25004  sdclem1  26556  heibor1lem  26636  heiborlem4  26641  mzpnegmpt  26925  diophrw  26941  vdioph  26962  diophren  26999  irrapxlem1  27010  rmxy0  27111  monotoddzzfi  27130  zindbi  27134  rmyeq0  27143  rmynn  27146  jm2.24nn  27149  jm2.17c  27152  jm2.24  27153  acongrep  27170  acongeq  27173  dvdsabsmod0  27182  jm2.18  27184  jm2.23  27192  jm2.20nn  27193  jm2.15nn0  27199  jm2.16nn0  27200  jm2.27a  27201  jm2.27c  27203  rmydioph  27210  mpaaeu  27458  stoweidlem11  27863  stoweidlem17  27869  stoweidlem26  27878  stoweidlem34  27886  stirlinglem5  27930  stirlinglem7  27932  f1oun2prg  28187  fzo0to3tp  28210  fzo0to42pr  28211  injresinj  28215  s2f1o  28223  usgraexvlem  28261  usgraexmpldifpr  28266  usgraexmpl  28267  wlkntrllem1  28345  wlkntrllem3  28347  wlkntrllem4  28348  0pth  28356  0spth  28357  usgrcyclnl1  28386  usgrcyclnl2  28387  3v3e3cycl1  28390  constr3lem4  28393  constr3trllem3  28398  constr3trllem5  28400  4cycl4v4e  28412  4cycl4dv4e  28414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-i2m1 8821  ax-1ne0 8822  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826
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 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-neg 9056  df-z 10041
  Copyright terms: Public domain W3C validator