Theorem 0z 11991

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 10642	. 2 ⊢ 0 ∈ ℝ
2		eqid 2821	. . 3 ⊢ 0 = 0
3	2	3mix1i 1329	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 11982	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 709	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1082   = wceq 1533   ∈ wcel 2110  ℝcr 10535  0cc0 10536  -cneg 10870  ℕcn 11637  ℤcz 11980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-1cn 10594  ax-addrcl 10597  ax-rnegex 10607  ax-cnre 10609

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-iota 6313  df-fv 6362  df-ov 7158  df-neg 10872  df-z 11981

This theorem is referenced by:  0zd  11992  elnn0z  11993  nn0ssz  12002  znegcl  12016  zgt0ge1  12035  nnm1ge0  12049  gtndiv  12058  zeo  12067  nn0ind  12076  fnn0ind  12080  eluzadd  12272  eluzsub  12273  nn0uz  12279  1eluzge0  12291  nn0inf  12329  eqreznegel  12333  fz10  12927  fz01en  12934  fzshftral  12994  fznn0  12998  fz1ssfz0  13002  fz0sn  13006  fz0tp  13007  fz0to3un2pr  13008  fz0to4untppr  13009  elfz0ubfz0  13010  fz0sn0fz1  13023  1fv  13025  fzo0n  13058  lbfzo0  13076  elfzonlteqm1  13112  fzo01  13118  fzo0to2pr  13121  fzo0to3tp  13122  ico01fl0  13188  flge0nn0  13189  divfl0  13193  btwnzge0  13197  zmodfz  13260  modid  13263  zmodid2  13266  modmuladdnn0  13282  ltweuz  13328  uzenom  13331  fzennn  13335  cardfz  13337  hashgf1o  13338  f13idfv  13367  seqfn  13380  seq1  13381  seqp1  13383  exp0  13432  bcnn  13671  bcval5  13677  bcpasc  13680  4bc2eq6  13688  hashgadd  13737  hashbc  13810  fz1isolem  13818  hashge2el2dif  13837  fi1uzind  13854  s111  13968  swrdnd  14015  swrds1  14027  repswswrd  14145  cshw0  14155  s2f1o  14277  f1oun2prg  14278  rexfiuz  14706  climz  14905  climaddc1  14990  climmulc2  14992  climsubc1  14993  climsubc2  14994  climlec2  15014  sumss  15080  binomlem  15183  binom  15184  bcxmas  15189  climcndslem1  15203  arisum2  15215  explecnv  15219  geomulcvg  15231  risefall0lem  15379  bpoly1  15404  bpolydiflem  15407  bpoly2  15410  bpoly3  15411  bpoly4  15412  ef0lem  15431  efcvgfsum  15438  ege2le3  15442  eftlub  15461  efgt1p2  15466  efgt1p  15467  ruclem4  15586  ruclem6  15587  nthruc  15604  dvds0  15624  0dvds  15629  fsumdvds  15657  odd2np1lem  15688  divalglem6  15748  divalglem7  15749  divalglem8  15750  bitsfzo  15783  bitsmod  15784  0bits  15787  m1bits  15788  sadc0  15802  smup0  15827  gcd0val  15845  gcddvds  15851  gcd0id  15866  gcdid0  15867  gcdaddm  15872  gcdid  15874  bezoutlem1  15886  bezout  15890  dfgcd2  15893  lcm0val  15937  dvdslcm  15941  lcmeq0  15943  lcmgcd  15950  lcmdvds  15951  lcmftp  15979  lcmfunsnlem2  15983  dfphi2  16110  phiprmpw  16112  pc0  16190  pcdvdstr  16211  dvdsprmpweqnn  16220  pcfaclem  16233  prmreclem2  16252  prmreclem4  16254  zgz  16268  igz  16269  4sqlem19  16298  ramz  16360  1259lem1  16463  1259lem4  16466  2503lem2  16470  4001lem1  16473  4001lem3  16475  gsumws1  18001  mulg0  18230  dfod2  18690  zaddablx  18991  0cyg  19012  srgbinomlem4  19292  ltbwe  20252  zring0  20626  zndvds0  20696  pmatcollpw3fi1  21395  iscmet3lem3  23892  vitalilem1  24208  itgcnlem  24389  dvn0  24520  dvexp3  24574  plyco  24830  0dgr  24834  0dgrb  24835  coefv0  24837  coemulc  24844  vieta1lem2  24899  vieta1  24900  elqaalem1  24907  elqaalem3  24909  aareccl  24914  aannenlem1  24916  aannenlem2  24917  aalioulem1  24920  taylfval  24946  taylplem1  24950  taylplem2  24951  taylpfval  24952  dvtaylp  24957  dvradcnv  25008  pserulm  25009  pserdvlem2  25015  abelthlem6  25023  abelthlem9  25027  logf1o2  25232  ang180lem3  25388  1cubr  25419  leibpi  25519  fsumharmonic  25588  muf  25716  0sgm  25720  1sgmprm  25774  ppiub  25779  bposlem1  25859  bposlem2  25860  lgslem2  25873  lgsfcl2  25878  lgsval2lem  25882  lgs0  25885  lgsdir2lem3  25902  lgsdirnn0  25919  lgsdinn0  25920  pntrlog2bndlem4  26155  padicabv  26205  ostth2lem2  26209  usgrexmpldifpr  27039  usgrexmplef  27040  wlkv0  27431  spthispth  27506  uhgrwkspthlem2  27534  pthdlem2  27548  clwwlkccatlem  27766  0ewlk  27892  0wlkons1  27899  0pth  27903  0pthon  27905  wlk2v2elem2  27934  ntrl2v2e  27936  0dp2dp  30585  cycpmrn  30785  zringnm  31201  qqh0  31225  qqhcn  31232  qqhucn  31233  rrh0  31256  eulerpartlemmf  31633  ballotlem2  31746  ballotlemfc0  31750  ballotlemfcc  31751  plymulx0  31817  signstf0  31838  signsvf0  31850  hgt750lemd  31919  hgt750lem  31922  0nn0m1nnn0  32351  revpfxsfxrev  32362  subfacval2  32434  cvmliftlem4  32535  cvmliftlem5  32536  fz0n  32962  bcneg1  32968  bccolsum  32971  fwddifn0  33625  fwddifnp1  33626  knoppcnlem8  33839  knoppcnlem11  33842  poimirlem24  34915  poimirlem27  34918  poimirlem28  34919  sdclem1  35017  heibor1lem  35086  heiborlem4  35091  mzpnegmpt  39339  diophrw  39354  vdioph  39374  diophren  39408  irrapxlem1  39417  rmxy0  39518  monotoddzzfi  39537  zindbi  39541  rmyeq0  39548  jm2.18  39583  jm2.15nn0  39598  jm2.16nn0  39599  mpaaeu  39748  nzss  40647  hashnzfz2  40651  dvradcnv2  40677  binomcxplemnn0  40679  binomcxplemrat  40680  binomcxplemnotnn0  40686  halffl  41561  lmbr3v  42024  dvnmul  42226  stoweidlem11  42295  stoweidlem17  42301  stirlinglem7  42364  fourierdlem20  42411  etransclem25  42543  etransclem26  42544  etransclem37  42555  smfmullem4  43068  2ffzoeq  43527  fmtnorec2  43704  0evenALTV  43852  0noddALTV  43853  2exp340mod341  43897  8exp8mod9  43900  nfermltl8rev  43906  1odd  44077  0even  44201  2zrngamgm  44209  altgsumbcALT  44400  blen1  44643  blen1b  44647  0dig1  44668  0dig2pr01  44669  nn0sumshdiglem1  44680  aacllem  44901