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

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

Proof of Theorem 0z
StepHypRef Expression
1 0re 10632 . 2 0 ∈ ℝ
2 eqid 2821 . . 3 0 = 0
323mix1i 1325 . 2 (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4 elz 11972 . 2 (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
51, 3, 4mpbir2an 707 1 0 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  w3o 1078   = wceq 1528  wcel 2105  cr 10525  0cc0 10526  -cneg 10860  cn 11627  cz 11970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-1cn 10584  ax-addrcl 10587  ax-rnegex 10597  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148  df-neg 10862  df-z 11971
This theorem is referenced by:  0zd  11982  elnn0z  11983  nn0ssz  11992  znegcl  12006  zgt0ge1  12025  nnm1ge0  12039  gtndiv  12048  zeo  12057  nn0ind  12066  fnn0ind  12070  eluzadd  12262  eluzsub  12263  nn0uz  12269  1eluzge0  12281  nn0inf  12319  eqreznegel  12323  fz10  12918  fz01en  12925  fzshftral  12985  fznn0  12989  fz1ssfz0  12993  fz0sn  12997  fz0tp  12998  fz0to3un2pr  12999  fz0to4untppr  13000  elfz0ubfz0  13001  fz0sn0fz1  13014  1fv  13016  fzo0n  13049  lbfzo0  13067  elfzonlteqm1  13103  fzo01  13109  fzo0to2pr  13112  fzo0to3tp  13113  ico01fl0  13179  flge0nn0  13180  divfl0  13184  btwnzge0  13188  zmodfz  13251  modid  13254  zmodid2  13257  modmuladdnn0  13273  ltweuz  13319  uzenom  13322  fzennn  13326  cardfz  13328  hashgf1o  13329  f13idfv  13358  seqfn  13371  seq1  13372  seqp1  13374  exp0  13423  bcnn  13662  bcval5  13668  bcpasc  13671  4bc2eq6  13679  hashgadd  13728  hashbc  13801  fz1isolem  13809  hashge2el2dif  13828  fi1uzind  13845  s111  13959  swrdnd  14006  swrds1  14018  repswswrd  14136  cshw0  14146  s2f1o  14268  f1oun2prg  14269  rexfiuz  14697  climz  14896  climaddc1  14981  climmulc2  14983  climsubc1  14984  climsubc2  14985  climlec2  15005  sumss  15071  binomlem  15174  binom  15175  bcxmas  15180  climcndslem1  15194  arisum2  15206  explecnv  15210  geomulcvg  15222  risefall0lem  15370  bpoly1  15395  bpolydiflem  15398  bpoly2  15401  bpoly3  15402  bpoly4  15403  ef0lem  15422  efcvgfsum  15429  ege2le3  15433  eftlub  15452  efgt1p2  15457  efgt1p  15458  ruclem4  15577  ruclem6  15578  nthruc  15595  dvds0  15615  0dvds  15620  fsumdvds  15648  odd2np1lem  15679  divalglem6  15739  divalglem7  15740  divalglem8  15741  bitsfzo  15774  bitsmod  15775  0bits  15778  m1bits  15779  sadc0  15793  smup0  15818  gcd0val  15836  gcddvds  15842  gcd0id  15857  gcdid0  15858  gcdaddm  15863  gcdid  15865  bezoutlem1  15877  bezout  15881  dfgcd2  15884  lcm0val  15928  dvdslcm  15932  lcmeq0  15934  lcmgcd  15941  lcmdvds  15942  lcmftp  15970  lcmfunsnlem2  15974  dfphi2  16101  phiprmpw  16103  pc0  16181  pcdvdstr  16202  dvdsprmpweqnn  16211  pcfaclem  16224  prmreclem2  16243  prmreclem4  16245  zgz  16259  igz  16260  4sqlem19  16289  ramz  16351  1259lem1  16454  1259lem4  16457  2503lem2  16461  4001lem1  16464  4001lem3  16466  gsumws1  17992  mulg0  18171  dfod2  18622  zaddablx  18923  0cyg  18944  srgbinomlem4  19224  ltbwe  20183  zring0  20557  zndvds0  20627  pmatcollpw3fi1  21326  iscmet3lem3  23822  vitalilem1  24138  itgcnlem  24319  dvn0  24450  dvexp3  24504  plyco  24760  0dgr  24764  0dgrb  24765  coefv0  24767  coemulc  24774  vieta1lem2  24829  vieta1  24830  elqaalem1  24837  elqaalem3  24839  aareccl  24844  aannenlem1  24846  aannenlem2  24847  aalioulem1  24850  taylfval  24876  taylplem1  24880  taylplem2  24881  taylpfval  24882  dvtaylp  24887  dvradcnv  24938  pserulm  24939  pserdvlem2  24945  abelthlem6  24953  abelthlem9  24957  logf1o2  25160  ang180lem3  25316  1cubr  25347  leibpi  25448  fsumharmonic  25517  muf  25645  0sgm  25649  1sgmprm  25703  ppiub  25708  bposlem1  25788  bposlem2  25789  lgslem2  25802  lgsfcl2  25807  lgsval2lem  25811  lgs0  25814  lgsdir2lem3  25831  lgsdirnn0  25848  lgsdinn0  25849  pntrlog2bndlem4  26084  padicabv  26134  ostth2lem2  26138  usgrexmpldifpr  26968  usgrexmplef  26969  wlkv0  27360  spthispth  27435  uhgrwkspthlem2  27463  pthdlem2  27477  clwwlkccatlem  27695  0ewlk  27821  0wlkons1  27828  0pth  27832  0pthon  27834  wlk2v2elem2  27863  ntrl2v2e  27865  0dp2dp  30513  cycpmrn  30713  zringnm  31101  qqh0  31125  qqhcn  31132  qqhucn  31133  rrh0  31156  eulerpartlemmf  31533  ballotlem2  31646  ballotlemfc0  31650  ballotlemfcc  31651  plymulx0  31717  signstf0  31738  signsvf0  31750  hgt750lemd  31819  hgt750lem  31822  0nn0m1nnn0  32249  revpfxsfxrev  32260  subfacval2  32332  cvmliftlem4  32433  cvmliftlem5  32434  fz0n  32860  bcneg1  32866  bccolsum  32869  fwddifn0  33523  fwddifnp1  33524  knoppcnlem8  33737  knoppcnlem11  33740  poimirlem24  34798  poimirlem27  34801  poimirlem28  34802  sdclem1  34901  heibor1lem  34970  heiborlem4  34975  mzpnegmpt  39221  diophrw  39236  vdioph  39256  diophren  39290  irrapxlem1  39299  rmxy0  39400  monotoddzzfi  39419  zindbi  39423  rmyeq0  39430  jm2.18  39465  jm2.15nn0  39480  jm2.16nn0  39481  mpaaeu  39630  nzss  40529  hashnzfz2  40533  dvradcnv2  40559  binomcxplemnn0  40561  binomcxplemrat  40562  binomcxplemnotnn0  40568  halffl  41443  lmbr3v  41906  dvnmul  42108  stoweidlem11  42177  stoweidlem17  42183  stirlinglem7  42246  fourierdlem20  42293  etransclem25  42425  etransclem26  42426  etransclem37  42437  smfmullem4  42950  2ffzoeq  43409  fmtnorec2  43552  0evenALTV  43700  0noddALTV  43701  2exp340mod341  43745  8exp8mod9  43748  nfermltl8rev  43754  1odd  43925  0even  44100  2zrngamgm  44108  altgsumbcALT  44299  blen1  44542  blen1b  44546  0dig1  44567  0dig2pr01  44568  nn0sumshdiglem1  44579  aacllem  44800
  Copyright terms: Public domain W3C validator