Theorem 0z 12489

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

Syntax hints:   ∨ w3o 1085   = wceq 1541   ∈ wcel 2113  ℝcr 11015  0cc0 11016  -cneg 11355  ℕcn 12135  ℤcz 12478

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 2115  ax-9 2123  ax-ext 2705  ax-1cn 11074  ax-addrcl 11077  ax-rnegex 11087  ax-cnre 11089

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 2712  df-cleq 2725  df-clel 2808  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-neg 11357  df-z 12479

This theorem is referenced by:  0zd  12490  elnn0z  12491  nn0ssz  12501  znegcl  12517  zgt0ge1  12537  nnm1ge0  12551  gtndiv  12560  zeo  12569  nn0ind  12578  fnn0ind  12582  eluzaddOLD  12777  eluzsubOLD  12778  nn0uz  12784  1eluzge0  12788  nn0inf  12838  eqreznegel  12842  fz10  13455  fz01en  13462  fzshftral  13525  fznn0  13529  fz1ssfz0  13533  fz0sn  13537  fz0tp  13538  fz0to3un2pr  13539  fz0to4untppr  13540  fz0to5un2tp  13541  elfz0ubfz0  13542  fz0sn0fz1  13555  1fv  13557  fzo0n  13591  lbfzo0  13609  elfzonlteqm1  13651  fzo01  13657  fzo0to2pr  13660  fz01pr  13661  fzo0to3tp  13662  ico01fl0  13733  flge0nn0  13734  divfl0  13738  btwnzge0  13742  zmodfz  13807  modid  13810  zmodid2  13813  modmuladdnn0  13832  ltweuz  13878  uzenom  13881  fzennn  13885  cardfz  13887  hashgf1o  13888  f13idfv  13917  seqfn  13930  seq1  13931  seqp1  13933  exp0  13982  bcnn  14229  bcval5  14235  bcpasc  14238  4bc2eq6  14246  hashgadd  14294  hashbc  14370  fz1isolem  14378  hashge2el2dif  14397  fi1uzind  14424  s111  14533  swrdnd  14572  swrds1  14584  repswswrd  14701  cshw0  14711  s2f1o  14833  f1oun2prg  14834  rexfiuz  15265  climz  15466  climaddc1  15552  climmulc2  15554  climsubc1  15555  climsubc2  15556  climlec2  15576  sumss  15641  binomlem  15746  binom  15747  bcxmas  15752  climcndslem1  15766  arisum2  15778  explecnv  15782  geomulcvg  15793  risefall0lem  15943  bpoly1  15968  bpolydiflem  15971  bpoly2  15974  bpoly3  15975  bpoly4  15976  ef0lem  15995  efcvgfsum  16003  ege2le3  16007  eftlub  16028  efgt1p2  16033  efgt1p  16034  ruclem4  16153  ruclem6  16154  nthruc  16171  dvds0  16192  0dvds  16197  fsumdvds  16229  odd2np1lem  16261  divalglem6  16319  divalglem7  16320  divalglem8  16321  bitsfzo  16356  bitsmod  16357  0bits  16360  m1bits  16361  sadc0  16375  smup0  16400  gcd0val  16418  gcddvds  16424  gcd0id  16440  gcdid0  16441  gcdaddm  16446  gcdid  16448  bezoutlem1  16460  bezout  16464  dfgcd2  16467  lcm0val  16515  dvdslcm  16519  lcmeq0  16521  lcmgcd  16528  lcmdvds  16529  lcmftp  16557  lcmfunsnlem2  16561  dfphi2  16695  phiprmpw  16697  pc0  16776  pcdvdstr  16798  dvdsprmpweqnn  16807  pcfaclem  16820  prmreclem2  16839  prmreclem4  16841  zgz  16855  igz  16856  4sqlem19  16885  ramz  16947  1259lem1  17052  1259lem4  17055  2503lem2  17059  4001lem1  17062  4001lem3  17064  chnub  18538  gsumws1  18756  mulg0  18997  dfod2  19486  zaddablx  19794  0cyg  19815  srgbinomlem4  20157  zringsub  21402  zring0  21405  pzriprnglem3  21430  pzriprnglem4  21431  pzriprnglem5  21432  pzriprnglem6  21433  pzriprnglem10  21437  pzriprng1ALT  21443  zndvds0  21497  ltbwe  21989  pmatcollpw3fi1  22713  iscmet3lem3  25227  vitalilem1  25546  itgcnlem  25728  dvn0  25863  dvexp3  25919  plyco  26183  0dgr  26187  0dgrb  26188  coefv0  26190  coemulc  26197  vieta1lem2  26256  vieta1  26257  elqaalem1  26264  elqaalem3  26266  aareccl  26271  aannenlem1  26273  aannenlem2  26274  aalioulem1  26277  taylfval  26303  taylplem1  26307  taylplem2  26308  taylpfval  26309  dvtaylp  26315  dvradcnv  26367  pserulm  26368  pserdvlem2  26375  abelthlem6  26383  abelthlem9  26387  logf1o2  26596  ang180lem3  26758  1cubr  26789  leibpi  26889  fsumharmonic  26959  muf  27087  0sgm  27091  1sgmprm  27147  ppiub  27152  bposlem1  27232  bposlem2  27233  lgslem2  27246  lgsfcl2  27251  lgsval2lem  27255  lgs0  27258  lgsdir2lem3  27275  lgsdirnn0  27292  lgsdinn0  27293  pntrlog2bndlem4  27528  padicabv  27578  ostth2lem2  27582  usgrexmpldifpr  29247  usgrexmplef  29248  wlkv0  29639  spthispth  29713  dfpth2  29718  uhgrwkspthlem2  29743  pthdlem2  29757  clwwlkccatlem  29980  0ewlk  30105  0wlkons1  30112  0pth  30116  0pthon  30118  wlk2v2elem2  30147  ntrl2v2e  30149  fzo0opth  32796  0dp2dp  32900  cycpmrn  33123  elrgspnlem1  33220  constrextdg2  33773  zringnm  33982  qqh0  34008  qqhcn  34015  qqhucn  34016  rrh0  34039  eulerpartlemmf  34399  ballotlem2  34513  ballotlemfc0  34517  ballotlemfcc  34518  plymulx0  34571  signstf0  34592  signsvf0  34604  hgt750lemd  34672  hgt750lem  34675  0nn0m1nnn0  35168  revpfxsfxrev  35171  subfacval2  35242  cvmliftlem4  35343  cvmliftlem5  35344  fz0n  35786  bcneg1  35791  bccolsum  35794  fwddifn0  36219  fwddifnp1  36220  knoppcnlem8  36555  knoppcnlem11  36558  poimirlem24  37694  poimirlem27  37697  poimirlem28  37698  sdclem1  37793  heibor1lem  37859  heiborlem4  37864  bccl2d  42094  aks6d1c1  42219  aks6d1c2lem4  42230  0dvds0  42435  mzpnegmpt  42851  diophrw  42866  vdioph  42886  diophren  42920  irrapxlem1  42929  rmxy0  43030  monotoddzzfi  43049  zindbi  43053  rmyeq0  43060  jm2.18  43095  jm2.15nn0  43110  jm2.16nn0  43111  mpaaeu  43257  nzss  44424  hashnzfz2  44428  dvradcnv2  44454  binomcxplemnn0  44456  binomcxplemrat  44457  binomcxplemnotnn0  44463  halffl  45411  lmbr3v  45857  dvnmul  46055  stoweidlem11  46123  stoweidlem17  46129  stirlinglem7  46192  fourierdlem20  46239  etransclem25  46371  etransclem26  46372  etransclem37  46383  smfmullem4  46906  chnsubseqwl  46991  2ffzoeq  47441  fmtnorec2  47657  0evenALTV  47802  0noddALTV  47803  2exp340mod341  47847  8exp8mod9  47850  nfermltl8rev  47856  gpgusgralem  48170  1odd  48285  0even  48351  2zrngamgm  48359  altgsumbcALT  48467  blen1  48699  blen1b  48703  0dig1  48724  0dig2pr01  48725  nn0sumshdiglem1  48736  itcoval0  48777  ackval0  48795  aacllem  49916