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

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

Proof of Theorem 0z
StepHypRef Expression
1 0re 11164 . 2 0 ∈ ℝ
2 eqid 2737 . . 3 0 = 0
323mix1i 1334 . 2 (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4 elz 12508 . 2 (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
51, 3, 4mpbir2an 710 1 0 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  w3o 1087   = wceq 1542  wcel 2107  cr 11057  0cc0 11058  -cneg 11393  cn 12160  cz 12506
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11116  ax-addrcl 11119  ax-rnegex 11129  ax-cnre 11131
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-neg 11395  df-z 12507
This theorem is referenced by:  0zd  12518  elnn0z  12519  nn0ssz  12529  znegcl  12545  zgt0ge1  12564  nnm1ge0  12578  gtndiv  12587  zeo  12596  nn0ind  12605  fnn0ind  12609  eluzaddOLD  12805  eluzsubOLD  12806  nn0uz  12812  1eluzge0  12824  nn0inf  12862  eqreznegel  12866  fz10  13469  fz01en  13476  fzshftral  13536  fznn0  13540  fz1ssfz0  13544  fz0sn  13548  fz0tp  13549  fz0to3un2pr  13550  fz0to4untppr  13551  elfz0ubfz0  13552  fz0sn0fz1  13565  1fv  13567  fzo0n  13601  lbfzo0  13619  elfzonlteqm1  13655  fzo01  13661  fzo0to2pr  13664  fzo0to3tp  13665  ico01fl0  13731  flge0nn0  13732  divfl0  13736  btwnzge0  13740  zmodfz  13805  modid  13808  zmodid2  13811  modmuladdnn0  13827  ltweuz  13873  uzenom  13876  fzennn  13880  cardfz  13882  hashgf1o  13883  f13idfv  13912  seqfn  13925  seq1  13926  seqp1  13928  exp0  13978  bcnn  14219  bcval5  14225  bcpasc  14228  4bc2eq6  14236  hashgadd  14284  hashbc  14357  fz1isolem  14367  hashge2el2dif  14386  fi1uzind  14403  s111  14510  swrdnd  14549  swrds1  14561  repswswrd  14679  cshw0  14689  s2f1o  14812  f1oun2prg  14813  rexfiuz  15239  climz  15438  climaddc1  15524  climmulc2  15526  climsubc1  15527  climsubc2  15528  climlec2  15550  sumss  15616  binomlem  15721  binom  15722  bcxmas  15727  climcndslem1  15741  arisum2  15753  explecnv  15757  geomulcvg  15768  risefall0lem  15916  bpoly1  15941  bpolydiflem  15944  bpoly2  15947  bpoly3  15948  bpoly4  15949  ef0lem  15968  efcvgfsum  15975  ege2le3  15979  eftlub  15998  efgt1p2  16003  efgt1p  16004  ruclem4  16123  ruclem6  16124  nthruc  16141  dvds0  16161  0dvds  16166  fsumdvds  16197  odd2np1lem  16229  divalglem6  16287  divalglem7  16288  divalglem8  16289  bitsfzo  16322  bitsmod  16323  0bits  16326  m1bits  16327  sadc0  16341  smup0  16366  gcd0val  16384  gcddvds  16390  gcd0id  16406  gcdid0  16407  gcdaddm  16412  gcdid  16414  bezoutlem1  16427  bezout  16431  dfgcd2  16434  lcm0val  16477  dvdslcm  16481  lcmeq0  16483  lcmgcd  16490  lcmdvds  16491  lcmftp  16519  lcmfunsnlem2  16523  dfphi2  16653  phiprmpw  16655  pc0  16733  pcdvdstr  16755  dvdsprmpweqnn  16764  pcfaclem  16777  prmreclem2  16796  prmreclem4  16798  zgz  16812  igz  16813  4sqlem19  16842  ramz  16904  1259lem1  17010  1259lem4  17013  2503lem2  17017  4001lem1  17020  4001lem3  17022  gsumws1  18655  mulg0  18886  dfod2  19353  zaddablx  19657  0cyg  19677  srgbinomlem4  19967  zring0  20895  zndvds0  20973  ltbwe  21461  pmatcollpw3fi1  22153  iscmet3lem3  24670  vitalilem1  24988  itgcnlem  25170  dvn0  25304  dvexp3  25358  plyco  25618  0dgr  25622  0dgrb  25623  coefv0  25625  coemulc  25632  vieta1lem2  25687  vieta1  25688  elqaalem1  25695  elqaalem3  25697  aareccl  25702  aannenlem1  25704  aannenlem2  25705  aalioulem1  25708  taylfval  25734  taylplem1  25738  taylplem2  25739  taylpfval  25740  dvtaylp  25745  dvradcnv  25796  pserulm  25797  pserdvlem2  25803  abelthlem6  25811  abelthlem9  25815  logf1o2  26021  ang180lem3  26177  1cubr  26208  leibpi  26308  fsumharmonic  26377  muf  26505  0sgm  26509  1sgmprm  26563  ppiub  26568  bposlem1  26648  bposlem2  26649  lgslem2  26662  lgsfcl2  26667  lgsval2lem  26671  lgs0  26674  lgsdir2lem3  26691  lgsdirnn0  26708  lgsdinn0  26709  pntrlog2bndlem4  26944  padicabv  26994  ostth2lem2  26998  usgrexmpldifpr  28248  usgrexmplef  28249  wlkv0  28641  spthispth  28716  uhgrwkspthlem2  28744  pthdlem2  28758  clwwlkccatlem  28975  0ewlk  29100  0wlkons1  29107  0pth  29111  0pthon  29113  wlk2v2elem2  29142  ntrl2v2e  29144  0dp2dp  31807  cycpmrn  32034  zringnm  32579  qqh0  32605  qqhcn  32612  qqhucn  32613  rrh0  32636  eulerpartlemmf  33015  ballotlem2  33128  ballotlemfc0  33132  ballotlemfcc  33133  plymulx0  33199  signstf0  33220  signsvf0  33232  hgt750lemd  33301  hgt750lem  33304  0nn0m1nnn0  33743  revpfxsfxrev  33749  subfacval2  33821  cvmliftlem4  33922  cvmliftlem5  33923  fz0n  34342  bcneg1  34348  bccolsum  34351  fwddifn0  34778  fwddifnp1  34779  knoppcnlem8  34992  knoppcnlem11  34995  poimirlem24  36131  poimirlem27  36134  poimirlem28  36135  sdclem1  36231  heibor1lem  36297  heiborlem4  36302  bccl2d  40478  0dvds0  40841  mzpnegmpt  41096  diophrw  41111  vdioph  41131  diophren  41165  irrapxlem1  41174  rmxy0  41276  monotoddzzfi  41295  zindbi  41299  rmyeq0  41306  jm2.18  41341  jm2.15nn0  41356  jm2.16nn0  41357  mpaaeu  41506  nzss  42671  hashnzfz2  42675  dvradcnv2  42701  binomcxplemnn0  42703  binomcxplemrat  42704  binomcxplemnotnn0  42710  halffl  43604  lmbr3v  44060  dvnmul  44258  stoweidlem11  44326  stoweidlem17  44332  stirlinglem7  44395  fourierdlem20  44442  etransclem25  44574  etransclem26  44575  etransclem37  44586  smfmullem4  45109  upwordnul  45193  tworepnotupword  45199  2ffzoeq  45634  fmtnorec2  45809  0evenALTV  45954  0noddALTV  45955  2exp340mod341  45999  8exp8mod9  46002  nfermltl8rev  46008  1odd  46179  0even  46303  2zrngamgm  46311  altgsumbcALT  46503  blen1  46744  blen1b  46748  0dig1  46769  0dig2pr01  46770  nn0sumshdiglem1  46781  itcoval0  46822  ackval0  46840  aacllem  47322
  Copyright terms: Public domain W3C validator