Theorem 0z 12476

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 11111	. 2 ⊢ 0 ∈ ℝ
2		eqid 2731	. . 3 ⊢ 0 = 0
3	2	3mix1i 1334	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12467	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 711	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1085   = wceq 1541   ∈ wcel 2111  ℝcr 11002  0cc0 11003  -cneg 11342  ℕcn 12122  ℤcz 12465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11061  ax-addrcl 11064  ax-rnegex 11074  ax-cnre 11076

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-neg 11344  df-z 12466

This theorem is referenced by:  0zd  12477  elnn0z  12478  nn0ssz  12488  znegcl  12504  zgt0ge1  12524  nnm1ge0  12538  gtndiv  12547  zeo  12556  nn0ind  12565  fnn0ind  12569  eluzaddOLD  12764  eluzsubOLD  12765  nn0uz  12771  1eluzge0  12775  nn0inf  12825  eqreznegel  12829  fz10  13442  fz01en  13449  fzshftral  13512  fznn0  13516  fz1ssfz0  13520  fz0sn  13524  fz0tp  13525  fz0to3un2pr  13526  fz0to4untppr  13527  fz0to5un2tp  13528  elfz0ubfz0  13529  fz0sn0fz1  13542  1fv  13544  fzo0n  13578  lbfzo0  13596  elfzonlteqm1  13638  fzo01  13644  fzo0to2pr  13647  fz01pr  13648  fzo0to3tp  13649  ico01fl0  13720  flge0nn0  13721  divfl0  13725  btwnzge0  13729  zmodfz  13794  modid  13797  zmodid2  13800  modmuladdnn0  13819  ltweuz  13865  uzenom  13868  fzennn  13872  cardfz  13874  hashgf1o  13875  f13idfv  13904  seqfn  13917  seq1  13918  seqp1  13920  exp0  13969  bcnn  14216  bcval5  14222  bcpasc  14225  4bc2eq6  14233  hashgadd  14281  hashbc  14357  fz1isolem  14365  hashge2el2dif  14384  fi1uzind  14411  s111  14520  swrdnd  14559  swrds1  14571  repswswrd  14688  cshw0  14698  s2f1o  14820  f1oun2prg  14821  rexfiuz  15252  climz  15453  climaddc1  15539  climmulc2  15541  climsubc1  15542  climsubc2  15543  climlec2  15563  sumss  15628  binomlem  15733  binom  15734  bcxmas  15739  climcndslem1  15753  arisum2  15765  explecnv  15769  geomulcvg  15780  risefall0lem  15930  bpoly1  15955  bpolydiflem  15958  bpoly2  15961  bpoly3  15962  bpoly4  15963  ef0lem  15982  efcvgfsum  15990  ege2le3  15994  eftlub  16015  efgt1p2  16020  efgt1p  16021  ruclem4  16140  ruclem6  16141  nthruc  16158  dvds0  16179  0dvds  16184  fsumdvds  16216  odd2np1lem  16248  divalglem6  16306  divalglem7  16307  divalglem8  16308  bitsfzo  16343  bitsmod  16344  0bits  16347  m1bits  16348  sadc0  16362  smup0  16387  gcd0val  16405  gcddvds  16411  gcd0id  16427  gcdid0  16428  gcdaddm  16433  gcdid  16435  bezoutlem1  16447  bezout  16451  dfgcd2  16454  lcm0val  16502  dvdslcm  16506  lcmeq0  16508  lcmgcd  16515  lcmdvds  16516  lcmftp  16544  lcmfunsnlem2  16548  dfphi2  16682  phiprmpw  16684  pc0  16763  pcdvdstr  16785  dvdsprmpweqnn  16794  pcfaclem  16807  prmreclem2  16826  prmreclem4  16828  zgz  16842  igz  16843  4sqlem19  16872  ramz  16934  1259lem1  17039  1259lem4  17042  2503lem2  17046  4001lem1  17049  4001lem3  17051  chnub  18525  gsumws1  18743  mulg0  18984  dfod2  19474  zaddablx  19782  0cyg  19803  srgbinomlem4  20145  zringsub  21390  zring0  21393  pzriprnglem3  21418  pzriprnglem4  21419  pzriprnglem5  21420  pzriprnglem6  21421  pzriprnglem10  21425  pzriprng1ALT  21431  zndvds0  21485  ltbwe  21977  pmatcollpw3fi1  22701  iscmet3lem3  25215  vitalilem1  25534  itgcnlem  25716  dvn0  25851  dvexp3  25907  plyco  26171  0dgr  26175  0dgrb  26176  coefv0  26178  coemulc  26185  vieta1lem2  26244  vieta1  26245  elqaalem1  26252  elqaalem3  26254  aareccl  26259  aannenlem1  26261  aannenlem2  26262  aalioulem1  26265  taylfval  26291  taylplem1  26295  taylplem2  26296  taylpfval  26297  dvtaylp  26303  dvradcnv  26355  pserulm  26356  pserdvlem2  26363  abelthlem6  26371  abelthlem9  26375  logf1o2  26584  ang180lem3  26746  1cubr  26777  leibpi  26877  fsumharmonic  26947  muf  27075  0sgm  27079  1sgmprm  27135  ppiub  27140  bposlem1  27220  bposlem2  27221  lgslem2  27234  lgsfcl2  27239  lgsval2lem  27243  lgs0  27246  lgsdir2lem3  27263  lgsdirnn0  27280  lgsdinn0  27281  pntrlog2bndlem4  27516  padicabv  27566  ostth2lem2  27570  usgrexmpldifpr  29234  usgrexmplef  29235  wlkv0  29626  spthispth  29700  dfpth2  29705  uhgrwkspthlem2  29730  pthdlem2  29744  clwwlkccatlem  29964  0ewlk  30089  0wlkons1  30096  0pth  30100  0pthon  30102  wlk2v2elem2  30131  ntrl2v2e  30133  fzo0opth  32780  0dp2dp  32884  cycpmrn  33107  elrgspnlem1  33204  constrextdg2  33757  zringnm  33966  qqh0  33992  qqhcn  33999  qqhucn  34000  rrh0  34023  eulerpartlemmf  34383  ballotlem2  34497  ballotlemfc0  34501  ballotlemfcc  34502  plymulx0  34555  signstf0  34576  signsvf0  34588  hgt750lemd  34656  hgt750lem  34659  0nn0m1nnn0  35145  revpfxsfxrev  35148  subfacval2  35219  cvmliftlem4  35320  cvmliftlem5  35321  fz0n  35763  bcneg1  35768  bccolsum  35771  fwddifn0  36197  fwddifnp1  36198  knoppcnlem8  36533  knoppcnlem11  36536  poimirlem24  37683  poimirlem27  37686  poimirlem28  37687  sdclem1  37782  heibor1lem  37848  heiborlem4  37853  bccl2d  42023  aks6d1c1  42148  aks6d1c2lem4  42159  0dvds0  42359  mzpnegmpt  42776  diophrw  42791  vdioph  42811  diophren  42845  irrapxlem1  42854  rmxy0  42955  monotoddzzfi  42974  zindbi  42978  rmyeq0  42985  jm2.18  43020  jm2.15nn0  43035  jm2.16nn0  43036  mpaaeu  43182  nzss  44349  hashnzfz2  44353  dvradcnv2  44379  binomcxplemnn0  44381  binomcxplemrat  44382  binomcxplemnotnn0  44388  halffl  45336  lmbr3v  45782  dvnmul  45980  stoweidlem11  46048  stoweidlem17  46054  stirlinglem7  46117  fourierdlem20  46164  etransclem25  46296  etransclem26  46297  etransclem37  46308  smfmullem4  46831  2ffzoeq  47357  fmtnorec2  47573  0evenALTV  47718  0noddALTV  47719  2exp340mod341  47763  8exp8mod9  47766  nfermltl8rev  47772  gpgusgralem  48086  1odd  48201  0even  48267  2zrngamgm  48275  altgsumbcALT  48383  blen1  48615  blen1b  48619  0dig1  48640  0dig2pr01  48641  nn0sumshdiglem1  48652  itcoval0  48693  ackval0  48711  aacllem  49832