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

Theorem 0z 10285
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 9083 . 2  |-  0  e.  RR
2 eqid 2435 . . 3  |-  0  =  0
323mix1i 1129 . 2  |-  ( 0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN )
4 elz 10276 . 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 1652    e. wcel 1725   RRcr 8981   0cc0 8982   -ucneg 9284   NNcn 9992   ZZcz 10274
This theorem is referenced by:  elnn0z  10286  nn0ssz  10294  znegcl  10305  nn0lt10b  10328  recnz  10337  gtndiv  10339  zeo  10347  nn0ind  10358  fnn0ind  10361  eluzadd  10506  eluzsub  10507  nn0uz  10512  nn0infm  10549  eqreznegel  10553  fz10  11067  fz01en  11071  fz0tp  11095  fznn0  11105  fzctr  11109  1fv  11112  fzshftral  11126  lbfzo0  11162  fzosubel3  11171  fzo01  11174  fzo0to2pr  11176  fzo0to3tp  11177  injresinj  11192  flge0nn0  11217  btwnzge0  11222  zmodfz  11260  modid  11262  ltweuz  11293  uzenom  11296  fzennn  11299  cardfz  11301  hashgf1o  11302  seqfn  11327  seq1  11328  seqp1  11330  exp0  11378  bcnn  11595  bcm1k  11598  bcval5  11601  bcpasc  11604  hashgadd  11643  hashbc  11694  fz1isolem  11702  brfi1uzind  11707  eqs1  11753  s111  11754  swrds1  11779  s2f1o  11855  f1oun2prg  11856  fzomaxdiflem  12138  rexfiuz  12143  climz  12335  climaddc1  12420  climmulc2  12422  climsubc1  12423  climsubc2  12424  climlec2  12444  sumss  12510  fsumzcl  12521  binomlem  12600  binom  12601  bcxmas  12607  isumnn0nn  12614  climcndslem1  12621  climcnds  12623  harmonic  12630  arisum2  12632  explecnv  12636  geolim  12639  geolim2  12640  geomulcvg  12645  geoisum  12646  geoisumr  12647  mertenslem1  12653  mertenslem2  12654  mertens  12655  ef0lem  12673  eff  12676  efcvg  12679  efcvgfsum  12680  reefcl  12681  ege2le3  12684  efcj  12686  eftlub  12702  effsumlt  12704  efgt1p2  12707  efgt1p  12708  eflegeo  12714  eirrlem  12795  ruclem4  12825  ruclem6  12826  nthruc  12842  dvds0  12857  0dvds  12862  fsumdvds  12885  dvdsmod  12898  odd2np1lem  12899  divalglem6  12910  divalglem7  12911  divalglem8  12912  bitsfzolem  12938  bitsfzo  12939  bitsmod  12940  0bits  12943  m1bits  12944  bitsinv1lem  12945  sadcf  12957  sadc0  12958  sadadd3  12965  smupf  12982  smup0  12983  gcd0val  13001  gcddvds  13007  gcd0id  13015  gcdid0  13016  gcdaddm  13021  gcdid  13023  bezoutlem1  13030  bezout  13034  alginv  13058  algcvg  13059  algcvga  13062  algfx  13063  eucalgcvga  13069  eucalg  13070  dfphi2  13155  phiprmpw  13157  fermltl  13165  prmdiveq  13167  prmdivdiv  13168  iserodd  13201  pcpre1  13208  pc0  13220  pcdvdstr  13241  pcfaclem  13259  qexpz  13262  prmreclem2  13277  prmreclem4  13279  zgz  13293  igz  13294  4sqlem19  13323  vdwapun  13334  vdwap0  13336  ramz  13385  1259lem1  13442  1259lem4  13445  2503lem2  13449  4001lem1  13452  4001lem3  13454  gsumws1  14777  mulg0  14887  odf1  15190  dfod2  15192  zaddablx  15475  0cyg  15494  psrbaglefi  16429  ltbwe  16525  zndvds0  16823  iscmet3lem3  19235  vitalilem1  19492  iblcnlem1  19671  itgcnlem  19673  dvnff  19801  dvn0  19802  dvexp3  19854  evlslem1  19928  dgrcl  20144  dgrub  20145  dgrlb  20147  plyco  20152  0dgr  20156  0dgrb  20157  coefv0  20158  coemulc  20165  vieta1lem2  20220  vieta1  20221  elqaalem1  20228  elqaalem2  20229  elqaalem3  20230  aareccl  20235  aannenlem1  20237  aannenlem2  20238  aalioulem1  20241  geolim3  20248  taylfval  20267  tayl0  20270  taylplem1  20271  taylplem2  20272  taylpfval  20273  dvtaylp  20278  radcnvlem1  20321  radcnvlem3  20323  radcnv0  20324  radcnvlt2  20327  dvradcnv  20329  pserulm  20330  psercn2  20331  pserdvlem2  20336  pserdv2  20338  abelthlem4  20342  abelthlem5  20343  abelthlem6  20344  abelthlem7  20346  abelthlem8  20347  abelthlem9  20348  cosne0  20424  logf1o2  20533  advlogexp  20538  logtayl  20543  ang180lem3  20645  1cubr  20674  leibpi  20774  leibpisum  20775  log2cnv  20776  log2tlbnd  20777  log2ublem3  20780  fsumharmonic  20842  wilthlem1  20843  basellem3  20857  muf  20915  0sgm  20919  1sgmprm  20975  ppiub  20980  dchrptlem2  21041  bcmono  21053  bposlem1  21060  bposlem2  21061  lgslem2  21073  lgslem4  21075  lgsfcl2  21078  lgsval2lem  21082  lgs0  21085  lgsdir2lem3  21101  lgsne0  21109  lgsdirnn0  21115  lgsdinn0  21116  pntrlog2bndlem4  21266  padicabv  21316  ostth2lem2  21320  usgraexvlem  21406  usgraexmpldifpr  21411  usgraexmpl  21412  2trllemD  21549  2trllemG  21550  wlkntrllem2  21552  wlkntrl  21554  0pth  21562  0spth  21563  constr1trl  21580  constr2spthlem1  21586  usgrcyclnl1  21619  usgrcyclnl2  21620  3v3e3cycl1  21623  constr3lem4  21626  constr3trllem3  21631  constr3trllem5  21633  4cycl4v4e  21645  4cycl4dv4e  21647  eupa0  21688  eupares  21689  gx0  21841  zaddsubgo  21934  zzs0  24259  zzsnm  24334  cnzh  24346  rezh  24347  qqh0  24360  qqhcn  24367  qqhucn  24368  ballotlem2  24738  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemfval0  24745  ballotlemodife  24747  subfacval2  24865  cvmliftlem4  24967  cvmliftlem5  24968  zmodid2  25106  relexp0  25121  fz0n  25194  4bc2eq6  25196  risefacval2  25318  fallfacval2  25319  risefall0lem  25334  binomfallfaclem2  25348  binomfallfac  25349  bpoly1  26089  bpolydiflem  26092  bpoly2  26095  bpoly3  26096  bpoly4  26097  itg2addnclem2  26247  sdclem1  26438  heibor1lem  26509  heiborlem4  26514  mzpnegmpt  26792  diophrw  26808  vdioph  26829  diophren  26865  irrapxlem1  26876  rmxy0  26977  monotoddzzfi  26996  zindbi  27000  rmyeq0  27009  rmynn  27012  jm2.24nn  27015  jm2.17c  27018  jm2.24  27019  acongrep  27036  acongeq  27039  dvdsabsmod0  27048  jm2.18  27050  jm2.23  27058  jm2.20nn  27059  jm2.15nn0  27065  jm2.16nn0  27066  jm2.27a  27067  jm2.27c  27069  rmydioph  27076  mpaaeu  27323  stoweidlem11  27727  stoweidlem17  27733  stoweidlem26  27742  stoweidlem34  27750  stirlinglem5  27794  stirlinglem7  27796  f13idfv  28068  1eluzge0  28085  2eluzge0  28086  elfzelfzelfz  28093  ubmelfzo  28109  ubmelm1fzo  28110  swrdltnd  28153  swrdccatin12lem3b  28175  swrdccat  28182  cshwoor  28203  cshwidx  28208
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-i2m1 9050  ax-1ne0 9051  ax-rnegex 9053  ax-rrecex 9054  ax-cnre 9055
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076  df-neg 9286  df-z 10275
  Copyright terms: Public domain W3C validator