Theorem 0z 12630

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 11238	. 2 ⊢ 0 ∈ ℝ
2		eqid 2762	. . 3 ⊢ 0 = 0
3	2	3mix1i 1352	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12621	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 724	1 ⊢ 0 ∈ ℤ

This proof depends on syntax axioms:   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145  ℝcr 11127  0cc0 11128  -cneg 11470  ℕcn 12261  ℤcz 12619

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-1cn 11186  ax-addrcl 11189  ax-rnegex 11199  ax-cnre 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-neg 11472  df-z 12620

This theorem is used by:  0zd  12631  elnn0z  12632  nn0ssz  12642  znegcl  12657  zgt0ge1  12678  0nn0m1nnn0  12679  nnm1ge0  12693  gtndiv  12702  zeo  12711  nn0ind  12720  fnn0ind  12724  nn0uz  12929  1eluzge0  12933  nn0inf  12983  eqreznegel  12987  fz10  13603  fz00m1  13604  fz01en  13611  fzshftral  13674  fznn0  13678  fz1ssfz0  13682  fz0sn  13686  fz0tp  13687  fz0to3un2pr  13688  fz0to4untppr  13689  fz0to5un2tp  13690  elfz0ubfz0  13691  fz0sn0fz1  13704  1fv  13706  fzo0n  13741  lbfzo0  13759  elfzonlteqm1  13801  fzo01  13807  fzo0to2pr  13810  fz01pr  13811  fzo0to3tp  13812  ico01fl0  13884  flge0nn0  13885  divfl0  13889  btwnzge0  13893  zmodfz  13958  modid  13961  zmodid2  13964  modmuladdnn0  13983  ltweuz  14029  uzenom  14032  fzennn  14036  cardfz  14038  hashgf1o  14039  f13idfv  14068  seqfn  14081  seq1  14082  seqp1  14084  exp0  14133  bcnn  14380  bcval5  14386  bcpasc  14389  4bc2eq6  14397  hashgadd  14445  hashbc  14522  fz1isolem  14530  hashge2el2dif  14549  fi1uzind  14576  s111  14687  swrdnd  14728  swrds1  14740  revpfxsfxrev  14841  repswswrd  14859  cshw0  14869  s2f1o  14991  f1oun2prg  14992  rexfiuz  15439  climz  15640  climaddc1  15726  climmulc2  15728  climsubc1  15729  climsubc2  15730  climlec2  15750  sumss  15814  binomlem  15922  binom  15923  bcxmas  15928  climcndslem1  15942  arisum2  15954  explecnv  15958  geomulcvg  15969  bpoly1  16143  bpolydiflem  16146  bpoly2  16149  bpoly3  16150  bpoly4  16151  ef0lem  16170  efcvgfsum  16178  ege2le3  16182  eftlub  16203  efgt1p2  16208  efgt1p  16209  ruclem4  16328  ruclem6  16329  nthruc  16346  dvds0  16367  0dvds  16372  fsumdvds  16404  odd2np1lem  16436  divalglem6  16494  divalglem7  16495  divalglem8  16496  bitsfzo  16531  bitsmod  16532  0bits  16535  m1bits  16536  sadc0  16550  smup0  16575  gcd0val  16593  gcddvds  16599  gcd0id  16615  gcdid0  16616  gcdaddm  16621  gcdid  16623  bezoutlem1  16635  bezout  16639  dfgcd2  16642  lcm0val  16690  dvdslcm  16694  lcmeq0  16696  lcmgcd  16703  lcmdvds  16704  lcmftp  16732  lcmfunsnlem2  16736  dfphi2  16871  phiprmpw  16873  pc0  16952  pcdvdstr  16974  dvdsprmpweqnn  16983  pcfaclem  16996  prmreclem2  17015  prmreclem4  17017  zgz  17031  igz  17032  4sqlem19  17061  ramz  17123  1259lem1  17229  1259lem4  17232  2503lem2  17236  4001lem1  17239  4001lem3  17241  chnub  18716  gsumws1  18953  mulg0  19203  dfod2  19697  zaddablx  20005  0cyg  20026  srgbinomlem4  20374  zringsub  21674  zring0  21677  pzriprnglem3  21702  pzriprnglem4  21703  pzriprnglem5  21704  pzriprnglem6  21705  pzriprnglem10  21709  pzriprng1ALT  21715  zndvds0  21769  ltbwe  22266  pmatcollpw3fi1  23019  iscmet3lem3  25524  vitalilem1  25842  itgcnlem  26024  dvn0  26158  dvexp3  26212  plyco  26474  0dgr  26478  0dgrb  26479  coefv0  26481  coemulc  26488  plyn0mulidp  26518  vieta1lem2  26550  vieta1  26551  elqaalem1  26558  elqaalem3  26560  0aa  26565  aareccl  26569  aannenlem1  26571  aannenlem2  26572  aalioulem1  26575  taylfval  26602  taylplem1  26606  taylplem2  26607  taylpfval  26608  dvtaylp  26613  dvradcnv  26664  pserulm  26665  pserdvlem2  26671  abelthlem6  26679  abelthlem9  26683  logf1o2  26895  ang180lem3  27056  1cubr  27087  leibpi  27187  fsumharmonic  27256  muf  27384  0sgm  27388  1sgmprm  27443  ppiub  27448  bposlem1  27528  bposlem2  27529  lgslem2  27542  lgsfcl2  27547  lgsval2lem  27551  lgs0  27554  lgsdir2lem3  27571  lgsdirnn0  27588  lgsdinn0  27589  pntrlog2bndlem4  27824  padicabv  27874  ostth2lem2  27878  usgrexmpldifpr  29726  usgrexmplef  29727  wlkv0  30117  spthispth  30196  dfpth2  30201  uhgrwkspthlem2  30227  pthdlem2  30241  clwwlkccatlem  30467  0ewlk  30592  0wlkons1  30599  0pth  30603  0pthon  30605  wlk2v2elem2  30644  ntrl2v2e  30646  fzo0opth  33282  0dp2dp  33362  cycpmrn  33591  elrgspnlem1  33690  constrextdg2  34267  zringnm  34476  qqh0  34502  qqhcn  34509  qqhucn  34510  rrh0  34533  eulerpartlemmf  34894  ballotlem2  35008  ballotlemfc0  35012  ballotlemfcc  35013  signstf0  35084  signsvf0  35096  hgt750lemd  35164  hgt750lem  35167  subfacval2  35774  cvmliftlem4  35875  cvmliftlem5  35876  fz0n  36318  bcneg1  36323  bccolsum  36326  fwddifn0  36752  fwddifnp1  36753  knoppcnlem8  37205  knoppcnlem11  37208  poimirlem24  38401  poimirlem27  38404  poimirlem28  38405  sdclem1  38501  heibor1lem  38567  heiborlem4  38572  bccl2d  42865  aks6d1c1  42990  aks6d1c2lem4  43001  0dvds0  43210  mzpnegmpt  43597  diophrw  43612  vdioph  43632  diophren  43662  irrapxlem1  43671  rmxy0  43772  monotoddzzfi  43791  zindbi  43795  rmyeq0  43802  jm2.18  43837  jm2.15nn0  43852  jm2.16nn0  43853  mpaaeu  43999  nzss  45149  hashnzfz2  45153  dvradcnv2  45179  binomcxplemnn0  45181  binomcxplemrat  45182  binomcxplemnotnn0  45188  halffl  46137  lmbr3v  46581  dvnmul  46779  stoweidlem11  46847  stoweidlem17  46853  stirlinglem7  46916  fourierdlem20  46963  etransclem25  47095  etransclem26  47096  etransclem37  47107  smfmullem4  47630  chnsubseqwl  47715  2ffzoeq  48224  fmtnorec2  48454  0evenALTV  48612  0noddALTV  48613  2exp340mod341  48657  8exp8mod9  48660  nfermltl8rev  48666  gpgusgralem  48980  1odd  49094  0even  49160  2zrngamgm  49168  altgsumbcALT  49291  blen1  49522  blen1b  49526  0dig1  49547  0dig2pr01  49548  nn0sumshdiglem1  49559  itcoval0  49600  ackval0  49618  aacllem  50780