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

Theorem 0z 10226
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 9025 . 2  |-  0  e.  RR
2 eqid 2388 . . 3  |-  0  =  0
323mix1i 1129 . 2  |-  ( 0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN )
4 elz 10217 . 2  |-  ( 0  e.  ZZ  <->  ( 0  e.  RR  /\  (
0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN ) ) )
51, 3, 4mpbir2an 887 1  |-  0  e.  ZZ
Colors of variables: wff set class
Syntax hints:    \/ w3o 935    = wceq 1649    e. wcel 1717   RRcr 8923   0cc0 8924   -ucneg 9225   NNcn 9933   ZZcz 10215
This theorem is referenced by:  elnn0z  10227  nn0ssz  10235  znegcl  10246  nn0lt10b  10269  recnz  10278  gtndiv  10280  zeo  10288  nn0ind  10299  fnn0ind  10302  eluzadd  10447  eluzsub  10448  nn0uz  10453  nn0infm  10490  eqreznegel  10494  fz10  11008  fz01en  11012  fznn0  11045  fzctr  11048  1fv  11051  fzshftral  11065  lbfzo0  11101  fzosubel3  11108  fzo01  11111  fzo0to2pr  11112  fzo0to3tp  11113  injresinj  11128  flge0nn0  11153  btwnzge0  11158  zmodfz  11196  modid  11198  ltweuz  11229  uzenom  11232  fzennn  11235  cardfz  11237  hashgf1o  11238  seqfn  11263  seq1  11264  seqp1  11266  exp0  11314  bcnn  11531  bcm1k  11534  bcval5  11537  bcpasc  11540  hashgadd  11579  hashbc  11630  fz1isolem  11638  brfi1uzind  11643  eqs1  11689  s111  11690  swrds1  11715  s2f1o  11791  f1oun2prg  11792  fzomaxdiflem  12074  rexfiuz  12079  climz  12271  climaddc1  12356  climmulc2  12358  climsubc1  12359  climsubc2  12360  climlec2  12380  sumss  12446  fsumzcl  12457  binomlem  12536  binom  12537  bcxmas  12543  isumnn0nn  12550  climcndslem1  12557  climcnds  12559  harmonic  12566  arisum2  12568  explecnv  12572  geolim  12575  geolim2  12576  geomulcvg  12581  geoisum  12582  geoisumr  12583  mertenslem1  12589  mertenslem2  12590  mertens  12591  ef0lem  12609  eff  12612  efcvg  12615  efcvgfsum  12616  reefcl  12617  ege2le3  12620  efcj  12622  eftlub  12638  effsumlt  12640  efgt1p2  12643  efgt1p  12644  eflegeo  12650  eirrlem  12731  ruclem4  12761  ruclem6  12762  nthruc  12778  dvds0  12793  0dvds  12798  fsumdvds  12821  dvdsmod  12834  odd2np1lem  12835  divalglem6  12846  divalglem7  12847  divalglem8  12848  bitsfzolem  12874  bitsfzo  12875  bitsmod  12876  0bits  12879  m1bits  12880  bitsinv1lem  12881  sadcf  12893  sadc0  12894  sadadd3  12901  smupf  12918  smup0  12919  gcd0val  12937  gcddvds  12943  gcd0id  12951  gcdid0  12952  gcdaddm  12957  gcdid  12959  bezoutlem1  12966  bezout  12970  alginv  12994  algcvg  12995  algcvga  12998  algfx  12999  eucalgcvga  13005  eucalg  13006  dfphi2  13091  phiprmpw  13093  fermltl  13101  prmdiveq  13103  prmdivdiv  13104  iserodd  13137  pcpre1  13144  pc0  13156  pcdvdstr  13177  pcfaclem  13195  qexpz  13198  prmreclem2  13213  prmreclem4  13215  zgz  13229  igz  13230  4sqlem19  13259  vdwapun  13270  vdwap0  13272  ramz  13321  1259lem1  13378  1259lem4  13381  2503lem2  13385  4001lem1  13388  4001lem3  13390  gsumws1  14713  mulg0  14823  odf1  15126  dfod2  15128  zaddablx  15411  0cyg  15430  psrbaglefi  16365  ltbwe  16461  zndvds0  16755  iscmet3lem3  19115  vitalilem1  19368  iblcnlem1  19547  itgcnlem  19549  dvnff  19677  dvn0  19678  dvexp3  19730  evlslem1  19804  dgrcl  20020  dgrub  20021  dgrlb  20023  plyco  20028  0dgr  20032  0dgrb  20033  coefv0  20034  coemulc  20041  vieta1lem2  20096  vieta1  20097  elqaalem1  20104  elqaalem2  20105  elqaalem3  20106  aareccl  20111  aannenlem1  20113  aannenlem2  20114  aalioulem1  20117  geolim3  20124  taylfval  20143  tayl0  20146  taylplem1  20147  taylplem2  20148  taylpfval  20149  dvtaylp  20154  radcnvlem1  20197  radcnvlem3  20199  radcnv0  20200  radcnvlt2  20203  dvradcnv  20205  pserulm  20206  psercn2  20207  pserdvlem2  20212  pserdv2  20214  abelthlem4  20218  abelthlem5  20219  abelthlem6  20220  abelthlem7  20222  abelthlem8  20223  abelthlem9  20224  cosne0  20300  logf1o2  20409  advlogexp  20414  logtayl  20419  ang180lem3  20521  1cubr  20550  leibpi  20650  leibpisum  20651  log2cnv  20652  log2tlbnd  20653  log2ublem3  20656  fsumharmonic  20718  wilthlem1  20719  basellem3  20733  muf  20791  0sgm  20795  1sgmprm  20851  ppiub  20856  dchrptlem2  20917  bcmono  20929  bposlem1  20936  bposlem2  20937  lgslem2  20949  lgslem4  20951  lgsfcl2  20954  lgsval2lem  20958  lgs0  20961  lgsdir2lem3  20977  lgsne0  20985  lgsdirnn0  20991  lgsdinn0  20992  pntrlog2bndlem4  21142  padicabv  21192  ostth2lem2  21196  usgraexvlem  21281  usgraexmpldifpr  21286  usgraexmpl  21287  wlkntrllem3  21416  wlkntrllem4  21417  0pth  21425  0spth  21426  constr1trl  21437  2trllem4  21446  constr2trl  21447  2pthonlem2  21449  usgrcyclnl1  21476  usgrcyclnl2  21477  3v3e3cycl1  21480  constr3lem4  21483  constr3trllem3  21488  constr3trllem5  21490  4cycl4v4e  21502  4cycl4dv4e  21504  eupa0  21545  eupares  21546  gx0  21698  zaddsubgo  21791  zzs0  24084  zzsnm  24145  qqh0  24168  qqhcn  24175  qqhucn  24176  rrhre  24184  ballotlem2  24526  ballotlemfc0  24530  ballotlemfcc  24531  ballotlemfval0  24533  ballotlemodife  24535  subfacval2  24653  cvmliftlem4  24755  cvmliftlem5  24756  zmodid2  24894  relexp0  24909  fz0n  24982  4bc2eq6  24984  risefacval2  25096  fallfacval2  25097  risefall0lem  25111  fallfacfac  25119  bpoly1  25812  bpolydiflem  25815  bpoly2  25818  bpoly3  25819  bpoly4  25820  itg2addnclem2  25959  sdclem1  26139  heibor1lem  26210  heiborlem4  26215  mzpnegmpt  26493  diophrw  26509  vdioph  26530  diophren  26566  irrapxlem1  26577  rmxy0  26678  monotoddzzfi  26697  zindbi  26701  rmyeq0  26710  rmynn  26713  jm2.24nn  26716  jm2.17c  26719  jm2.24  26720  acongrep  26737  acongeq  26740  dvdsabsmod0  26749  jm2.18  26751  jm2.23  26759  jm2.20nn  26760  jm2.15nn0  26766  jm2.16nn0  26767  jm2.27a  26768  jm2.27c  26770  rmydioph  26777  mpaaeu  27025  stoweidlem11  27429  stoweidlem17  27435  stoweidlem26  27444  stoweidlem34  27452  stirlinglem5  27496  stirlinglem7  27498
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-1cn 8982  ax-icn 8983  ax-addcl 8984  ax-addrcl 8985  ax-mulcl 8986  ax-mulrcl 8987  ax-i2m1 8992  ax-1ne0 8993  ax-rnegex 8995  ax-rrecex 8996  ax-cnre 8997
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-iota 5359  df-fv 5403  df-ov 6024  df-neg 9227  df-z 10216
  Copyright terms: Public domain W3C validator