Theorem 0z 12650

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 11292	. 2 ⊢ 0 ∈ ℝ
2		eqid 2740	. . 3 ⊢ 0 = 0
3	2	3mix1i 1333	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12641	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 710	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1086   = wceq 1537   ∈ wcel 2108  ℝcr 11183  0cc0 11184  -cneg 11521  ℕcn 12293  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addrcl 11245  ax-rnegex 11255  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-neg 11523  df-z 12640

This theorem is referenced by:  0zd  12651  elnn0z  12652  nn0ssz  12662  znegcl  12678  zgt0ge1  12697  nnm1ge0  12711  gtndiv  12720  zeo  12729  nn0ind  12738  fnn0ind  12742  eluzaddOLD  12938  eluzsubOLD  12939  nn0uz  12945  1eluzge0  12957  nn0inf  12995  eqreznegel  12999  fz10  13605  fz01en  13612  fzshftral  13672  fznn0  13676  fz1ssfz0  13680  fz0sn  13684  fz0tp  13685  fz0to3un2pr  13686  fz0to4untppr  13687  fz0to5un2tp  13688  elfz0ubfz0  13689  fz0sn0fz1  13702  1fv  13704  fzo0n  13738  lbfzo0  13756  elfzonlteqm1  13792  fzo01  13798  fzo0to2pr  13801  fzo0to3tp  13802  ico01fl0  13870  flge0nn0  13871  divfl0  13875  btwnzge0  13879  zmodfz  13944  modid  13947  zmodid2  13950  modmuladdnn0  13966  ltweuz  14012  uzenom  14015  fzennn  14019  cardfz  14021  hashgf1o  14022  f13idfv  14051  seqfn  14064  seq1  14065  seqp1  14067  exp0  14116  bcnn  14361  bcval5  14367  bcpasc  14370  4bc2eq6  14378  hashgadd  14426  hashbc  14502  fz1isolem  14510  hashge2el2dif  14529  fi1uzind  14556  s111  14663  swrdnd  14702  swrds1  14714  repswswrd  14832  cshw0  14842  s2f1o  14965  f1oun2prg  14966  rexfiuz  15396  climz  15595  climaddc1  15681  climmulc2  15683  climsubc1  15684  climsubc2  15685  climlec2  15707  sumss  15772  binomlem  15877  binom  15878  bcxmas  15883  climcndslem1  15897  arisum2  15909  explecnv  15913  geomulcvg  15924  risefall0lem  16074  bpoly1  16099  bpolydiflem  16102  bpoly2  16105  bpoly3  16106  bpoly4  16107  ef0lem  16126  efcvgfsum  16134  ege2le3  16138  eftlub  16157  efgt1p2  16162  efgt1p  16163  ruclem4  16282  ruclem6  16283  nthruc  16300  dvds0  16320  0dvds  16325  fsumdvds  16356  odd2np1lem  16388  divalglem6  16446  divalglem7  16447  divalglem8  16448  bitsfzo  16481  bitsmod  16482  0bits  16485  m1bits  16486  sadc0  16500  smup0  16525  gcd0val  16543  gcddvds  16549  gcd0id  16565  gcdid0  16566  gcdaddm  16571  gcdid  16573  bezoutlem1  16586  bezout  16590  dfgcd2  16593  lcm0val  16641  dvdslcm  16645  lcmeq0  16647  lcmgcd  16654  lcmdvds  16655  lcmftp  16683  lcmfunsnlem2  16687  dfphi2  16821  phiprmpw  16823  pc0  16901  pcdvdstr  16923  dvdsprmpweqnn  16932  pcfaclem  16945  prmreclem2  16964  prmreclem4  16966  zgz  16980  igz  16981  4sqlem19  17010  ramz  17072  1259lem1  17178  1259lem4  17181  2503lem2  17185  4001lem1  17188  4001lem3  17190  gsumws1  18873  mulg0  19114  dfod2  19606  zaddablx  19914  0cyg  19935  srgbinomlem4  20256  zringsub  21489  zring0  21492  pzriprnglem3  21517  pzriprnglem4  21518  pzriprnglem5  21519  pzriprnglem6  21520  pzriprnglem10  21524  pzriprng1ALT  21530  zndvds0  21592  ltbwe  22085  pmatcollpw3fi1  22815  iscmet3lem3  25343  vitalilem1  25662  itgcnlem  25845  dvn0  25980  dvexp3  26036  plyco  26300  0dgr  26304  0dgrb  26305  coefv0  26307  coemulc  26314  vieta1lem2  26371  vieta1  26372  elqaalem1  26379  elqaalem3  26381  aareccl  26386  aannenlem1  26388  aannenlem2  26389  aalioulem1  26392  taylfval  26418  taylplem1  26422  taylplem2  26423  taylpfval  26424  dvtaylp  26430  dvradcnv  26482  pserulm  26483  pserdvlem2  26490  abelthlem6  26498  abelthlem9  26502  logf1o2  26710  ang180lem3  26872  1cubr  26903  leibpi  27003  fsumharmonic  27073  muf  27201  0sgm  27205  1sgmprm  27261  ppiub  27266  bposlem1  27346  bposlem2  27347  lgslem2  27360  lgsfcl2  27365  lgsval2lem  27369  lgs0  27372  lgsdir2lem3  27389  lgsdirnn0  27406  lgsdinn0  27407  pntrlog2bndlem4  27642  padicabv  27692  ostth2lem2  27696  usgrexmpldifpr  29293  usgrexmplef  29294  wlkv0  29687  spthispth  29762  uhgrwkspthlem2  29790  pthdlem2  29804  clwwlkccatlem  30021  0ewlk  30146  0wlkons1  30153  0pth  30157  0pthon  30159  wlk2v2elem2  30188  ntrl2v2e  30190  fzo0opth  32810  0dp2dp  32873  chnub  32984  cycpmrn  33136  zringnm  33904  qqh0  33930  qqhcn  33937  qqhucn  33938  rrh0  33961  eulerpartlemmf  34340  ballotlem2  34453  ballotlemfc0  34457  ballotlemfcc  34458  plymulx0  34524  signstf0  34545  signsvf0  34557  hgt750lemd  34625  hgt750lem  34628  0nn0m1nnn0  35080  revpfxsfxrev  35083  subfacval2  35155  cvmliftlem4  35256  cvmliftlem5  35257  fz0n  35693  bcneg1  35698  bccolsum  35701  fwddifn0  36128  fwddifnp1  36129  knoppcnlem8  36466  knoppcnlem11  36469  poimirlem24  37604  poimirlem27  37607  poimirlem28  37608  sdclem1  37703  heibor1lem  37769  heiborlem4  37774  bccl2d  41948  aks6d1c1  42073  aks6d1c2lem4  42084  0dvds0  42314  mzpnegmpt  42700  diophrw  42715  vdioph  42735  diophren  42769  irrapxlem1  42778  rmxy0  42880  monotoddzzfi  42899  zindbi  42903  rmyeq0  42910  jm2.18  42945  jm2.15nn0  42960  jm2.16nn0  42961  mpaaeu  43107  nzss  44286  hashnzfz2  44290  dvradcnv2  44316  binomcxplemnn0  44318  binomcxplemrat  44319  binomcxplemnotnn0  44325  halffl  45211  lmbr3v  45666  dvnmul  45864  stoweidlem11  45932  stoweidlem17  45938  stirlinglem7  46001  fourierdlem20  46048  etransclem25  46180  etransclem26  46181  etransclem37  46192  smfmullem4  46715  upwordnul  46799  tworepnotupword  46805  2ffzoeq  47242  fmtnorec2  47417  0evenALTV  47562  0noddALTV  47563  2exp340mod341  47607  8exp8mod9  47610  nfermltl8rev  47616  1odd  47894  0even  47960  2zrngamgm  47968  altgsumbcALT  48078  blen1  48318  blen1b  48322  0dig1  48343  0dig2pr01  48344  nn0sumshdiglem1  48355  itcoval0  48396  ackval0  48414  aacllem  48895