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

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

Proof of Theorem 0z
StepHypRef Expression
1 0re 10037 . 2 0 ∈ ℝ
2 eqid 2621 . . 3 0 = 0
323mix1i 1232 . 2 (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4 elz 11376 . 2 (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
51, 3, 4mpbir2an 955 1 0 ∈ ℤ
Colors of variables: wff setvar class
Syntax hints:  w3o 1036   = wceq 1482  wcel 1989  cr 9932  0cc0 9933  -cneg 10264  cn 11017  cz 11374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-1cn 9991  ax-icn 9992  ax-addcl 9993  ax-addrcl 9994  ax-mulcl 9995  ax-mulrcl 9996  ax-i2m1 10001  ax-1ne0 10002  ax-rnegex 10004  ax-rrecex 10005  ax-cnre 10006
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-iota 5849  df-fv 5894  df-ov 6650  df-neg 10266  df-z 11375
This theorem is referenced by:  0zd  11386  elnn0z  11387  nn0ssz  11395  znegcl  11409  zgt0ge1  11428  nnm1ge0  11442  gtndiv  11451  zeo  11460  nn0ind  11469  fnn0ind  11473  eluzadd  11713  eluzsub  11714  nn0uz  11719  1eluzge0  11729  nn0inf  11767  eqreznegel  11771  fz10  12359  fz01en  12366  fzshftral  12424  fznn0  12428  fz0sn  12435  fz0tp  12436  fz0to3un2pr  12437  fz0to4untppr  12438  elfz0ubfz0  12439  fz0sn0fz1  12452  1fv  12454  fzo0n  12486  lbfzo0  12503  elfzonlteqm1  12539  fzo01  12546  fzo0to2pr  12549  fzo0to3tp  12550  ico01fl0  12615  flge0nn0  12616  divfl0  12620  btwnzge0  12624  zmodfz  12687  modid  12690  zmodid2  12693  modmuladdnn0  12709  ltweuz  12755  uzenom  12758  fzennn  12762  cardfz  12764  hashgf1o  12765  f13idfv  12795  seqfn  12808  seq1  12809  seqp1  12811  exp0  12859  bcnn  13094  bcm1k  13097  bcval5  13100  bcpasc  13103  4bc2eq6  13111  hashgadd  13161  hashbc  13232  fz1isolem  13240  hashge2el2dif  13257  fi1uzind  13274  fi1uzindOLD  13280  s111  13390  swrdnd  13426  swrds1  13445  repswswrd  13525  cshw0  13534  s2f1o  13655  f1oun2prg  13656  rexfiuz  14081  climz  14274  climaddc1  14359  climmulc2  14361  climsubc1  14362  climsubc2  14363  climlec2  14383  sumss  14449  binomlem  14555  binom  14556  bcxmas  14561  climcndslem1  14575  arisum2  14587  explecnv  14591  geomulcvg  14601  risefall0lem  14751  binomfallfac  14766  bpoly1  14776  bpolydiflem  14779  bpoly2  14782  bpoly3  14783  bpoly4  14784  ef0lem  14803  efcvgfsum  14810  ege2le3  14814  eftlub  14833  efgt1p2  14838  efgt1p  14839  ruclem4  14957  ruclem6  14958  nthruc  14975  dvds0  14991  0dvds  14996  fsumdvds  15024  odd2np1lem  15058  divalglem6  15115  divalglem7  15116  divalglem8  15117  bitsfzo  15151  bitsmod  15152  0bits  15155  m1bits  15156  sadc0  15170  smup0  15195  gcd0val  15213  gcddvds  15219  gcd0id  15234  gcdid0  15235  gcdaddm  15240  gcdid  15242  bezoutlem1  15250  bezout  15254  dfgcd2  15257  lcm0val  15301  dvdslcm  15305  lcmeq0  15307  lcmgcd  15314  lcmdvds  15315  lcmftp  15343  lcmfunsnlem2  15347  dfphi2  15473  phiprmpw  15475  prmdiveq  15485  prmdivdiv  15486  pc0  15553  pcdvdstr  15574  dvdsprmpweqnn  15583  pcfaclem  15596  prmreclem2  15615  prmreclem4  15617  zgz  15631  igz  15632  4sqlem19  15661  vdwap0  15674  ramz  15723  1259lem1  15832  1259lem4  15835  2503lem2  15839  4001lem1  15842  4001lem3  15844  gsumws1  17370  mulg0  17540  dfod2  17975  zaddablx  18269  0cyg  18288  srgbinomlem4  18537  srgbinom  18539  ltbwe  19466  zring0  19822  zndvds0  19893  pmatcollpw3fi1lem1  20585  pmatcollpw3fi1  20587  iscmet3lem3  23082  vitalilem1  23370  vitalilem1OLD  23371  iblcnlem1  23548  itgcnlem  23550  dvn0  23681  dvexp3  23735  plyco  23991  0dgr  23995  0dgrb  23996  coefv0  23998  coemulc  24005  vieta1lem2  24060  vieta1  24061  elqaalem1  24068  elqaalem3  24070  aareccl  24075  aannenlem1  24077  aannenlem2  24078  aalioulem1  24081  taylfval  24107  taylplem1  24111  taylplem2  24112  taylpfval  24113  dvtaylp  24118  dvradcnv  24169  pserulm  24170  pserdvlem2  24176  abelthlem6  24184  abelthlem9  24188  logf1o2  24390  advlogexp  24395  ang180lem3  24535  1cubr  24563  leibpi  24663  fsumharmonic  24732  wilthlem1  24788  muf  24860  0sgm  24864  1sgmprm  24918  ppiub  24923  bposlem1  25003  bposlem2  25004  lgslem2  25017  lgsfcl2  25022  lgsval2lem  25026  lgs0  25029  lgsdir2lem3  25046  lgsdirnn0  25063  lgsdinn0  25064  pntrlog2bndlem4  25263  padicabv  25313  ostth2lem2  25317  usgrexmpldifpr  26144  usgrexmplef  26145  wlkv0  26541  spthispth  26616  uhgrwkspthlem2  26644  pthdlem2  26658  0ewlk  26968  0wlkons1  26975  0pth  26979  0pthon  26981  wlk2v2elem2  27009  ntrl2v2e  27011  0dp2dp  29602  zringnm  29989  qqh0  30013  qqhcn  30020  qqhucn  30021  rrh0  30044  eulerpartlemmf  30422  ballotlem2  30535  ballotlemfc0  30539  ballotlemfcc  30540  ballotlemodife  30544  plymulx0  30609  signstf0  30630  signsvf0  30642  hgt750lemd  30711  hgt750lem  30714  subfacval2  31154  cvmliftlem4  31255  cvmliftlem5  31256  fz0n  31602  bcneg1  31608  bccolsum  31611  fwddifn0  32255  fwddifnp1  32256  knoppcnlem8  32474  knoppcnlem11  32477  poimirlem24  33413  poimirlem27  33416  poimirlem28  33417  sdclem1  33519  heibor1lem  33588  heiborlem4  33593  mzpnegmpt  37133  diophrw  37148  vdioph  37169  diophren  37203  irrapxlem1  37212  rmxy0  37314  monotoddzzfi  37333  zindbi  37337  rmyeq0  37346  jm2.18  37381  jm2.15nn0  37396  jm2.16nn0  37397  mpaaeu  37546  nzss  38342  hashnzfz2  38346  dvradcnv2  38372  binomcxplemnn0  38374  binomcxplemrat  38375  binomcxplemnotnn0  38381  halffl  39329  fz1ssfz0  39343  dvnmul  39927  stoweidlem11  39997  stoweidlem17  40003  stoweidlem26  40012  stoweidlem34  40020  stirlinglem7  40066  fourierdlem20  40113  etransclem25  40245  etransclem26  40246  etransclem37  40257  smfmullem4  40770  2ffzoeq  41107  fmtnorec2  41226  0evenALTV  41370  0noddALTV  41371  1odd  41582  0even  41702  2zrngamgm  41710  altgsumbcALT  41902  blen1  42149  blen1b  42153  0dig1  42174  0dig2pr01  42175  nn0sumshdiglem1  42186  aacllem  42318
  Copyright terms: Public domain W3C validator