Theorem 0z 12511

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 11146	. 2 ⊢ 0 ∈ ℝ
2		eqid 2737	. . 3 ⊢ 0 = 0
3	2	3mix1i 1335	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 12502	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 712	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ℝcr 11037  0cc0 11038  -cneg 11377  ℕcn 12157  ℤcz 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501

This theorem is referenced by:  0zd  12512  elnn0z  12513  nn0ssz  12523  znegcl  12538  zgt0ge1  12558  nnm1ge0  12572  gtndiv  12581  zeo  12590  nn0ind  12599  fnn0ind  12603  nn0uz  12801  1eluzge0  12805  nn0inf  12855  eqreznegel  12859  fz10  13473  fz01en  13480  fzshftral  13543  fznn0  13547  fz1ssfz0  13551  fz0sn  13555  fz0tp  13556  fz0to3un2pr  13557  fz0to4untppr  13558  fz0to5un2tp  13559  elfz0ubfz0  13560  fz0sn0fz1  13573  1fv  13575  fzo0n  13609  lbfzo0  13627  elfzonlteqm1  13669  fzo01  13675  fzo0to2pr  13678  fz01pr  13679  fzo0to3tp  13680  ico01fl0  13751  flge0nn0  13752  divfl0  13756  btwnzge0  13760  zmodfz  13825  modid  13828  zmodid2  13831  modmuladdnn0  13850  ltweuz  13896  uzenom  13899  fzennn  13903  cardfz  13905  hashgf1o  13906  f13idfv  13935  seqfn  13948  seq1  13949  seqp1  13951  exp0  14000  bcnn  14247  bcval5  14253  bcpasc  14256  4bc2eq6  14264  hashgadd  14312  hashbc  14388  fz1isolem  14396  hashge2el2dif  14415  fi1uzind  14442  s111  14551  swrdnd  14590  swrds1  14602  repswswrd  14719  cshw0  14729  s2f1o  14851  f1oun2prg  14852  rexfiuz  15283  climz  15484  climaddc1  15570  climmulc2  15572  climsubc1  15573  climsubc2  15574  climlec2  15594  sumss  15659  binomlem  15764  binom  15765  bcxmas  15770  climcndslem1  15784  arisum2  15796  explecnv  15800  geomulcvg  15811  risefall0lem  15961  bpoly1  15986  bpolydiflem  15989  bpoly2  15992  bpoly3  15993  bpoly4  15994  ef0lem  16013  efcvgfsum  16021  ege2le3  16025  eftlub  16046  efgt1p2  16051  efgt1p  16052  ruclem4  16171  ruclem6  16172  nthruc  16189  dvds0  16210  0dvds  16215  fsumdvds  16247  odd2np1lem  16279  divalglem6  16337  divalglem7  16338  divalglem8  16339  bitsfzo  16374  bitsmod  16375  0bits  16378  m1bits  16379  sadc0  16393  smup0  16418  gcd0val  16436  gcddvds  16442  gcd0id  16458  gcdid0  16459  gcdaddm  16464  gcdid  16466  bezoutlem1  16478  bezout  16482  dfgcd2  16485  lcm0val  16533  dvdslcm  16537  lcmeq0  16539  lcmgcd  16546  lcmdvds  16547  lcmftp  16575  lcmfunsnlem2  16579  dfphi2  16713  phiprmpw  16715  pc0  16794  pcdvdstr  16816  dvdsprmpweqnn  16825  pcfaclem  16838  prmreclem2  16857  prmreclem4  16859  zgz  16873  igz  16874  4sqlem19  16903  ramz  16965  1259lem1  17070  1259lem4  17073  2503lem2  17077  4001lem1  17080  4001lem3  17082  chnub  18557  gsumws1  18775  mulg0  19016  dfod2  19505  zaddablx  19813  0cyg  19834  srgbinomlem4  20176  zringsub  21422  zring0  21425  pzriprnglem3  21450  pzriprnglem4  21451  pzriprnglem5  21452  pzriprnglem6  21453  pzriprnglem10  21457  pzriprng1ALT  21463  zndvds0  21517  ltbwe  22011  pmatcollpw3fi1  22744  iscmet3lem3  25258  vitalilem1  25577  itgcnlem  25759  dvn0  25894  dvexp3  25950  plyco  26214  0dgr  26218  0dgrb  26219  coefv0  26221  coemulc  26228  vieta1lem2  26287  vieta1  26288  elqaalem1  26295  elqaalem3  26297  aareccl  26302  aannenlem1  26304  aannenlem2  26305  aalioulem1  26308  taylfval  26334  taylplem1  26338  taylplem2  26339  taylpfval  26340  dvtaylp  26346  dvradcnv  26398  pserulm  26399  pserdvlem2  26406  abelthlem6  26414  abelthlem9  26418  logf1o2  26627  ang180lem3  26789  1cubr  26820  leibpi  26920  fsumharmonic  26990  muf  27118  0sgm  27122  1sgmprm  27178  ppiub  27183  bposlem1  27263  bposlem2  27264  lgslem2  27277  lgsfcl2  27282  lgsval2lem  27286  lgs0  27289  lgsdir2lem3  27306  lgsdirnn0  27323  lgsdinn0  27324  pntrlog2bndlem4  27559  padicabv  27609  ostth2lem2  27613  usgrexmpldifpr  29343  usgrexmplef  29344  wlkv0  29735  spthispth  29809  dfpth2  29814  uhgrwkspthlem2  29839  pthdlem2  29853  clwwlkccatlem  30076  0ewlk  30201  0wlkons1  30208  0pth  30212  0pthon  30214  wlk2v2elem2  30243  ntrl2v2e  30245  fzo0opth  32893  0dp2dp  33000  cycpmrn  33236  elrgspnlem1  33335  constrextdg2  33926  zringnm  34135  qqh0  34161  qqhcn  34168  qqhucn  34169  rrh0  34192  eulerpartlemmf  34552  ballotlem2  34666  ballotlemfc0  34670  ballotlemfcc  34671  plymulx0  34724  signstf0  34745  signsvf0  34757  hgt750lemd  34825  hgt750lem  34828  0nn0m1nnn0  35326  revpfxsfxrev  35329  subfacval2  35400  cvmliftlem4  35501  cvmliftlem5  35502  fz0n  35944  bcneg1  35949  bccolsum  35952  fwddifn0  36377  fwddifnp1  36378  knoppcnlem8  36719  knoppcnlem11  36722  poimirlem24  37889  poimirlem27  37892  poimirlem28  37893  sdclem1  37988  heibor1lem  38054  heiborlem4  38059  bccl2d  42355  aks6d1c1  42480  aks6d1c2lem4  42491  0dvds0  42691  mzpnegmpt  43095  diophrw  43110  vdioph  43130  diophren  43164  irrapxlem1  43173  rmxy0  43274  monotoddzzfi  43293  zindbi  43297  rmyeq0  43304  jm2.18  43339  jm2.15nn0  43354  jm2.16nn0  43355  mpaaeu  43501  nzss  44667  hashnzfz2  44671  dvradcnv2  44697  binomcxplemnn0  44699  binomcxplemrat  44700  binomcxplemnotnn0  44706  halffl  45652  lmbr3v  46097  dvnmul  46295  stoweidlem11  46363  stoweidlem17  46369  stirlinglem7  46432  fourierdlem20  46479  etransclem25  46611  etransclem26  46612  etransclem37  46623  smfmullem4  47146  chnsubseqwl  47231  2ffzoeq  47681  fmtnorec2  47897  0evenALTV  48042  0noddALTV  48043  2exp340mod341  48087  8exp8mod9  48090  nfermltl8rev  48096  gpgusgralem  48410  1odd  48525  0even  48591  2zrngamgm  48599  altgsumbcALT  48707  blen1  48938  blen1b  48942  0dig1  48963  0dig2pr01  48964  nn0sumshdiglem1  48975  itcoval0  49016  ackval0  49034  aacllem  50154