Theorem 0z 12604

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

Syntax hints:   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  ℝcr 11133  0cc0 11134  -cneg 11472  ℕcn 12245  ℤcz 12593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-1cn 11192  ax-addrcl 11195  ax-rnegex 11205  ax-cnre 11207

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-neg 11474  df-z 12594

This theorem is referenced by:  0zd  12605  elnn0z  12606  nn0ssz  12616  znegcl  12632  zgt0ge1  12652  nnm1ge0  12666  gtndiv  12675  zeo  12684  nn0ind  12693  fnn0ind  12697  eluzaddOLD  12892  eluzsubOLD  12893  nn0uz  12899  1eluzge0  12913  nn0inf  12951  eqreznegel  12955  fz10  13567  fz01en  13574  fzshftral  13637  fznn0  13641  fz1ssfz0  13645  fz0sn  13649  fz0tp  13650  fz0to3un2pr  13651  fz0to4untppr  13652  fz0to5un2tp  13653  elfz0ubfz0  13654  fz0sn0fz1  13667  1fv  13669  fzo0n  13703  lbfzo0  13721  elfzonlteqm1  13762  fzo01  13768  fzo0to2pr  13771  fz01pr  13772  fzo0to3tp  13773  ico01fl0  13841  flge0nn0  13842  divfl0  13846  btwnzge0  13850  zmodfz  13915  modid  13918  zmodid2  13921  modmuladdnn0  13938  ltweuz  13984  uzenom  13987  fzennn  13991  cardfz  13993  hashgf1o  13994  f13idfv  14023  seqfn  14036  seq1  14037  seqp1  14039  exp0  14088  bcnn  14335  bcval5  14341  bcpasc  14344  4bc2eq6  14352  hashgadd  14400  hashbc  14476  fz1isolem  14484  hashge2el2dif  14503  fi1uzind  14530  s111  14638  swrdnd  14677  swrds1  14689  repswswrd  14807  cshw0  14817  s2f1o  14940  f1oun2prg  14941  rexfiuz  15371  climz  15570  climaddc1  15656  climmulc2  15658  climsubc1  15659  climsubc2  15660  climlec2  15680  sumss  15745  binomlem  15850  binom  15851  bcxmas  15856  climcndslem1  15870  arisum2  15882  explecnv  15886  geomulcvg  15897  risefall0lem  16047  bpoly1  16072  bpolydiflem  16075  bpoly2  16078  bpoly3  16079  bpoly4  16080  ef0lem  16099  efcvgfsum  16107  ege2le3  16111  eftlub  16132  efgt1p2  16137  efgt1p  16138  ruclem4  16257  ruclem6  16258  nthruc  16275  dvds0  16296  0dvds  16301  fsumdvds  16332  odd2np1lem  16364  divalglem6  16422  divalglem7  16423  divalglem8  16424  bitsfzo  16459  bitsmod  16460  0bits  16463  m1bits  16464  sadc0  16478  smup0  16503  gcd0val  16521  gcddvds  16527  gcd0id  16543  gcdid0  16544  gcdaddm  16549  gcdid  16551  bezoutlem1  16563  bezout  16567  dfgcd2  16570  lcm0val  16618  dvdslcm  16622  lcmeq0  16624  lcmgcd  16631  lcmdvds  16632  lcmftp  16660  lcmfunsnlem2  16664  dfphi2  16798  phiprmpw  16800  pc0  16879  pcdvdstr  16901  dvdsprmpweqnn  16910  pcfaclem  16923  prmreclem2  16942  prmreclem4  16944  zgz  16958  igz  16959  4sqlem19  16988  ramz  17050  1259lem1  17155  1259lem4  17158  2503lem2  17162  4001lem1  17165  4001lem3  17167  gsumws1  18821  mulg0  19062  dfod2  19550  zaddablx  19858  0cyg  19879  srgbinomlem4  20194  zringsub  21421  zring0  21424  pzriprnglem3  21449  pzriprnglem4  21450  pzriprnglem5  21451  pzriprnglem6  21452  pzriprnglem10  21456  pzriprng1ALT  21462  zndvds0  21516  ltbwe  22007  pmatcollpw3fi1  22731  iscmet3lem3  25247  vitalilem1  25566  itgcnlem  25748  dvn0  25883  dvexp3  25939  plyco  26203  0dgr  26207  0dgrb  26208  coefv0  26210  coemulc  26217  vieta1lem2  26276  vieta1  26277  elqaalem1  26284  elqaalem3  26286  aareccl  26291  aannenlem1  26293  aannenlem2  26294  aalioulem1  26297  taylfval  26323  taylplem1  26327  taylplem2  26328  taylpfval  26329  dvtaylp  26335  dvradcnv  26387  pserulm  26388  pserdvlem2  26395  abelthlem6  26403  abelthlem9  26407  logf1o2  26616  ang180lem3  26778  1cubr  26809  leibpi  26909  fsumharmonic  26979  muf  27107  0sgm  27111  1sgmprm  27167  ppiub  27172  bposlem1  27252  bposlem2  27253  lgslem2  27266  lgsfcl2  27271  lgsval2lem  27275  lgs0  27278  lgsdir2lem3  27295  lgsdirnn0  27312  lgsdinn0  27313  pntrlog2bndlem4  27548  padicabv  27598  ostth2lem2  27602  usgrexmpldifpr  29242  usgrexmplef  29243  wlkv0  29636  spthispth  29711  dfpth2  29716  uhgrwkspthlem2  29741  pthdlem2  29755  clwwlkccatlem  29975  0ewlk  30100  0wlkons1  30107  0pth  30111  0pthon  30113  wlk2v2elem2  30142  ntrl2v2e  30144  fzo0opth  32787  0dp2dp  32888  chnub  32997  cycpmrn  33159  elrgspnlem1  33242  constrextdg2  33788  zringnm  33994  qqh0  34020  qqhcn  34027  qqhucn  34028  rrh0  34051  eulerpartlemmf  34412  ballotlem2  34526  ballotlemfc0  34530  ballotlemfcc  34531  plymulx0  34584  signstf0  34605  signsvf0  34617  hgt750lemd  34685  hgt750lem  34688  0nn0m1nnn0  35140  revpfxsfxrev  35143  subfacval2  35214  cvmliftlem4  35315  cvmliftlem5  35316  fz0n  35753  bcneg1  35758  bccolsum  35761  fwddifn0  36187  fwddifnp1  36188  knoppcnlem8  36523  knoppcnlem11  36526  poimirlem24  37673  poimirlem27  37676  poimirlem28  37677  sdclem1  37772  heibor1lem  37838  heiborlem4  37843  bccl2d  42009  aks6d1c1  42134  aks6d1c2lem4  42145  0dvds0  42345  mzpnegmpt  42742  diophrw  42757  vdioph  42777  diophren  42811  irrapxlem1  42820  rmxy0  42922  monotoddzzfi  42941  zindbi  42945  rmyeq0  42952  jm2.18  42987  jm2.15nn0  43002  jm2.16nn0  43003  mpaaeu  43149  nzss  44316  hashnzfz2  44320  dvradcnv2  44346  binomcxplemnn0  44348  binomcxplemrat  44349  binomcxplemnotnn0  44355  halffl  45305  lmbr3v  45754  dvnmul  45952  stoweidlem11  46020  stoweidlem17  46026  stirlinglem7  46089  fourierdlem20  46136  etransclem25  46268  etransclem26  46269  etransclem37  46280  smfmullem4  46803  upwordnul  46889  tworepnotupword  46895  2ffzoeq  47336  fmtnorec2  47537  0evenALTV  47682  0noddALTV  47683  2exp340mod341  47727  8exp8mod9  47730  nfermltl8rev  47736  gpgusgralem  48040  1odd  48126  0even  48192  2zrngamgm  48200  altgsumbcALT  48308  blen1  48544  blen1b  48548  0dig1  48569  0dig2pr01  48570  nn0sumshdiglem1  48581  itcoval0  48622  ackval0  48640  aacllem  49645