Theorem 0z 12500

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

Syntax hints:   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  ℝcr 11027  0cc0 11028  -cneg 11366  ℕcn 12146  ℤcz 12489

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 11086  ax-addrcl 11089  ax-rnegex 11099  ax-cnre 11101

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-neg 11368  df-z 12490

This theorem is referenced by:  0zd  12501  elnn0z  12502  nn0ssz  12512  znegcl  12528  zgt0ge1  12548  nnm1ge0  12562  gtndiv  12571  zeo  12580  nn0ind  12589  fnn0ind  12593  eluzaddOLD  12788  eluzsubOLD  12789  nn0uz  12795  1eluzge0  12799  nn0inf  12849  eqreznegel  12853  fz10  13466  fz01en  13473  fzshftral  13536  fznn0  13540  fz1ssfz0  13544  fz0sn  13548  fz0tp  13549  fz0to3un2pr  13550  fz0to4untppr  13551  fz0to5un2tp  13552  elfz0ubfz0  13553  fz0sn0fz1  13566  1fv  13568  fzo0n  13602  lbfzo0  13620  elfzonlteqm1  13662  fzo01  13668  fzo0to2pr  13671  fz01pr  13672  fzo0to3tp  13673  ico01fl0  13741  flge0nn0  13742  divfl0  13746  btwnzge0  13750  zmodfz  13815  modid  13818  zmodid2  13821  modmuladdnn0  13840  ltweuz  13886  uzenom  13889  fzennn  13893  cardfz  13895  hashgf1o  13896  f13idfv  13925  seqfn  13938  seq1  13939  seqp1  13941  exp0  13990  bcnn  14237  bcval5  14243  bcpasc  14246  4bc2eq6  14254  hashgadd  14302  hashbc  14378  fz1isolem  14386  hashge2el2dif  14405  fi1uzind  14432  s111  14540  swrdnd  14579  swrds1  14591  repswswrd  14708  cshw0  14718  s2f1o  14841  f1oun2prg  14842  rexfiuz  15273  climz  15474  climaddc1  15560  climmulc2  15562  climsubc1  15563  climsubc2  15564  climlec2  15584  sumss  15649  binomlem  15754  binom  15755  bcxmas  15760  climcndslem1  15774  arisum2  15786  explecnv  15790  geomulcvg  15801  risefall0lem  15951  bpoly1  15976  bpolydiflem  15979  bpoly2  15982  bpoly3  15983  bpoly4  15984  ef0lem  16003  efcvgfsum  16011  ege2le3  16015  eftlub  16036  efgt1p2  16041  efgt1p  16042  ruclem4  16161  ruclem6  16162  nthruc  16179  dvds0  16200  0dvds  16205  fsumdvds  16237  odd2np1lem  16269  divalglem6  16327  divalglem7  16328  divalglem8  16329  bitsfzo  16364  bitsmod  16365  0bits  16368  m1bits  16369  sadc0  16383  smup0  16408  gcd0val  16426  gcddvds  16432  gcd0id  16448  gcdid0  16449  gcdaddm  16454  gcdid  16456  bezoutlem1  16468  bezout  16472  dfgcd2  16475  lcm0val  16523  dvdslcm  16527  lcmeq0  16529  lcmgcd  16536  lcmdvds  16537  lcmftp  16565  lcmfunsnlem2  16569  dfphi2  16703  phiprmpw  16705  pc0  16784  pcdvdstr  16806  dvdsprmpweqnn  16815  pcfaclem  16828  prmreclem2  16847  prmreclem4  16849  zgz  16863  igz  16864  4sqlem19  16893  ramz  16955  1259lem1  17060  1259lem4  17063  2503lem2  17067  4001lem1  17070  4001lem3  17072  gsumws1  18730  mulg0  18971  dfod2  19461  zaddablx  19769  0cyg  19790  srgbinomlem4  20132  zringsub  21380  zring0  21383  pzriprnglem3  21408  pzriprnglem4  21409  pzriprnglem5  21410  pzriprnglem6  21411  pzriprnglem10  21415  pzriprng1ALT  21421  zndvds0  21475  ltbwe  21967  pmatcollpw3fi1  22691  iscmet3lem3  25206  vitalilem1  25525  itgcnlem  25707  dvn0  25842  dvexp3  25898  plyco  26162  0dgr  26166  0dgrb  26167  coefv0  26169  coemulc  26176  vieta1lem2  26235  vieta1  26236  elqaalem1  26243  elqaalem3  26245  aareccl  26250  aannenlem1  26252  aannenlem2  26253  aalioulem1  26256  taylfval  26282  taylplem1  26286  taylplem2  26287  taylpfval  26288  dvtaylp  26294  dvradcnv  26346  pserulm  26347  pserdvlem2  26354  abelthlem6  26362  abelthlem9  26366  logf1o2  26575  ang180lem3  26737  1cubr  26768  leibpi  26868  fsumharmonic  26938  muf  27066  0sgm  27070  1sgmprm  27126  ppiub  27131  bposlem1  27211  bposlem2  27212  lgslem2  27225  lgsfcl2  27230  lgsval2lem  27234  lgs0  27237  lgsdir2lem3  27254  lgsdirnn0  27271  lgsdinn0  27272  pntrlog2bndlem4  27507  padicabv  27557  ostth2lem2  27561  usgrexmpldifpr  29221  usgrexmplef  29222  wlkv0  29613  spthispth  29687  dfpth2  29692  uhgrwkspthlem2  29717  pthdlem2  29731  clwwlkccatlem  29951  0ewlk  30076  0wlkons1  30083  0pth  30087  0pthon  30089  wlk2v2elem2  30118  ntrl2v2e  30120  fzo0opth  32761  0dp2dp  32862  chnub  32967  cycpmrn  33098  elrgspnlem1  33192  constrextdg2  33715  zringnm  33924  qqh0  33950  qqhcn  33957  qqhucn  33958  rrh0  33981  eulerpartlemmf  34342  ballotlem2  34456  ballotlemfc0  34460  ballotlemfcc  34461  plymulx0  34514  signstf0  34535  signsvf0  34547  hgt750lemd  34615  hgt750lem  34618  0nn0m1nnn0  35085  revpfxsfxrev  35088  subfacval2  35159  cvmliftlem4  35260  cvmliftlem5  35261  fz0n  35703  bcneg1  35708  bccolsum  35711  fwddifn0  36137  fwddifnp1  36138  knoppcnlem8  36473  knoppcnlem11  36476  poimirlem24  37623  poimirlem27  37626  poimirlem28  37627  sdclem1  37722  heibor1lem  37788  heiborlem4  37793  bccl2d  41964  aks6d1c1  42089  aks6d1c2lem4  42100  0dvds0  42300  mzpnegmpt  42717  diophrw  42732  vdioph  42752  diophren  42786  irrapxlem1  42795  rmxy0  42896  monotoddzzfi  42915  zindbi  42919  rmyeq0  42926  jm2.18  42961  jm2.15nn0  42976  jm2.16nn0  42977  mpaaeu  43123  nzss  44290  hashnzfz2  44294  dvradcnv2  44320  binomcxplemnn0  44322  binomcxplemrat  44323  binomcxplemnotnn0  44329  halffl  45278  lmbr3v  45727  dvnmul  45925  stoweidlem11  45993  stoweidlem17  45999  stirlinglem7  46062  fourierdlem20  46109  etransclem25  46241  etransclem26  46242  etransclem37  46253  smfmullem4  46776  upwordnul  46862  tworepnotupword  46868  2ffzoeq  47312  fmtnorec2  47528  0evenALTV  47673  0noddALTV  47674  2exp340mod341  47718  8exp8mod9  47721  nfermltl8rev  47727  gpgusgralem  48041  1odd  48156  0even  48222  2zrngamgm  48230  altgsumbcALT  48338  blen1  48570  blen1b  48574  0dig1  48595  0dig2pr01  48596  nn0sumshdiglem1  48607  itcoval0  48648  ackval0  48666  aacllem  49787