Theorem 0z 12620

Description: Zero is an integer. (Contributed by NM, 12-Jan-2002.)

Assertion

Ref	Expression
0z	⊢ 0 ∈ ℤ

Proof of Theorem 0z

Step	Hyp	Ref	Expression
1		0re 11228	. 2 ⊢ 0 ∈ ℝ
2		eqid 2766	. . 3 ⊢ 0 = 0
3	2	3mix1i 1352	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12611	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 724	1 ⊢ 0 ∈ ℤ

This proof depends on syntax axioms:   ∨ w3o 1102   = wceq 1570   ∈ wcel 2146  ℝcr 11117  0cc0 11118  -cneg 11460  ℕcn 12251  ℤcz 12609

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-1cn 11176  ax-addrcl 11179  ax-rnegex 11189  ax-cnre 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-neg 11462  df-z 12610

This theorem is used by:  0zd  12621  elnn0z  12622  nn0ssz  12632  znegcl  12647  zgt0ge1  12668  nnm1ge0  12682  gtndiv  12691  zeo  12700  nn0ind  12709  fnn0ind  12713  nn0uz  12918  1eluzge0  12922  nn0inf  12972  eqreznegel  12976  fz10  13591  fz00m1  13592  fz01en  13599  fzshftral  13662  fznn0  13666  fz1ssfz0  13670  fz0sn  13674  fz0tp  13675  fz0to3un2pr  13676  fz0to4untppr  13677  fz0to5un2tp  13678  elfz0ubfz0  13679  fz0sn0fz1  13692  1fv  13694  fzo0n  13729  lbfzo0  13747  elfzonlteqm1  13789  fzo01  13795  fzo0to2pr  13798  fz01pr  13799  fzo0to3tp  13800  ico01fl0  13872  flge0nn0  13873  divfl0  13877  btwnzge0  13881  zmodfz  13946  modid  13949  zmodid2  13952  modmuladdnn0  13971  ltweuz  14017  uzenom  14020  fzennn  14024  cardfz  14026  hashgf1o  14027  f13idfv  14056  seqfn  14069  seq1  14070  seqp1  14072  exp0  14121  bcnn  14368  bcval5  14374  bcpasc  14377  4bc2eq6  14385  hashgadd  14433  hashbc  14510  fz1isolem  14518  hashge2el2dif  14537  fi1uzind  14564  s111  14675  swrdnd  14716  swrds1  14728  revpfxsfxrev  14829  repswswrd  14847  cshw0  14857  s2f1o  14979  f1oun2prg  14980  rexfiuz  15425  climz  15626  climaddc1  15712  climmulc2  15714  climsubc1  15715  climsubc2  15716  climlec2  15736  sumss  15801  binomlem  15909  binom  15910  bcxmas  15915  climcndslem1  15929  arisum2  15941  explecnv  15945  geomulcvg  15956  bpoly1  16130  bpolydiflem  16133  bpoly2  16136  bpoly3  16137  bpoly4  16138  ef0lem  16157  efcvgfsum  16165  ege2le3  16169  eftlub  16190  efgt1p2  16195  efgt1p  16196  ruclem4  16315  ruclem6  16316  nthruc  16333  dvds0  16354  0dvds  16359  fsumdvds  16391  odd2np1lem  16423  divalglem6  16481  divalglem7  16482  divalglem8  16483  bitsfzo  16518  bitsmod  16519  0bits  16522  m1bits  16523  sadc0  16537  smup0  16562  gcd0val  16580  gcddvds  16586  gcd0id  16602  gcdid0  16603  gcdaddm  16608  gcdid  16610  bezoutlem1  16622  bezout  16626  dfgcd2  16629  lcm0val  16677  dvdslcm  16681  lcmeq0  16683  lcmgcd  16690  lcmdvds  16691  lcmftp  16719  lcmfunsnlem2  16723  dfphi2  16858  phiprmpw  16860  pc0  16939  pcdvdstr  16961  dvdsprmpweqnn  16970  pcfaclem  16983  prmreclem2  17002  prmreclem4  17004  zgz  17018  igz  17019  4sqlem19  17048  ramz  17110  1259lem1  17216  1259lem4  17219  2503lem2  17223  4001lem1  17226  4001lem3  17228  chnub  18703  gsumws1  18928  mulg0  19171  dfod2  19665  zaddablx  19973  0cyg  19994  srgbinomlem4  20342  zringsub  21642  zring0  21645  pzriprnglem3  21670  pzriprnglem4  21671  pzriprnglem5  21672  pzriprnglem6  21673  pzriprnglem10  21677  pzriprng1ALT  21683  zndvds0  21737  ltbwe  22232  pmatcollpw3fi1  22982  iscmet3lem3  25486  vitalilem1  25804  itgcnlem  25986  dvn0  26120  dvexp3  26174  plyco  26435  0dgr  26439  0dgrb  26440  coefv0  26442  coemulc  26449  plyn0mulidp  26479  vieta1lem2  26509  vieta1  26510  elqaalem1  26517  elqaalem3  26519  0aa  26523  aareccl  26526  aannenlem1  26528  aannenlem2  26529  aalioulem1  26532  taylfval  26559  taylplem1  26563  taylplem2  26564  taylpfval  26565  dvtaylp  26570  dvradcnv  26621  pserulm  26622  pserdvlem2  26628  abelthlem6  26636  abelthlem9  26640  logf1o2  26852  ang180lem3  27013  1cubr  27044  leibpi  27144  fsumharmonic  27213  muf  27341  0sgm  27345  1sgmprm  27400  ppiub  27405  bposlem1  27485  bposlem2  27486  lgslem2  27499  lgsfcl2  27504  lgsval2lem  27508  lgs0  27511  lgsdir2lem3  27528  lgsdirnn0  27545  lgsdinn0  27546  pntrlog2bndlem4  27781  padicabv  27831  ostth2lem2  27835  usgrexmpldifpr  29645  usgrexmplef  29646  wlkv0  30036  spthispth  30110  dfpth2  30115  uhgrwkspthlem2  30140  pthdlem2  30154  clwwlkccatlem  30377  0ewlk  30502  0wlkons1  30509  0pth  30513  0pthon  30515  wlk2v2elem2  30544  ntrl2v2e  30546  fzo0opth  33185  0dp2dp  33265  cycpmrn  33494  elrgspnlem1  33593  constrextdg2  34170  zringnm  34379  qqh0  34405  qqhcn  34412  qqhucn  34413  rrh0  34436  eulerpartlemmf  34797  ballotlem2  34911  ballotlemfc0  34915  ballotlemfcc  34916  signstf0  34987  signsvf0  34999  hgt750lemd  35067  hgt750lem  35070  0nn0m1nnn0  35628  subfacval2  35700  cvmliftlem4  35801  cvmliftlem5  35802  fz0n  36244  bcneg1  36249  bccolsum  36252  fwddifn0  36677  fwddifnp1  36678  knoppcnlem8  37130  knoppcnlem11  37133  poimirlem24  38336  poimirlem27  38339  poimirlem28  38340  sdclem1  38435  heibor1lem  38501  heiborlem4  38506  bccl2d  42799  aks6d1c1  42924  aks6d1c2lem4  42935  0dvds0  43129  mzpnegmpt  43516  diophrw  43531  vdioph  43551  diophren  43581  irrapxlem1  43590  rmxy0  43691  monotoddzzfi  43710  zindbi  43714  rmyeq0  43721  jm2.18  43756  jm2.15nn0  43771  jm2.16nn0  43772  mpaaeu  43918  nzss  45068  hashnzfz2  45072  dvradcnv2  45098  binomcxplemnn0  45100  binomcxplemrat  45101  binomcxplemnotnn0  45107  halffl  46056  lmbr3v  46500  dvnmul  46698  stoweidlem11  46766  stoweidlem17  46772  stirlinglem7  46835  fourierdlem20  46882  etransclem25  47014  etransclem26  47015  etransclem37  47026  smfmullem4  47549  chnsubseqwl  47636  2ffzoeq  48106  fmtnorec2  48336  0evenALTV  48494  0noddALTV  48495  2exp340mod341  48539  8exp8mod9  48542  nfermltl8rev  48548  gpgusgralem  48862  1odd  48977  0even  49043  2zrngamgm  49051  altgsumbcALT  49174  blen1  49405  blen1b  49409  0dig1  49430  0dig2pr01  49431  nn0sumshdiglem1  49442  itcoval0  49483  ackval0  49501  aacllem  50662