Theorem 0z 12533

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 11144	. 2 ⊢ 0 ∈ ℝ
2		eqid 2740	. . 3 ⊢ 0 = 0
3	2	3mix1i 1340	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12524	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 717	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1091   = wceq 1547   ∈ wcel 2119  ℝcr 11035  0cc0 11036  -cneg 11376  ℕcn 12172  ℤcz 12522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-1cn 11094  ax-addrcl 11097  ax-rnegex 11107  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-neg 11378  df-z 12523

This theorem is referenced by:  0zd  12534  elnn0z  12535  nn0ssz  12545  znegcl  12560  zgt0ge1  12581  nnm1ge0  12595  gtndiv  12604  zeo  12613  nn0ind  12622  fnn0ind  12626  nn0uz  12824  1eluzge0  12828  nn0inf  12878  eqreznegel  12882  fz10  13497  fz01en  13504  fzshftral  13567  fznn0  13571  fz1ssfz0  13575  fz0sn  13579  fz0tp  13580  fz0to3un2pr  13581  fz0to4untppr  13582  fz0to5un2tp  13583  elfz0ubfz0  13584  fz0sn0fz1  13597  1fv  13599  fzo0n  13634  lbfzo0  13652  elfzonlteqm1  13694  fzo01  13700  fzo0to2pr  13703  fz01pr  13704  fzo0to3tp  13705  ico01fl0  13776  flge0nn0  13777  divfl0  13781  btwnzge0  13785  zmodfz  13850  modid  13853  zmodid2  13856  modmuladdnn0  13875  ltweuz  13921  uzenom  13924  fzennn  13928  cardfz  13930  hashgf1o  13931  f13idfv  13960  seqfn  13973  seq1  13974  seqp1  13976  exp0  14025  bcnn  14272  bcval5  14278  bcpasc  14281  4bc2eq6  14289  hashgadd  14337  hashbc  14413  fz1isolem  14421  hashge2el2dif  14440  fi1uzind  14467  s111  14576  swrdnd  14615  swrds1  14627  repswswrd  14744  cshw0  14754  s2f1o  14876  f1oun2prg  14877  rexfiuz  15308  climz  15509  climaddc1  15595  climmulc2  15597  climsubc1  15598  climsubc2  15599  climlec2  15619  sumss  15684  binomlem  15792  binom  15793  bcxmas  15798  climcndslem1  15812  arisum2  15824  explecnv  15828  geomulcvg  15839  risefall0lem  15989  bpoly1  16014  bpolydiflem  16017  bpoly2  16020  bpoly3  16021  bpoly4  16022  ef0lem  16041  efcvgfsum  16049  ege2le3  16053  eftlub  16074  efgt1p2  16079  efgt1p  16080  ruclem4  16199  ruclem6  16200  nthruc  16217  dvds0  16238  0dvds  16243  fsumdvds  16275  odd2np1lem  16307  divalglem6  16365  divalglem7  16366  divalglem8  16367  bitsfzo  16402  bitsmod  16403  0bits  16406  m1bits  16407  sadc0  16421  smup0  16446  gcd0val  16464  gcddvds  16470  gcd0id  16486  gcdid0  16487  gcdaddm  16492  gcdid  16494  bezoutlem1  16506  bezout  16510  dfgcd2  16513  lcm0val  16561  dvdslcm  16565  lcmeq0  16567  lcmgcd  16574  lcmdvds  16575  lcmftp  16603  lcmfunsnlem2  16607  dfphi2  16742  phiprmpw  16744  pc0  16823  pcdvdstr  16845  dvdsprmpweqnn  16854  pcfaclem  16867  prmreclem2  16886  prmreclem4  16888  zgz  16902  igz  16903  4sqlem19  16932  ramz  16994  1259lem1  17099  1259lem4  17102  2503lem2  17106  4001lem1  17109  4001lem3  17111  chnub  18586  gsumws1  18804  mulg0  19048  dfod2  19537  zaddablx  19845  0cyg  19866  srgbinomlem4  20208  zringsub  21437  zring0  21440  pzriprnglem3  21465  pzriprnglem4  21466  pzriprnglem5  21467  pzriprnglem6  21468  pzriprnglem10  21472  pzriprng1ALT  21478  zndvds0  21532  ltbwe  22027  pmatcollpw3fi1  22778  iscmet3lem3  25282  vitalilem1  25600  itgcnlem  25782  dvn0  25916  dvexp3  25970  plyco  26231  0dgr  26235  0dgrb  26236  coefv0  26238  coemulc  26245  vieta1lem2  26302  vieta1  26303  elqaalem1  26310  elqaalem3  26312  aareccl  26317  aannenlem1  26319  aannenlem2  26320  aalioulem1  26323  taylfval  26349  taylplem1  26353  taylplem2  26354  taylpfval  26355  dvtaylp  26360  dvradcnv  26411  pserulm  26412  pserdvlem2  26418  abelthlem6  26426  abelthlem9  26430  logf1o2  26639  ang180lem3  26800  1cubr  26831  leibpi  26931  fsumharmonic  27000  muf  27128  0sgm  27132  1sgmprm  27187  ppiub  27192  bposlem1  27272  bposlem2  27273  lgslem2  27286  lgsfcl2  27291  lgsval2lem  27295  lgs0  27298  lgsdir2lem3  27315  lgsdirnn0  27332  lgsdinn0  27333  pntrlog2bndlem4  27568  padicabv  27618  ostth2lem2  27622  usgrexmpldifpr  29352  usgrexmplef  29353  wlkv0  29743  spthispth  29817  dfpth2  29822  uhgrwkspthlem2  29847  pthdlem2  29861  clwwlkccatlem  30084  0ewlk  30209  0wlkons1  30216  0pth  30220  0pthon  30222  wlk2v2elem2  30251  ntrl2v2e  30253  fzo0opth  32902  0dp2dp  32994  cycpmrn  33231  elrgspnlem1  33330  constrextdg2  33940  zringnm  34149  qqh0  34175  qqhcn  34182  qqhucn  34183  rrh0  34206  eulerpartlemmf  34566  ballotlem2  34680  ballotlemfc0  34684  ballotlemfcc  34685  plymulx0  34738  signstf0  34759  signsvf0  34771  hgt750lemd  34839  hgt750lem  34842  0nn0m1nnn0  35348  revpfxsfxrev  35351  subfacval2  35422  cvmliftlem4  35523  cvmliftlem5  35524  fz0n  35966  bcneg1  35971  bccolsum  35974  fwddifn0  36399  fwddifnp1  36400  knoppcnlem8  36813  knoppcnlem11  36816  poimirlem24  38018  poimirlem27  38021  poimirlem28  38022  sdclem1  38117  heibor1lem  38183  heiborlem4  38188  bccl2d  42483  aks6d1c1  42608  aks6d1c2lem4  42619  0dvds0  42811  mzpnegmpt  43200  diophrw  43215  vdioph  43235  diophren  43265  irrapxlem1  43274  rmxy0  43375  monotoddzzfi  43394  zindbi  43398  rmyeq0  43405  jm2.18  43440  jm2.15nn0  43455  jm2.16nn0  43456  mpaaeu  43602  nzss  44768  hashnzfz2  44772  dvradcnv2  44798  binomcxplemnn0  44800  binomcxplemrat  44801  binomcxplemnotnn0  44807  halffl  45751  lmbr3v  46195  dvnmul  46393  stoweidlem11  46461  stoweidlem17  46467  stirlinglem7  46530  fourierdlem20  46577  etransclem25  46709  etransclem26  46710  etransclem37  46721  smfmullem4  47244  chnsubseqwl  47331  2ffzoeq  47798  fmtnorec2  48028  0evenALTV  48186  0noddALTV  48187  2exp340mod341  48231  8exp8mod9  48234  nfermltl8rev  48240  gpgusgralem  48554  1odd  48669  0even  48735  2zrngamgm  48743  altgsumbcALT  48851  blen1  49082  blen1b  49086  0dig1  49107  0dig2pr01  49108  nn0sumshdiglem1  49119  itcoval0  49160  ackval0  49178  aacllem  50298