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

Theorem 0z 11218
Description: Zero is an integer. (Contributed by NM, 12-Jan-2002.)
Assertion
Ref Expression
0z 0 ∈ ℤ

Proof of Theorem 0z
StepHypRef Expression
1 0re 9893 . 2 0 ∈ ℝ
2 eqid 2606 . . 3 0 = 0
323mix1i 1225 . 2 (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4 elz 11209 . 2 (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
51, 3, 4mpbir2an 956 1 0 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  w3o 1029   = wceq 1474  wcel 1976  cr 9788  0cc0 9789  -cneg 10115  cn 10864  cz 11207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-i2m1 9857  ax-1ne0 9858  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-iota 5751  df-fv 5795  df-ov 6527  df-neg 10117  df-z 11208
This theorem is referenced by:  0zd  11219  elnn0z  11220  nn0ssz  11228  znegcl  11242  zgt0ge1  11261  nnm1ge0  11274  gtndiv  11283  zeo  11292  nn0ind  11301  fnn0ind  11305  eluzadd  11545  eluzsub  11546  nn0uz  11551  1eluzge0  11561  nn0inf  11599  eqreznegel  11603  fz10  12185  fz01en  12192  fzshftral  12249  fznn0  12253  fz0sn  12260  fz0tp  12261  fz0to3un2pr  12262  fz0to4untppr  12263  elfz0ubfz0  12264  fz0sn0fz1  12277  1fv  12279  fzo0n  12311  lbfzo0  12327  elfzonlteqm1  12362  fzo01  12369  fzo0to2pr  12372  fzo0to3tp  12373  ico01fl0  12434  flge0nn0  12435  divfl0  12439  btwnzge0  12443  zmodfz  12506  modid  12509  zmodid2  12512  modmuladdnn0  12528  ltweuz  12574  uzenom  12577  fzennn  12581  cardfz  12583  hashgf1o  12584  f13idfv  12614  seqfn  12627  seq1  12628  seqp1  12630  exp0  12678  bcnn  12913  bcm1k  12916  bcval5  12919  bcpasc  12922  4bc2eq6  12930  hashgadd  12976  hashbc  13043  fz1isolem  13051  hashge2el2dif  13064  fi1uzind  13077  fi1uzindOLD  13083  s111  13191  swrdnd  13227  swrds1  13246  repswswrd  13325  cshw0  13334  s2f1o  13454  f1oun2prg  13455  rexfiuz  13878  climz  14071  climaddc1  14156  climmulc2  14158  climsubc1  14159  climsubc2  14160  climlec2  14180  sumss  14245  binomlem  14343  binom  14344  bcxmas  14349  climcndslem1  14363  arisum2  14375  explecnv  14379  geomulcvg  14389  risefall0lem  14539  binomfallfac  14554  bpoly1  14564  bpolydiflem  14567  bpoly2  14570  bpoly3  14571  bpoly4  14572  ef0lem  14591  efcvgfsum  14598  ege2le3  14602  eftlub  14621  efgt1p2  14626  efgt1p  14627  ruclem4  14745  ruclem6  14746  nthruc  14762  dvds0  14778  0dvds  14783  fsumdvds  14811  odd2np1lem  14845  divalglem6  14902  divalglem7  14903  divalglem8  14904  bitsfzo  14938  bitsmod  14939  0bits  14942  m1bits  14943  sadc0  14957  smup0  14982  gcd0val  15000  gcddvds  15006  gcd0id  15021  gcdid0  15022  gcdaddm  15027  gcdid  15029  bezoutlem1  15037  bezout  15041  dfgcd2  15044  lcm0val  15088  dvdslcm  15092  lcmeq0  15094  lcmgcd  15101  lcmdvds  15102  lcmftp  15130  lcmfunsnlem2  15134  dfphi2  15260  phiprmpw  15262  prmdiveq  15272  prmdivdiv  15273  pc0  15340  pcdvdstr  15361  dvdsprmpweqnn  15370  pcfaclem  15383  prmreclem2  15402  prmreclem4  15404  zgz  15418  igz  15419  4sqlem19  15448  vdwap0  15461  ramz  15510  1259lem1  15619  1259lem4  15622  2503lem2  15626  4001lem1  15629  4001lem3  15631  gsumws1  17142  mulg0  17312  dfod2  17747  zaddablx  18041  0cyg  18060  srgbinomlem4  18309  srgbinom  18311  ltbwe  19236  zring0  19590  zndvds0  19660  pmatcollpw3fi1lem1  20349  pmatcollpw3fi1  20351  iscmet3lem3  22811  vitalilem1  23096  vitalilem1OLD  23097  iblcnlem1  23274  itgcnlem  23276  dvn0  23407  dvexp3  23459  plyco  23715  0dgr  23719  0dgrb  23720  coefv0  23722  coemulc  23729  vieta1lem2  23784  vieta1  23785  elqaalem1  23792  elqaalem3  23794  aareccl  23799  aannenlem1  23801  aannenlem2  23802  aalioulem1  23805  taylfval  23831  taylplem1  23835  taylplem2  23836  taylpfval  23837  dvtaylp  23842  dvradcnv  23893  pserulm  23894  pserdvlem2  23900  abelthlem6  23908  abelthlem9  23912  logf1o2  24110  advlogexp  24115  ang180lem3  24255  1cubr  24283  leibpi  24383  fsumharmonic  24452  wilthlem1  24508  muf  24580  0sgm  24584  1sgmprm  24638  ppiub  24643  bposlem1  24723  bposlem2  24724  lgslem2  24737  lgsfcl2  24742  lgsval2lem  24746  lgs0  24749  lgsdir2lem3  24766  lgsdirnn0  24783  lgsdinn0  24784  pntrlog2bndlem4  24983  padicabv  25033  ostth2lem2  25037  usgraexmpldifpr  25691  usgraexmplef  25692  2trllemD  25850  2trllemG  25851  wlkntrllem2  25853  wlkntrl  25855  0pth  25863  0spth  25864  constr1trl  25881  constr2spthlem1  25887  usgrcyclnl1  25931  3v3e3cycl1  25935  constr3lem4  25938  constr3trllem3  25943  constr3trllem5  25945  wlkv0  26051  eupa0  26264  eupares  26265  zringnm  29135  qqh0  29159  qqhcn  29166  qqhucn  29167  rrh0  29190  eulerpartlemmf  29567  ballotlem2  29680  ballotlemfc0  29684  ballotlemfcc  29685  ballotlemodife  29689  plymulx0  29753  signstf0  29774  signsvf0  29786  subfacval2  30226  cvmliftlem4  30327  cvmliftlem5  30328  fz0n  30672  bcneg1  30678  bccolsum  30681  fwddifn0  31244  fwddifnp1  31245  knoppcnlem8  31463  knoppcnlem11  31466  poimirlem24  32403  poimirlem27  32406  poimirlem28  32407  sdclem1  32509  heibor1lem  32578  heiborlem4  32583  mzpnegmpt  36125  diophrw  36140  vdioph  36161  diophren  36195  irrapxlem1  36204  rmxy0  36306  monotoddzzfi  36325  zindbi  36329  rmyeq0  36338  jm2.18  36373  jm2.15nn0  36388  jm2.16nn0  36389  mpaaeu  36539  nzss  37338  hashnzfz2  37342  dvradcnv2  37368  binomcxplemnn0  37370  binomcxplemrat  37371  binomcxplemnotnn0  37377  halffl  38251  fz1ssfz0  38265  dvnmul  38634  stoweidlem11  38705  stoweidlem17  38711  stoweidlem26  38720  stoweidlem34  38728  stirlinglem7  38774  fourierdlem20  38821  etransclem25  38953  etransclem26  38954  etransclem37  38965  smfmullem4  39480  fmtnorec2  39795  0evenALTV  39939  0noddALTV  39940  2ffzoeq  40185  1wlkv0  40858  sPthisPth  40931  uhgr1wlkspthlem2  40959  pthdlem2  40973  0ewlk  41281  0wlkOns1  41288  0pth-av  41292  0spth-av  41293  1wlk2v2elem2  41322  ntrl2v2e  41324  1odd  41600  0even  41720  2zrngamgm  41728  altgsumbcALT  41923  blen1  42175  blen1b  42179  0dig1  42200  0dig2pr01  42201  nn0sumshdiglem1  42212  aacllem  42316
  Copyright terms: Public domain W3C validator