Theorem 0z 12621

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

Syntax hints:   ∨ w3o 1085   = wceq 1536   ∈ wcel 2105  ℝcr 11151  0cc0 11152  -cneg 11490  ℕcn 12263  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-addrcl 11213  ax-rnegex 11223  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-neg 11492  df-z 12611

This theorem is referenced by:  0zd  12622  elnn0z  12623  nn0ssz  12633  znegcl  12649  zgt0ge1  12669  nnm1ge0  12683  gtndiv  12692  zeo  12701  nn0ind  12710  fnn0ind  12714  eluzaddOLD  12910  eluzsubOLD  12911  nn0uz  12917  1eluzge0  12931  nn0inf  12969  eqreznegel  12973  fz10  13581  fz01en  13588  fzshftral  13651  fznn0  13655  fz1ssfz0  13659  fz0sn  13663  fz0tp  13664  fz0to3un2pr  13665  fz0to4untppr  13666  fz0to5un2tp  13667  elfz0ubfz0  13668  fz0sn0fz1  13681  1fv  13683  fzo0n  13717  lbfzo0  13735  elfzonlteqm1  13776  fzo01  13782  fzo0to2pr  13785  fz01pr  13786  fzo0to3tp  13787  ico01fl0  13855  flge0nn0  13856  divfl0  13860  btwnzge0  13864  zmodfz  13929  modid  13932  zmodid2  13935  modmuladdnn0  13952  ltweuz  13998  uzenom  14001  fzennn  14005  cardfz  14007  hashgf1o  14008  f13idfv  14037  seqfn  14050  seq1  14051  seqp1  14053  exp0  14102  bcnn  14347  bcval5  14353  bcpasc  14356  4bc2eq6  14364  hashgadd  14412  hashbc  14488  fz1isolem  14496  hashge2el2dif  14515  fi1uzind  14542  s111  14649  swrdnd  14688  swrds1  14700  repswswrd  14818  cshw0  14828  s2f1o  14951  f1oun2prg  14952  rexfiuz  15382  climz  15581  climaddc1  15667  climmulc2  15669  climsubc1  15670  climsubc2  15671  climlec2  15691  sumss  15756  binomlem  15861  binom  15862  bcxmas  15867  climcndslem1  15881  arisum2  15893  explecnv  15897  geomulcvg  15908  risefall0lem  16058  bpoly1  16083  bpolydiflem  16086  bpoly2  16089  bpoly3  16090  bpoly4  16091  ef0lem  16110  efcvgfsum  16118  ege2le3  16122  eftlub  16141  efgt1p2  16146  efgt1p  16147  ruclem4  16266  ruclem6  16267  nthruc  16284  dvds0  16305  0dvds  16310  fsumdvds  16341  odd2np1lem  16373  divalglem6  16431  divalglem7  16432  divalglem8  16433  bitsfzo  16468  bitsmod  16469  0bits  16472  m1bits  16473  sadc0  16487  smup0  16512  gcd0val  16530  gcddvds  16536  gcd0id  16552  gcdid0  16553  gcdaddm  16558  gcdid  16560  bezoutlem1  16572  bezout  16576  dfgcd2  16579  lcm0val  16627  dvdslcm  16631  lcmeq0  16633  lcmgcd  16640  lcmdvds  16641  lcmftp  16669  lcmfunsnlem2  16673  dfphi2  16807  phiprmpw  16809  pc0  16887  pcdvdstr  16909  dvdsprmpweqnn  16918  pcfaclem  16931  prmreclem2  16950  prmreclem4  16952  zgz  16966  igz  16967  4sqlem19  16996  ramz  17058  1259lem1  17164  1259lem4  17167  2503lem2  17171  4001lem1  17174  4001lem3  17176  gsumws1  18863  mulg0  19104  dfod2  19596  zaddablx  19904  0cyg  19925  srgbinomlem4  20246  zringsub  21483  zring0  21486  pzriprnglem3  21511  pzriprnglem4  21512  pzriprnglem5  21513  pzriprnglem6  21514  pzriprnglem10  21518  pzriprng1ALT  21524  zndvds0  21586  ltbwe  22079  pmatcollpw3fi1  22809  iscmet3lem3  25337  vitalilem1  25656  itgcnlem  25839  dvn0  25974  dvexp3  26030  plyco  26294  0dgr  26298  0dgrb  26299  coefv0  26301  coemulc  26308  vieta1lem2  26367  vieta1  26368  elqaalem1  26375  elqaalem3  26377  aareccl  26382  aannenlem1  26384  aannenlem2  26385  aalioulem1  26388  taylfval  26414  taylplem1  26418  taylplem2  26419  taylpfval  26420  dvtaylp  26426  dvradcnv  26478  pserulm  26479  pserdvlem2  26486  abelthlem6  26494  abelthlem9  26498  logf1o2  26706  ang180lem3  26868  1cubr  26899  leibpi  26999  fsumharmonic  27069  muf  27197  0sgm  27201  1sgmprm  27257  ppiub  27262  bposlem1  27342  bposlem2  27343  lgslem2  27356  lgsfcl2  27361  lgsval2lem  27365  lgs0  27368  lgsdir2lem3  27385  lgsdirnn0  27402  lgsdinn0  27403  pntrlog2bndlem4  27638  padicabv  27688  ostth2lem2  27692  usgrexmpldifpr  29289  usgrexmplef  29290  wlkv0  29683  spthispth  29758  uhgrwkspthlem2  29786  pthdlem2  29800  clwwlkccatlem  30017  0ewlk  30142  0wlkons1  30149  0pth  30153  0pthon  30155  wlk2v2elem2  30184  ntrl2v2e  30186  fzo0opth  32812  0dp2dp  32875  chnub  32985  cycpmrn  33145  elrgspnlem1  33231  zringnm  33918  qqh0  33946  qqhcn  33953  qqhucn  33954  rrh0  33977  eulerpartlemmf  34356  ballotlem2  34469  ballotlemfc0  34473  ballotlemfcc  34474  plymulx0  34540  signstf0  34561  signsvf0  34573  hgt750lemd  34641  hgt750lem  34644  0nn0m1nnn0  35096  revpfxsfxrev  35099  subfacval2  35171  cvmliftlem4  35272  cvmliftlem5  35273  fz0n  35710  bcneg1  35715  bccolsum  35718  fwddifn0  36145  fwddifnp1  36146  knoppcnlem8  36482  knoppcnlem11  36485  poimirlem24  37630  poimirlem27  37633  poimirlem28  37634  sdclem1  37729  heibor1lem  37795  heiborlem4  37800  bccl2d  41972  aks6d1c1  42097  aks6d1c2lem4  42108  0dvds0  42340  mzpnegmpt  42731  diophrw  42746  vdioph  42766  diophren  42800  irrapxlem1  42809  rmxy0  42911  monotoddzzfi  42930  zindbi  42934  rmyeq0  42941  jm2.18  42976  jm2.15nn0  42991  jm2.16nn0  42992  mpaaeu  43138  nzss  44312  hashnzfz2  44316  dvradcnv2  44342  binomcxplemnn0  44344  binomcxplemrat  44345  binomcxplemnotnn0  44351  halffl  45246  lmbr3v  45700  dvnmul  45898  stoweidlem11  45966  stoweidlem17  45972  stirlinglem7  46035  fourierdlem20  46082  etransclem25  46214  etransclem26  46215  etransclem37  46226  smfmullem4  46749  upwordnul  46833  tworepnotupword  46839  2ffzoeq  47276  fmtnorec2  47467  0evenALTV  47612  0noddALTV  47613  2exp340mod341  47657  8exp8mod9  47660  nfermltl8rev  47666  gpgusgralem  47945  1odd  48014  0even  48080  2zrngamgm  48088  altgsumbcALT  48197  blen1  48433  blen1b  48437  0dig1  48458  0dig2pr01  48459  nn0sumshdiglem1  48470  itcoval0  48511  ackval0  48529  aacllem  49031