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

Theorem 0z 10977
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 9669 . 2  |-  0  e.  RR
2 eqid 2462 . . 3  |-  0  =  0
323mix1i 1186 . 2  |-  ( 0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN )
4 elz 10968 . 2  |-  ( 0  e.  ZZ  <->  ( 0  e.  RR  /\  (
0  =  0  \/  0  e.  NN  \/  -u 0  e.  NN ) ) )
51, 3, 4mpbir2an 936 1  |-  0  e.  ZZ
Colors of variables: wff setvar class
Syntax hints:    \/ w3o 990    = wceq 1455    e. wcel 1898   RRcr 9564   0cc0 9565   -ucneg 9887   NNcn 10637   ZZcz 10966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-i2m1 9633  ax-1ne0 9634  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-iota 5565  df-fv 5609  df-ov 6318  df-neg 9889  df-z 10967
This theorem is referenced by:  0zd  10978  elnn0z  10979  nn0ssz  10987  znegcl  11001  zgt0ge1  11019  nn0lt10bOLD  11028  nnm1ge0  11033  gtndiv  11042  zeo  11050  nn0ind  11059  fnn0ind  11063  eluzadd  11216  eluzsub  11217  nn0uz  11222  1eluzge0  11231  2eluzge0OLD  11233  nn0inf  11270  nn0infmOLD  11272  eqreznegel  11278  fz10  11849  fz01en  11856  fzshftral  11911  fznn0  11915  fz0tp  11922  fz0to3un2pr  11923  elfz0ubfz0  11924  1fv  11939  fzo0n  11971  lbfzo0  11986  elfzonlteqm1  12020  fzo01  12026  fzo0to2pr  12029  fzo0to3tp  12030  ico01fl0  12085  flge0nn0  12086  btwnzge0  12093  zmodfz  12150  modid  12153  zmodid2  12157  ltweuz  12207  uzenom  12210  fzennn  12213  cardfz  12215  hashgf1o  12216  f13idfv  12244  seqfn  12257  seq1  12258  seqp1  12260  exp0  12308  bcnn  12529  bcm1k  12532  bcval5  12535  bcpasc  12538  4bc2eq6  12546  hashgadd  12588  hashbc  12649  fz1isolem  12657  hashge2el2dif  12670  fi1uzind  12683  s111  12789  swrdnd  12825  swrds1  12844  repswswrd  12924  cshw0  12933  s2f1o  13047  f1oun2prg  13048  rexfiuz  13459  climz  13662  climaddc1  13747  climmulc2  13749  climsubc1  13750  climsubc2  13751  climlec2  13771  sumss  13839  binomlem  13936  binom  13937  bcxmas  13942  climcndslem1  13956  arisum2  13968  explecnv  13972  geomulcvg  13981  risefall0lem  14128  binomfallfac  14143  bpoly1  14153  bpolydiflem  14156  bpoly2  14159  bpoly3  14160  bpoly4  14161  ef0lem  14182  efcvgfsum  14189  ege2le3  14193  eftlub  14212  efgt1p2  14217  efgt1p  14218  ruclem4  14335  ruclem6  14336  nthruc  14352  dvds0  14367  0dvds  14372  fsumdvds  14397  odd2np1lem  14413  divalglem6  14427  divalglem7  14428  divalglem8  14429  bitsfzo  14458  bitsmod  14459  0bits  14462  m1bits  14463  sadc0  14477  smup0  14502  gcd0val  14520  gcddvds  14526  gcd0id  14536  gcdid0  14537  gcdaddm  14542  gcdid  14544  bezoutlem1  14552  bezout  14559  lcm0val  14607  dvdslcm  14612  lcmeq0  14614  lcmgcd  14621  lcmdvds  14622  lcmftp  14658  lcmfunsnlem2  14662  dfphi2  14771  phiprmpw  14773  prmdiveq  14783  prmdivdiv  14784  pc0  14853  pcdvdstr  14874  pcfaclem  14892  prmreclem2  14910  prmreclem4  14912  zgz  14926  igz  14927  4sqlem19  14962  vdwap0  14975  ramz  15032  1259lem1  15151  1259lem4  15154  2503lem2  15158  4001lem1  15161  4001lem3  15163  gsumws1  16672  mulg0  16812  dfod2  17264  zaddablx  17557  0cyg  17576  srgbinomlem4  17825  srgbinom  17827  psrbaglefi  18645  ltbwe  18745  zring0  19098  zndvds0  19170  pmatcollpw3fi1lem1  19859  pmatcollpw3fi1  19861  iscmet3lem3  22309  vitalilem1  22615  iblcnlem1  22794  itgcnlem  22796  dvn0  22927  dvexp3  22979  plyco  23244  0dgr  23248  0dgrb  23249  coefv0  23251  coemulc  23258  vieta1lem2  23313  vieta1  23314  elqaalem1  23321  elqaalem3  23323  elqaalem1OLD  23324  elqaalem3OLD  23326  aareccl  23331  aannenlem1  23333  aannenlem2  23334  aalioulem1  23337  taylfval  23363  taylplem1  23367  taylplem2  23368  taylpfval  23369  dvtaylp  23374  dvradcnv  23425  pserulm  23426  pserdvlem2  23432  abelthlem6  23440  abelthlem9  23444  logf1o2  23644  advlogexp  23649  ang180lem3  23789  1cubr  23817  leibpi  23917  log2ublem3  23923  fsumharmonic  23986  wilthlem1  24042  muf  24116  0sgm  24120  1sgmprm  24176  ppiub  24181  bposlem1  24261  bposlem2  24262  lgslem2  24274  lgsfcl2  24279  lgsval2lem  24283  lgs0  24286  lgsdir2lem3  24302  lgsdirnn0  24316  lgsdinn0  24317  pntrlog2bndlem4  24467  padicabv  24517  ostth2lem2  24521  usgraexmplvtxlem  25171  usgraexmpldifpr  25176  usgraexmplef  25177  2trllemD  25336  2trllemG  25337  wlkntrllem2  25339  wlkntrl  25341  0pth  25349  0spth  25350  constr1trl  25367  constr2spthlem1  25373  usgrcyclnl1  25417  3v3e3cycl1  25421  constr3lem4  25424  constr3trllem3  25429  constr3trllem5  25431  wlkv0  25537  eupa0  25751  eupares  25752  gx0  26038  zaddsubgo  26131  zringnm  28813  qqh0  28837  qqhcn  28844  qqhucn  28845  rrh0  28868  eulerpartlemmf  29257  ballotlem2  29370  ballotlemfc0  29374  ballotlemfcc  29375  ballotlemodife  29379  plymulx0  29485  signstf0  29506  signsvf0  29518  subfacval2  29959  cvmliftlem4  30060  cvmliftlem5  30061  fz0n  30413  bcneg1  30421  bccolsum  30424  fwddifn0  30980  fwddifnp1  30981  poimirlem24  32009  poimirlem27  32012  poimirlem28  32013  sdclem1  32117  heibor1lem  32186  heiborlem4  32191  mzpnegmpt  35631  diophrw  35646  vdioph  35667  diophren  35701  irrapxlem1  35711  rmxy0  35816  monotoddzzfi  35835  zindbi  35839  rmyeq0  35848  jm2.18  35888  jm2.15nn0  35903  jm2.16nn0  35904  mpaaeu  36061  nzss  36710  hashnzfz2  36714  dvradcnv2  36740  binomcxplemnn0  36742  binomcxplemrat  36743  binomcxplemnotnn0  36749  halffl  37551  fz1ssfz0  37566  dvnmul  37856  stoweidlem11  37909  stoweidlem17  37915  stoweidlem26  37924  stoweidlem34  37933  stirlinglem7  37980  fourierdlem20  38027  etransclem25  38162  etransclem26  38163  etransclem37  38174  0evenALTV  38855  0noddALTV  38856  2ffzoeq  39106  sPthisPth  39760  uhgr1wlkspthlem2  39786  pthdlem2  39794  0ewlk  39828  1wlkv0  39830  is01wlklem  39833  0pth-av  39841  0spth-av  39842  1wlk2v2elem2  39871  ntrl2v2e  39873  1odd  40084  0even  40204  2zrngamgm  40212  altgsumbcALT  40407  blen1  40668  blen1b  40672  0dig1  40693  0dig2pr01  40694  nn0sumshdiglem1  40705  aacllem  40813
  Copyright terms: Public domain W3C validator