Theorem 0z 12431

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

Syntax hints:   ∨ w3o 1085   = wceq 1540   ∈ wcel 2105  ℝcr 10971  0cc0 10972  -cneg 11307  ℕcn 12074  ℤcz 12420

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-1cn 11030  ax-addrcl 11033  ax-rnegex 11043  ax-cnre 11045

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-iota 6431  df-fv 6487  df-ov 7340  df-neg 11309  df-z 12421

This theorem is referenced by:  0zd  12432  elnn0z  12433  nn0ssz  12442  znegcl  12456  zgt0ge1  12475  nnm1ge0  12489  gtndiv  12498  zeo  12507  nn0ind  12516  fnn0ind  12520  eluzadd  12714  eluzsub  12715  nn0uz  12721  1eluzge0  12733  nn0inf  12771  eqreznegel  12775  fz10  13378  fz01en  13385  fzshftral  13445  fznn0  13449  fz1ssfz0  13453  fz0sn  13457  fz0tp  13458  fz0to3un2pr  13459  fz0to4untppr  13460  elfz0ubfz0  13461  fz0sn0fz1  13474  1fv  13476  fzo0n  13510  lbfzo0  13528  elfzonlteqm1  13564  fzo01  13570  fzo0to2pr  13573  fzo0to3tp  13574  ico01fl0  13640  flge0nn0  13641  divfl0  13645  btwnzge0  13649  zmodfz  13714  modid  13717  zmodid2  13720  modmuladdnn0  13736  ltweuz  13782  uzenom  13785  fzennn  13789  cardfz  13791  hashgf1o  13792  f13idfv  13821  seqfn  13834  seq1  13835  seqp1  13837  exp0  13887  bcnn  14127  bcval5  14133  bcpasc  14136  4bc2eq6  14144  hashgadd  14192  hashbc  14265  fz1isolem  14275  hashge2el2dif  14294  fi1uzind  14311  s111  14419  swrdnd  14465  swrds1  14477  repswswrd  14595  cshw0  14605  s2f1o  14728  f1oun2prg  14729  rexfiuz  15158  climz  15357  climaddc1  15443  climmulc2  15445  climsubc1  15446  climsubc2  15447  climlec2  15469  sumss  15535  binomlem  15640  binom  15641  bcxmas  15646  climcndslem1  15660  arisum2  15672  explecnv  15676  geomulcvg  15687  risefall0lem  15835  bpoly1  15860  bpolydiflem  15863  bpoly2  15866  bpoly3  15867  bpoly4  15868  ef0lem  15887  efcvgfsum  15894  ege2le3  15898  eftlub  15917  efgt1p2  15922  efgt1p  15923  ruclem4  16042  ruclem6  16043  nthruc  16060  dvds0  16080  0dvds  16085  fsumdvds  16116  odd2np1lem  16148  divalglem6  16206  divalglem7  16207  divalglem8  16208  bitsfzo  16241  bitsmod  16242  0bits  16245  m1bits  16246  sadc0  16260  smup0  16285  gcd0val  16303  gcddvds  16309  gcd0id  16325  gcdid0  16326  gcdaddm  16331  gcdid  16333  bezoutlem1  16346  bezout  16350  dfgcd2  16353  lcm0val  16396  dvdslcm  16400  lcmeq0  16402  lcmgcd  16409  lcmdvds  16410  lcmftp  16438  lcmfunsnlem2  16442  dfphi2  16572  phiprmpw  16574  pc0  16652  pcdvdstr  16674  dvdsprmpweqnn  16683  pcfaclem  16696  prmreclem2  16715  prmreclem4  16717  zgz  16731  igz  16732  4sqlem19  16761  ramz  16823  1259lem1  16929  1259lem4  16932  2503lem2  16936  4001lem1  16939  4001lem3  16941  gsumws1  18573  mulg0  18803  dfod2  19267  zaddablx  19568  0cyg  19589  srgbinomlem4  19874  zring0  20786  zndvds0  20864  ltbwe  21351  pmatcollpw3fi1  22043  iscmet3lem3  24560  vitalilem1  24878  itgcnlem  25060  dvn0  25194  dvexp3  25248  plyco  25508  0dgr  25512  0dgrb  25513  coefv0  25515  coemulc  25522  vieta1lem2  25577  vieta1  25578  elqaalem1  25585  elqaalem3  25587  aareccl  25592  aannenlem1  25594  aannenlem2  25595  aalioulem1  25598  taylfval  25624  taylplem1  25628  taylplem2  25629  taylpfval  25630  dvtaylp  25635  dvradcnv  25686  pserulm  25687  pserdvlem2  25693  abelthlem6  25701  abelthlem9  25705  logf1o2  25911  ang180lem3  26067  1cubr  26098  leibpi  26198  fsumharmonic  26267  muf  26395  0sgm  26399  1sgmprm  26453  ppiub  26458  bposlem1  26538  bposlem2  26539  lgslem2  26552  lgsfcl2  26557  lgsval2lem  26561  lgs0  26564  lgsdir2lem3  26581  lgsdirnn0  26598  lgsdinn0  26599  pntrlog2bndlem4  26834  padicabv  26884  ostth2lem2  26888  usgrexmpldifpr  27914  usgrexmplef  27915  wlkv0  28307  spthispth  28382  uhgrwkspthlem2  28410  pthdlem2  28424  clwwlkccatlem  28641  0ewlk  28766  0wlkons1  28773  0pth  28777  0pthon  28779  wlk2v2elem2  28808  ntrl2v2e  28810  0dp2dp  31470  cycpmrn  31697  zringnm  32206  qqh0  32232  qqhcn  32239  qqhucn  32240  rrh0  32263  eulerpartlemmf  32642  ballotlem2  32755  ballotlemfc0  32759  ballotlemfcc  32760  plymulx0  32826  signstf0  32847  signsvf0  32859  hgt750lemd  32928  hgt750lem  32931  0nn0m1nnn0  33370  revpfxsfxrev  33376  subfacval2  33448  cvmliftlem4  33549  cvmliftlem5  33550  fz0n  33986  bcneg1  33992  bccolsum  33995  fwddifn0  34562  fwddifnp1  34563  knoppcnlem8  34776  knoppcnlem11  34779  poimirlem24  35914  poimirlem27  35917  poimirlem28  35918  sdclem1  36014  heibor1lem  36080  heiborlem4  36085  bccl2d  40262  0dvds0  40594  mzpnegmpt  40836  diophrw  40851  vdioph  40871  diophren  40905  irrapxlem1  40914  rmxy0  41016  monotoddzzfi  41035  zindbi  41039  rmyeq0  41046  jm2.18  41081  jm2.15nn0  41096  jm2.16nn0  41097  mpaaeu  41246  nzss  42264  hashnzfz2  42268  dvradcnv2  42294  binomcxplemnn0  42296  binomcxplemrat  42297  binomcxplemnotnn0  42303  halffl  43178  lmbr3v  43630  dvnmul  43828  stoweidlem11  43896  stoweidlem17  43902  stirlinglem7  43965  fourierdlem20  44012  etransclem25  44144  etransclem26  44145  etransclem37  44156  smfmullem4  44677  2ffzoeq  45179  fmtnorec2  45354  0evenALTV  45499  0noddALTV  45500  2exp340mod341  45544  8exp8mod9  45547  nfermltl8rev  45553  1odd  45724  0even  45848  2zrngamgm  45856  altgsumbcALT  46048  blen1  46289  blen1b  46293  0dig1  46314  0dig2pr01  46315  nn0sumshdiglem1  46326  itcoval0  46367  ackval0  46385  aacllem  46864  upwordnul  46874  tworepnotupword  46880