Theorem 0z 11995

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

Syntax hints:   ∨ w3o 1082   = wceq 1536   ∈ wcel 2113  ℝcr 10539  0cc0 10540  -cneg 10874  ℕcn 11641  ℤcz 11984

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-1cn 10598  ax-addrcl 10601  ax-rnegex 10611  ax-cnre 10613

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-iota 6317  df-fv 6366  df-ov 7162  df-neg 10876  df-z 11985

This theorem is referenced by:  0zd  11996  elnn0z  11997  nn0ssz  12006  znegcl  12020  zgt0ge1  12039  nnm1ge0  12053  gtndiv  12062  zeo  12071  nn0ind  12080  fnn0ind  12084  eluzadd  12276  eluzsub  12277  nn0uz  12283  1eluzge0  12295  nn0inf  12333  eqreznegel  12337  fz10  12931  fz01en  12938  fzshftral  12998  fznn0  13002  fz1ssfz0  13006  fz0sn  13010  fz0tp  13011  fz0to3un2pr  13012  fz0to4untppr  13013  elfz0ubfz0  13014  fz0sn0fz1  13027  1fv  13029  fzo0n  13062  lbfzo0  13080  elfzonlteqm1  13116  fzo01  13122  fzo0to2pr  13125  fzo0to3tp  13126  ico01fl0  13192  flge0nn0  13193  divfl0  13197  btwnzge0  13201  zmodfz  13264  modid  13267  zmodid2  13270  modmuladdnn0  13286  ltweuz  13332  uzenom  13335  fzennn  13339  cardfz  13341  hashgf1o  13342  f13idfv  13371  seqfn  13384  seq1  13385  seqp1  13387  exp0  13436  bcnn  13675  bcval5  13681  bcpasc  13684  4bc2eq6  13692  hashgadd  13741  hashbc  13814  fz1isolem  13822  hashge2el2dif  13841  fi1uzind  13858  s111  13972  swrdnd  14019  swrds1  14031  repswswrd  14149  cshw0  14159  s2f1o  14281  f1oun2prg  14282  rexfiuz  14710  climz  14909  climaddc1  14994  climmulc2  14996  climsubc1  14997  climsubc2  14998  climlec2  15018  sumss  15084  binomlem  15187  binom  15188  bcxmas  15193  climcndslem1  15207  arisum2  15219  explecnv  15223  geomulcvg  15235  risefall0lem  15383  bpoly1  15408  bpolydiflem  15411  bpoly2  15414  bpoly3  15415  bpoly4  15416  ef0lem  15435  efcvgfsum  15442  ege2le3  15446  eftlub  15465  efgt1p2  15470  efgt1p  15471  ruclem4  15590  ruclem6  15591  nthruc  15608  dvds0  15628  0dvds  15633  fsumdvds  15661  odd2np1lem  15692  divalglem6  15752  divalglem7  15753  divalglem8  15754  bitsfzo  15787  bitsmod  15788  0bits  15791  m1bits  15792  sadc0  15806  smup0  15831  gcd0val  15849  gcddvds  15855  gcd0id  15870  gcdid0  15871  gcdaddm  15876  gcdid  15878  bezoutlem1  15890  bezout  15894  dfgcd2  15897  lcm0val  15941  dvdslcm  15945  lcmeq0  15947  lcmgcd  15954  lcmdvds  15955  lcmftp  15983  lcmfunsnlem2  15987  dfphi2  16114  phiprmpw  16116  pc0  16194  pcdvdstr  16215  dvdsprmpweqnn  16224  pcfaclem  16237  prmreclem2  16256  prmreclem4  16258  zgz  16272  igz  16273  4sqlem19  16302  ramz  16364  1259lem1  16467  1259lem4  16470  2503lem2  16474  4001lem1  16477  4001lem3  16479  gsumws1  18005  mulg0  18234  dfod2  18694  zaddablx  18995  0cyg  19016  srgbinomlem4  19296  ltbwe  20256  zring0  20630  zndvds0  20700  pmatcollpw3fi1  21399  iscmet3lem3  23896  vitalilem1  24212  itgcnlem  24393  dvn0  24524  dvexp3  24578  plyco  24834  0dgr  24838  0dgrb  24839  coefv0  24841  coemulc  24848  vieta1lem2  24903  vieta1  24904  elqaalem1  24911  elqaalem3  24913  aareccl  24918  aannenlem1  24920  aannenlem2  24921  aalioulem1  24924  taylfval  24950  taylplem1  24954  taylplem2  24955  taylpfval  24956  dvtaylp  24961  dvradcnv  25012  pserulm  25013  pserdvlem2  25019  abelthlem6  25027  abelthlem9  25031  logf1o2  25236  ang180lem3  25392  1cubr  25423  leibpi  25523  fsumharmonic  25592  muf  25720  0sgm  25724  1sgmprm  25778  ppiub  25783  bposlem1  25863  bposlem2  25864  lgslem2  25877  lgsfcl2  25882  lgsval2lem  25886  lgs0  25889  lgsdir2lem3  25906  lgsdirnn0  25923  lgsdinn0  25924  pntrlog2bndlem4  26159  padicabv  26209  ostth2lem2  26213  usgrexmpldifpr  27043  usgrexmplef  27044  wlkv0  27435  spthispth  27510  uhgrwkspthlem2  27538  pthdlem2  27552  clwwlkccatlem  27770  0ewlk  27896  0wlkons1  27903  0pth  27907  0pthon  27909  wlk2v2elem2  27938  ntrl2v2e  27940  0dp2dp  30589  cycpmrn  30789  zringnm  31205  qqh0  31229  qqhcn  31236  qqhucn  31237  rrh0  31260  eulerpartlemmf  31637  ballotlem2  31750  ballotlemfc0  31754  ballotlemfcc  31755  plymulx0  31821  signstf0  31842  signsvf0  31854  hgt750lemd  31923  hgt750lem  31926  0nn0m1nnn0  32355  revpfxsfxrev  32366  subfacval2  32438  cvmliftlem4  32539  cvmliftlem5  32540  fz0n  32966  bcneg1  32972  bccolsum  32975  fwddifn0  33629  fwddifnp1  33630  knoppcnlem8  33843  knoppcnlem11  33846  poimirlem24  34920  poimirlem27  34923  poimirlem28  34924  sdclem1  35022  heibor1lem  35091  heiborlem4  35096  mzpnegmpt  39347  diophrw  39362  vdioph  39382  diophren  39416  irrapxlem1  39425  rmxy0  39526  monotoddzzfi  39545  zindbi  39549  rmyeq0  39556  jm2.18  39591  jm2.15nn0  39606  jm2.16nn0  39607  mpaaeu  39756  nzss  40655  hashnzfz2  40659  dvradcnv2  40685  binomcxplemnn0  40687  binomcxplemrat  40688  binomcxplemnotnn0  40694  halffl  41569  lmbr3v  42032  dvnmul  42234  stoweidlem11  42303  stoweidlem17  42309  stirlinglem7  42372  fourierdlem20  42419  etransclem25  42551  etransclem26  42552  etransclem37  42563  smfmullem4  43076  2ffzoeq  43535  fmtnorec2  43712  0evenALTV  43860  0noddALTV  43861  2exp340mod341  43905  8exp8mod9  43908  nfermltl8rev  43914  1odd  44085  0even  44209  2zrngamgm  44217  altgsumbcALT  44408  blen1  44651  blen1b  44655  0dig1  44676  0dig2pr01  44677  nn0sumshdiglem1  44688  aacllem  44909