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

Theorem 0z 10864
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 9585 . 2  |-  0  e.  RR
2 eqid 2460 . . 3  |-  0  =  0
323mix1i 1163 . 2  |-  ( 0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN )
4 elz 10855 . 2  |-  ( 0  e.  ZZ  <->  ( 0  e.  RR  /\  (
0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN ) ) )
51, 3, 4mpbir2an 913 1  |-  0  e.  ZZ
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 967    = wceq 1374    e. wcel 1762   RRcr 9480   0cc0 9481   -ucneg 9795   NNcn 10525   ZZcz 10853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278  df-neg 9797  df-z 10854
This theorem is referenced by:  0zd  10865  elnn0z  10866  nn0ssz  10874  znegcl  10887  zgt0ge1  10905  nn0lt10b  10913  nnm1ge0  10918  recnz  10925  gtndiv  10927  zeo  10935  nn0ind  10946  fnn0ind  10949  eluzadd  11099  eluzsub  11100  nn0uz  11105  1eluzge0  11114  2eluzge0  11115  nn0infm  11152  eqreznegel  11156  fz10  11695  fz01en  11702  fzshftral  11754  fznn0  11758  fz0tp  11764  elfz0ubfz0  11765  1fv  11778  lbfzo0  11819  elfzonlteqm1  11848  fzo01  11854  fzo0to2pr  11856  fzo0to3tp  11857  injresinj  11883  flge0nn0  11910  btwnzge0  11917  zmodfz  11973  modid  11976  zmodid2  11980  ltweuz  12028  uzenom  12031  fzennn  12034  cardfz  12036  hashgf1o  12037  f13idfv  12062  seqfn  12075  seq1  12076  seqp1  12078  exp0  12126  bcnn  12345  bcm1k  12348  bcval5  12351  bcpasc  12354  hashgadd  12400  hashbc  12455  fz1isolem  12463  hashge2el2dif  12474  brfi1uzind  12485  lswccat0lsw  12559  eqs1  12571  s111  12573  swrdlend  12606  swrd0  12608  wrdeqswrdlsw  12624  swrds1  12626  repswswrd  12706  cshw0  12715  s2f1o  12814  f1oun2prg  12815  rexfiuz  13129  climz  13321  climaddc1  13406  climmulc2  13408  climsubc1  13409  climsubc2  13410  climlec2  13430  sumss  13495  binomlem  13593  binom  13594  bcxmas  13599  climcndslem1  13613  arisum2  13624  explecnv  13628  geomulcvg  13637  ef0lem  13665  efcvgfsum  13672  ege2le3  13676  eftlub  13694  efgt1p2  13699  efgt1p  13700  ruclem4  13817  ruclem6  13818  nthruc  13834  dvds0  13849  0dvds  13854  fsumdvds  13877  odd2np1lem  13893  divalglem6  13904  divalglem7  13905  divalglem8  13906  bitsfzo  13933  bitsmod  13934  0bits  13937  m1bits  13938  sadc0  13952  smup0  13977  gcd0val  13995  gcddvds  14001  gcd0id  14009  gcdid0  14010  gcdaddm  14015  gcdid  14017  bezoutlem1  14024  bezout  14028  dfphi2  14152  phiprmpw  14154  prmdiveq  14164  prmdivdiv  14165  pc0  14226  pcdvdstr  14247  pcfaclem  14265  prmreclem2  14283  prmreclem4  14285  zgz  14299  igz  14300  4sqlem19  14329  vdwap0  14342  ramz  14391  1259lem1  14460  1259lem4  14463  2503lem2  14467  4001lem1  14470  4001lem3  14472  gsumws1  15823  mulg0  15940  dfod2  16375  zaddablx  16660  0cyg  16679  srgbinomlem4  16975  srgbinom  16977  psrbaglefi  17787  psrbaglefiOLD  17788  ltbwe  17901  zring0  18259  zrng0  18265  zndvds0  18349  pmatcollpw3fi1lem1  19047  pmatcollpw3fi1  19049  iscmet3lem3  21457  vitalilem1  21745  iblcnlem1  21922  itgcnlem  21924  dvn0  22055  dvexp3  22107  plyco  22366  0dgr  22370  0dgrb  22371  coefv0  22372  coemulc  22379  vieta1lem2  22434  vieta1  22435  elqaalem1  22442  elqaalem3  22444  aareccl  22449  aannenlem1  22451  aannenlem2  22452  aalioulem1  22455  taylfval  22481  taylplem1  22485  taylplem2  22486  taylpfval  22487  dvtaylp  22492  dvradcnv  22543  pserulm  22544  pserdvlem2  22550  abelthlem6  22558  abelthlem9  22562  logf1o2  22752  advlogexp  22757  ang180lem3  22864  1cubr  22894  leibpi  22994  log2ublem3  23000  fsumharmonic  23062  wilthlem1  23063  muf  23135  0sgm  23139  1sgmprm  23195  ppiub  23200  bposlem1  23280  bposlem2  23281  lgslem2  23293  lgsfcl2  23298  lgsval2lem  23302  lgs0  23305  lgsdir2lem3  23321  lgsdirnn0  23335  lgsdinn0  23336  pntrlog2bndlem4  23486  padicabv  23536  ostth2lem2  23540  usgraexvlem  24057  usgraexmpldifpr  24062  usgraexmpl  24063  2trllemD  24221  2trllemG  24222  wlkntrllem2  24224  wlkntrl  24226  0pth  24234  0spth  24235  constr1trl  24252  constr2spthlem1  24258  usgrcyclnl1  24302  usgrcyclnl2  24303  3v3e3cycl1  24306  constr3lem4  24309  constr3trllem3  24314  constr3trllem5  24316  4cycl4v4e  24328  4cycl4dv4e  24330  wlkv0  24422  eupa0  24636  eupares  24637  gx0  24789  zaddsubgo  24882  zringnm  27426  zzsnmOLD  27428  cnzh  27437  qqh0  27451  qqhcn  27458  qqhucn  27459  eulerpartlemmf  27804  ballotlem2  27917  ballotlemfc0  27921  ballotlemfcc  27922  ballotlemodife  27926  plymulx0  27994  signstf0  28015  signsvf0  28027  subfacval2  28121  cvmliftlem4  28223  cvmliftlem5  28224  relexp0  28377  fz0n  28435  4bc2eq6  28437  risefall0lem  28575  binomfallfac  28590  bpoly1  29240  bpolydiflem  29243  bpoly2  29246  bpoly3  29247  bpoly4  29248  sdclem1  29690  heibor1lem  29759  heiborlem4  29764  mzpnegmpt  30131  diophrw  30147  vdioph  30168  diophren  30202  irrapxlem1  30213  rmxy0  30314  monotoddzzfi  30333  zindbi  30337  rmyeq0  30346  jm2.18  30387  jm2.15nn0  30402  jm2.16nn0  30403  mpaaeu  30557  halffl  30889  sinaover2ne0  31023  stoweidlem11  31130  stoweidlem17  31136  stoweidlem26  31145  stoweidlem34  31153  stirlinglem7  31199  fourierdlem11  31237  fourierdlem14  31240  fourierdlem15  31241  fourierdlem20  31246  fourierdlem24  31250  fourierdlem25  31251  fourierdlem36  31262  fourierdlem37  31263  fourierdlem48  31274  fourierdlem49  31275  fourierdlem50  31276  fourierdlem54  31280  fourierdlem69  31295  fourierdlem73  31299  fourierdlem79  31305  fourierdlem81  31307  fourierdlem92  31318  fourierdlem93  31319  fourierdlem111  31337  2ffzoeq  31629  altgsumbcALT  31881  bj-flbi3  33554
  Copyright terms: Public domain W3C validator