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

Theorem 0z 10810
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 9525 . 2  |-  0  e.  RR
2 eqid 2392 . . 3  |-  0  =  0
323mix1i 1166 . 2  |-  ( 0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN )
4 elz 10801 . 2  |-  ( 0  e.  ZZ  <->  ( 0  e.  RR  /\  (
0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN ) ) )
51, 3, 4mpbir2an 918 1  |-  0  e.  ZZ
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 970    = wceq 1399    e. wcel 1836   RRcr 9420   0cc0 9421   -ucneg 9737   NNcn 10470   ZZcz 10799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-i2m1 9489  ax-1ne0 9490  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-iota 5473  df-fv 5517  df-ov 6217  df-neg 9739  df-z 10800
This theorem is referenced by:  0zd  10811  elnn0z  10812  nn0ssz  10820  znegcl  10834  zgt0ge1  10852  nn0lt10bOLD  10861  nnm1ge0  10866  gtndiv  10875  zeo  10883  nn0ind  10892  fnn0ind  10896  eluzadd  11047  eluzsub  11048  nn0uz  11053  1eluzge0  11062  2eluzge0OLD  11064  nn0infm  11100  eqreznegel  11104  fz10  11645  fz01en  11652  fzshftral  11706  fznn0  11710  fz0tp  11717  elfz0ubfz0  11718  1fv  11732  fzo0n  11760  lbfzo0  11775  elfzonlteqm1  11808  fzo01  11814  fzo0to2pr  11817  fzo0to3tp  11818  ico01fl0  11872  flge0nn0  11873  btwnzge0  11880  zmodfz  11937  modid  11940  zmodid2  11944  ltweuz  11994  uzenom  11997  fzennn  12000  cardfz  12002  hashgf1o  12003  f13idfv  12028  seqfn  12041  seq1  12042  seqp1  12044  exp0  12092  bcnn  12311  bcm1k  12314  bcval5  12317  bcpasc  12320  hashgadd  12367  hashbc  12425  fz1isolem  12433  hashge2el2dif  12444  brfi1uzind  12455  s111  12551  swrdnd  12587  swrds1  12606  repswswrd  12686  cshw0  12695  s2f1o  12794  f1oun2prg  12795  rexfiuz  13201  climz  13393  climaddc1  13478  climmulc2  13480  climsubc1  13481  climsubc2  13482  climlec2  13502  sumss  13567  binomlem  13662  binom  13663  bcxmas  13668  climcndslem1  13682  arisum2  13693  explecnv  13697  geomulcvg  13706  ef0lem  13835  efcvgfsum  13842  ege2le3  13846  eftlub  13865  efgt1p2  13870  efgt1p  13871  ruclem4  13988  ruclem6  13989  nthruc  14005  dvds0  14020  0dvds  14025  fsumdvds  14050  odd2np1lem  14066  divalglem6  14077  divalglem7  14078  divalglem8  14079  bitsfzo  14106  bitsmod  14107  0bits  14110  m1bits  14111  sadc0  14125  smup0  14150  gcd0val  14168  gcddvds  14174  gcd0id  14182  gcdid0  14183  gcdaddm  14188  gcdid  14190  bezoutlem1  14197  bezout  14201  dfphi2  14325  phiprmpw  14327  prmdiveq  14337  prmdivdiv  14338  pc0  14399  pcdvdstr  14420  pcfaclem  14438  prmreclem2  14456  prmreclem4  14458  zgz  14472  igz  14473  4sqlem19  14502  vdwap0  14515  ramz  14564  1259lem1  14634  1259lem4  14637  2503lem2  14641  4001lem1  14644  4001lem3  14646  gsumws1  16143  mulg0  16283  dfod2  16722  zaddablx  17012  0cyg  17031  srgbinomlem4  17326  srgbinom  17328  psrbaglefi  18155  psrbaglefiOLD  18156  ltbwe  18269  zring0  18630  zndvds0  18699  pmatcollpw3fi1lem1  19391  pmatcollpw3fi1  19393  iscmet3lem3  21833  vitalilem1  22121  iblcnlem1  22298  itgcnlem  22300  dvn0  22431  dvexp3  22483  plyco  22742  0dgr  22746  0dgrb  22747  coefv0  22749  coemulc  22756  vieta1lem2  22811  vieta1  22812  elqaalem1  22819  elqaalem3  22821  aareccl  22826  aannenlem1  22828  aannenlem2  22829  aalioulem1  22832  taylfval  22858  taylplem1  22862  taylplem2  22863  taylpfval  22864  dvtaylp  22869  dvradcnv  22920  pserulm  22921  pserdvlem2  22927  abelthlem6  22935  abelthlem9  22939  logf1o2  23137  advlogexp  23142  ang180lem3  23280  1cubr  23308  leibpi  23408  log2ublem3  23414  fsumharmonic  23477  wilthlem1  23478  muf  23550  0sgm  23554  1sgmprm  23610  ppiub  23615  bposlem1  23695  bposlem2  23696  lgslem2  23708  lgsfcl2  23713  lgsval2lem  23717  lgs0  23720  lgsdir2lem3  23736  lgsdirnn0  23750  lgsdinn0  23751  pntrlog2bndlem4  23901  padicabv  23951  ostth2lem2  23955  usgraexvlem  24537  usgraexmpldifpr  24542  usgraexmpl  24543  2trllemD  24701  2trllemG  24702  wlkntrllem2  24704  wlkntrl  24706  0pth  24714  0spth  24715  constr1trl  24732  constr2spthlem1  24738  usgrcyclnl1  24782  3v3e3cycl1  24786  constr3lem4  24789  constr3trllem3  24794  constr3trllem5  24796  wlkv0  24902  eupa0  25116  eupares  25117  gx0  25401  zaddsubgo  25494  zringnm  28125  qqh0  28149  qqhcn  28156  qqhucn  28157  eulerpartlemmf  28533  ballotlem2  28646  ballotlemfc0  28650  ballotlemfcc  28651  ballotlemodife  28655  plymulx0  28723  signstf0  28744  signsvf0  28756  subfacval2  28856  cvmliftlem4  28958  cvmliftlem5  28959  fz0n  29312  4bc2eq6  29314  risefall0lem  29350  binomfallfac  29365  bpoly1  30002  bpolydiflem  30005  bpoly2  30008  bpoly3  30009  bpoly4  30010  sdclem1  30438  heibor1lem  30507  heiborlem4  30512  mzpnegmpt  30878  diophrw  30893  vdioph  30914  diophren  30948  irrapxlem1  30959  rmxy0  31060  monotoddzzfi  31079  zindbi  31083  rmyeq0  31092  jm2.18  31132  jm2.15nn0  31147  jm2.16nn0  31148  mpaaeu  31303  lcm0val  31404  dvdslcm  31408  lcmeq0  31410  lcmgcd  31417  lcmdvds  31418  nzss  31426  hashnzfz2  31430  dvradcnv2  31456  binomcxplemnn0  31458  binomcxplemrat  31459  binomcxplemnotnn0  31465  halffl  31694  fz1ssfz0  31711  dvnmul  31941  stoweidlem11  31994  stoweidlem17  32000  stoweidlem26  32009  stoweidlem34  32017  stirlinglem7  32063  fourierdlem20  32110  etransclem25  32243  etransclem26  32244  etransclem37  32255  0evenALTV  32565  0noddALTV  32566  2ffzoeq  32696  1odd  32852  0even  32972  2zrngamgm  32980  altgsumbcALT  33177  blen1  33440  blen1b  33444  0dig1  33465  0dig2pr01  33466  nn0sumshdiglem1  33477  aacllem  33585
  Copyright terms: Public domain W3C validator