Theorem 0z 11265

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 9919	. 2 ⊢ 0 ∈ ℝ
2		eqid 2610	. . 3 ⊢ 0 = 0
3	2	3mix1i 1226	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 11256	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 957	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977  ℝcr 9814  0cc0 9815  -cneg 10146  ℕcn 10897  ℤcz 11254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-neg 10148  df-z 11255

This theorem is referenced by:  0zd  11266  elnn0z  11267  nn0ssz  11275  znegcl  11289  zgt0ge1  11308  nnm1ge0  11321  gtndiv  11330  zeo  11339  nn0ind  11348  fnn0ind  11352  eluzadd  11592  eluzsub  11593  nn0uz  11598  1eluzge0  11608  nn0inf  11646  eqreznegel  11650  fz10  12233  fz01en  12240  fzshftral  12297  fznn0  12301  fz0sn  12308  fz0tp  12309  fz0to3un2pr  12310  fz0to4untppr  12311  elfz0ubfz0  12312  fz0sn0fz1  12325  1fv  12327  fzo0n  12359  lbfzo0  12375  elfzonlteqm1  12410  fzo01  12417  fzo0to2pr  12420  fzo0to3tp  12421  ico01fl0  12482  flge0nn0  12483  divfl0  12487  btwnzge0  12491  zmodfz  12554  modid  12557  zmodid2  12560  modmuladdnn0  12576  ltweuz  12622  uzenom  12625  fzennn  12629  cardfz  12631  hashgf1o  12632  f13idfv  12662  seqfn  12675  seq1  12676  seqp1  12678  exp0  12726  bcnn  12961  bcm1k  12964  bcval5  12967  bcpasc  12970  4bc2eq6  12978  hashgadd  13027  hashbc  13094  fz1isolem  13102  hashge2el2dif  13117  fi1uzind  13134  fi1uzindOLD  13140  s111  13248  swrdnd  13284  swrds1  13303  repswswrd  13382  cshw0  13391  s2f1o  13511  f1oun2prg  13512  rexfiuz  13935  climz  14128  climaddc1  14213  climmulc2  14215  climsubc1  14216  climsubc2  14217  climlec2  14237  sumss  14302  binomlem  14400  binom  14401  bcxmas  14406  climcndslem1  14420  arisum2  14432  explecnv  14436  geomulcvg  14446  risefall0lem  14596  binomfallfac  14611  bpoly1  14621  bpolydiflem  14624  bpoly2  14627  bpoly3  14628  bpoly4  14629  ef0lem  14648  efcvgfsum  14655  ege2le3  14659  eftlub  14678  efgt1p2  14683  efgt1p  14684  ruclem4  14802  ruclem6  14803  nthruc  14819  dvds0  14835  0dvds  14840  fsumdvds  14868  odd2np1lem  14902  divalglem6  14959  divalglem7  14960  divalglem8  14961  bitsfzo  14995  bitsmod  14996  0bits  14999  m1bits  15000  sadc0  15014  smup0  15039  gcd0val  15057  gcddvds  15063  gcd0id  15078  gcdid0  15079  gcdaddm  15084  gcdid  15086  bezoutlem1  15094  bezout  15098  dfgcd2  15101  lcm0val  15145  dvdslcm  15149  lcmeq0  15151  lcmgcd  15158  lcmdvds  15159  lcmftp  15187  lcmfunsnlem2  15191  dfphi2  15317  phiprmpw  15319  prmdiveq  15329  prmdivdiv  15330  pc0  15397  pcdvdstr  15418  dvdsprmpweqnn  15427  pcfaclem  15440  prmreclem2  15459  prmreclem4  15461  zgz  15475  igz  15476  4sqlem19  15505  vdwap0  15518  ramz  15567  1259lem1  15676  1259lem4  15679  2503lem2  15683  4001lem1  15686  4001lem3  15688  gsumws1  17199  mulg0  17369  dfod2  17804  zaddablx  18098  0cyg  18117  srgbinomlem4  18366  srgbinom  18368  ltbwe  19293  zring0  19647  zndvds0  19718  pmatcollpw3fi1lem1  20410  pmatcollpw3fi1  20412  iscmet3lem3  22896  vitalilem1  23182  vitalilem1OLD  23183  iblcnlem1  23360  itgcnlem  23362  dvn0  23493  dvexp3  23545  plyco  23801  0dgr  23805  0dgrb  23806  coefv0  23808  coemulc  23815  vieta1lem2  23870  vieta1  23871  elqaalem1  23878  elqaalem3  23880  aareccl  23885  aannenlem1  23887  aannenlem2  23888  aalioulem1  23891  taylfval  23917  taylplem1  23921  taylplem2  23922  taylpfval  23923  dvtaylp  23928  dvradcnv  23979  pserulm  23980  pserdvlem2  23986  abelthlem6  23994  abelthlem9  23998  logf1o2  24196  advlogexp  24201  ang180lem3  24341  1cubr  24369  leibpi  24469  fsumharmonic  24538  wilthlem1  24594  muf  24666  0sgm  24670  1sgmprm  24724  ppiub  24729  bposlem1  24809  bposlem2  24810  lgslem2  24823  lgsfcl2  24828  lgsval2lem  24832  lgs0  24835  lgsdir2lem3  24852  lgsdirnn0  24869  lgsdinn0  24870  pntrlog2bndlem4  25069  padicabv  25119  ostth2lem2  25123  usgraexmpldifpr  25928  usgraexmplef  25929  2trllemD  26087  2trllemG  26088  wlkntrllem2  26090  wlkntrl  26092  0pth  26100  0spth  26101  constr1trl  26118  constr2spthlem1  26124  usgrcyclnl1  26168  3v3e3cycl1  26172  constr3lem4  26175  constr3trllem3  26180  constr3trllem5  26182  wlkv0  26288  eupa0  26501  eupares  26502  zringnm  29332  qqh0  29356  qqhcn  29363  qqhucn  29364  rrh0  29387  eulerpartlemmf  29764  ballotlem2  29877  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemodife  29886  plymulx0  29950  signstf0  29971  signsvf0  29983  subfacval2  30423  cvmliftlem4  30524  cvmliftlem5  30525  fz0n  30869  bcneg1  30875  bccolsum  30878  fwddifn0  31441  fwddifnp1  31442  knoppcnlem8  31660  knoppcnlem11  31663  poimirlem24  32603  poimirlem27  32606  poimirlem28  32607  sdclem1  32709  heibor1lem  32778  heiborlem4  32783  mzpnegmpt  36325  diophrw  36340  vdioph  36361  diophren  36395  irrapxlem1  36404  rmxy0  36506  monotoddzzfi  36525  zindbi  36529  rmyeq0  36538  jm2.18  36573  jm2.15nn0  36588  jm2.16nn0  36589  mpaaeu  36739  nzss  37538  hashnzfz2  37542  dvradcnv2  37568  binomcxplemnn0  37570  binomcxplemrat  37571  binomcxplemnotnn0  37577  halffl  38451  fz1ssfz0  38465  dvnmul  38833  stoweidlem11  38904  stoweidlem17  38910  stoweidlem26  38919  stoweidlem34  38927  stirlinglem7  38973  fourierdlem20  39020  etransclem25  39152  etransclem26  39153  etransclem37  39164  smfmullem4  39679  fmtnorec2  39993  0evenALTV  40137  0noddALTV  40138  2ffzoeq  40361  1wlkv0  40859  sPthisPth  40932  uhgr1wlkspthlem2  40960  pthdlem2  40974  0ewlk  41282  0wlkOns1  41289  0pth-av  41293  0spth-av  41294  1wlk2v2elem2  41323  ntrl2v2e  41325  1odd  41601  0even  41721  2zrngamgm  41729  altgsumbcALT  41924  blen1  42176  blen1b  42180  0dig1  42201  0dig2pr01  42202  nn0sumshdiglem1  42213  aacllem  42356