Theorem 0z 12540

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

Syntax hints:   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  ℝcr 11067  0cc0 11068  -cneg 11406  ℕcn 12186  ℤcz 12529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addrcl 11129  ax-rnegex 11139  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530

This theorem is referenced by:  0zd  12541  elnn0z  12542  nn0ssz  12552  znegcl  12568  zgt0ge1  12588  nnm1ge0  12602  gtndiv  12611  zeo  12620  nn0ind  12629  fnn0ind  12633  eluzaddOLD  12828  eluzsubOLD  12829  nn0uz  12835  1eluzge0  12839  nn0inf  12889  eqreznegel  12893  fz10  13506  fz01en  13513  fzshftral  13576  fznn0  13580  fz1ssfz0  13584  fz0sn  13588  fz0tp  13589  fz0to3un2pr  13590  fz0to4untppr  13591  fz0to5un2tp  13592  elfz0ubfz0  13593  fz0sn0fz1  13606  1fv  13608  fzo0n  13642  lbfzo0  13660  elfzonlteqm1  13702  fzo01  13708  fzo0to2pr  13711  fz01pr  13712  fzo0to3tp  13713  ico01fl0  13781  flge0nn0  13782  divfl0  13786  btwnzge0  13790  zmodfz  13855  modid  13858  zmodid2  13861  modmuladdnn0  13880  ltweuz  13926  uzenom  13929  fzennn  13933  cardfz  13935  hashgf1o  13936  f13idfv  13965  seqfn  13978  seq1  13979  seqp1  13981  exp0  14030  bcnn  14277  bcval5  14283  bcpasc  14286  4bc2eq6  14294  hashgadd  14342  hashbc  14418  fz1isolem  14426  hashge2el2dif  14445  fi1uzind  14472  s111  14580  swrdnd  14619  swrds1  14631  repswswrd  14749  cshw0  14759  s2f1o  14882  f1oun2prg  14883  rexfiuz  15314  climz  15515  climaddc1  15601  climmulc2  15603  climsubc1  15604  climsubc2  15605  climlec2  15625  sumss  15690  binomlem  15795  binom  15796  bcxmas  15801  climcndslem1  15815  arisum2  15827  explecnv  15831  geomulcvg  15842  risefall0lem  15992  bpoly1  16017  bpolydiflem  16020  bpoly2  16023  bpoly3  16024  bpoly4  16025  ef0lem  16044  efcvgfsum  16052  ege2le3  16056  eftlub  16077  efgt1p2  16082  efgt1p  16083  ruclem4  16202  ruclem6  16203  nthruc  16220  dvds0  16241  0dvds  16246  fsumdvds  16278  odd2np1lem  16310  divalglem6  16368  divalglem7  16369  divalglem8  16370  bitsfzo  16405  bitsmod  16406  0bits  16409  m1bits  16410  sadc0  16424  smup0  16449  gcd0val  16467  gcddvds  16473  gcd0id  16489  gcdid0  16490  gcdaddm  16495  gcdid  16497  bezoutlem1  16509  bezout  16513  dfgcd2  16516  lcm0val  16564  dvdslcm  16568  lcmeq0  16570  lcmgcd  16577  lcmdvds  16578  lcmftp  16606  lcmfunsnlem2  16610  dfphi2  16744  phiprmpw  16746  pc0  16825  pcdvdstr  16847  dvdsprmpweqnn  16856  pcfaclem  16869  prmreclem2  16888  prmreclem4  16890  zgz  16904  igz  16905  4sqlem19  16934  ramz  16996  1259lem1  17101  1259lem4  17104  2503lem2  17108  4001lem1  17111  4001lem3  17113  gsumws1  18765  mulg0  19006  dfod2  19494  zaddablx  19802  0cyg  19823  srgbinomlem4  20138  zringsub  21365  zring0  21368  pzriprnglem3  21393  pzriprnglem4  21394  pzriprnglem5  21395  pzriprnglem6  21396  pzriprnglem10  21400  pzriprng1ALT  21406  zndvds0  21460  ltbwe  21951  pmatcollpw3fi1  22675  iscmet3lem3  25190  vitalilem1  25509  itgcnlem  25691  dvn0  25826  dvexp3  25882  plyco  26146  0dgr  26150  0dgrb  26151  coefv0  26153  coemulc  26160  vieta1lem2  26219  vieta1  26220  elqaalem1  26227  elqaalem3  26229  aareccl  26234  aannenlem1  26236  aannenlem2  26237  aalioulem1  26240  taylfval  26266  taylplem1  26270  taylplem2  26271  taylpfval  26272  dvtaylp  26278  dvradcnv  26330  pserulm  26331  pserdvlem2  26338  abelthlem6  26346  abelthlem9  26350  logf1o2  26559  ang180lem3  26721  1cubr  26752  leibpi  26852  fsumharmonic  26922  muf  27050  0sgm  27054  1sgmprm  27110  ppiub  27115  bposlem1  27195  bposlem2  27196  lgslem2  27209  lgsfcl2  27214  lgsval2lem  27218  lgs0  27221  lgsdir2lem3  27238  lgsdirnn0  27255  lgsdinn0  27256  pntrlog2bndlem4  27491  padicabv  27541  ostth2lem2  27545  usgrexmpldifpr  29185  usgrexmplef  29186  wlkv0  29579  spthispth  29654  dfpth2  29659  uhgrwkspthlem2  29684  pthdlem2  29698  clwwlkccatlem  29918  0ewlk  30043  0wlkons1  30050  0pth  30054  0pthon  30056  wlk2v2elem2  30085  ntrl2v2e  30087  fzo0opth  32728  0dp2dp  32829  chnub  32938  cycpmrn  33100  elrgspnlem1  33193  constrextdg2  33739  zringnm  33948  qqh0  33974  qqhcn  33981  qqhucn  33982  rrh0  34005  eulerpartlemmf  34366  ballotlem2  34480  ballotlemfc0  34484  ballotlemfcc  34485  plymulx0  34538  signstf0  34559  signsvf0  34571  hgt750lemd  34639  hgt750lem  34642  0nn0m1nnn0  35100  revpfxsfxrev  35103  subfacval2  35174  cvmliftlem4  35275  cvmliftlem5  35276  fz0n  35718  bcneg1  35723  bccolsum  35726  fwddifn0  36152  fwddifnp1  36153  knoppcnlem8  36488  knoppcnlem11  36491  poimirlem24  37638  poimirlem27  37641  poimirlem28  37642  sdclem1  37737  heibor1lem  37803  heiborlem4  37808  bccl2d  41979  aks6d1c1  42104  aks6d1c2lem4  42115  0dvds0  42315  mzpnegmpt  42732  diophrw  42747  vdioph  42767  diophren  42801  irrapxlem1  42810  rmxy0  42912  monotoddzzfi  42931  zindbi  42935  rmyeq0  42942  jm2.18  42977  jm2.15nn0  42992  jm2.16nn0  42993  mpaaeu  43139  nzss  44306  hashnzfz2  44310  dvradcnv2  44336  binomcxplemnn0  44338  binomcxplemrat  44339  binomcxplemnotnn0  44345  halffl  45294  lmbr3v  45743  dvnmul  45941  stoweidlem11  46009  stoweidlem17  46015  stirlinglem7  46078  fourierdlem20  46125  etransclem25  46257  etransclem26  46258  etransclem37  46269  smfmullem4  46792  upwordnul  46878  tworepnotupword  46884  2ffzoeq  47328  fmtnorec2  47544  0evenALTV  47689  0noddALTV  47690  2exp340mod341  47734  8exp8mod9  47737  nfermltl8rev  47743  gpgusgralem  48047  1odd  48159  0even  48225  2zrngamgm  48233  altgsumbcALT  48341  blen1  48573  blen1b  48577  0dig1  48598  0dig2pr01  48599  nn0sumshdiglem1  48610  itcoval0  48651  ackval0  48669  aacllem  49790