Theorem 0z 8822

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 7549	. 2 ⊢ 0 ∈ ℝ
2		eqid 2089	. . 3 ⊢ 0 = 0
3	2	3mix1i 1116	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 8813	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 889	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 924   = wceq 1290   ∈ wcel 1439  ℝcr 7410  0cc0 7411  -cneg 7715  ℕcn 8483  ℤcz 8811

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-1re 7500  ax-addrcl 7503  ax-rnegex 7515

This theorem depends on definitions:  df-bi 116  df-3or 926  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-rab 2369  df-v 2622  df-un 3004  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-br 3852  df-iota 4993  df-fv 5036  df-ov 5669  df-neg 7717  df-z 8812

This theorem is referenced by:  0zd  8823  nn0ssz  8829  znegcl  8842  zgt0ge1  8869  nn0n0n1ge2b  8887  nn0lt10b  8888  nnm1ge0  8893  gtndiv  8902  msqznn  8907  zeo  8912  nn0ind  8921  fnn0ind  8923  nn0uz  9114  1eluzge0  9123  eqreznegel  9160  qreccl  9188  qdivcl  9189  irrmul  9193  fz10  9521  fz01en  9528  fzpreddisj  9546  fzshftral  9583  fznn0  9588  fz1ssfz0  9592  fz0tp  9596  elfz0ubfz0  9597  1fv  9611  lbfzo0  9653  elfzonlteqm1  9682  fzo01  9688  fzo0to2pr  9690  fzo0to3tp  9691  flqge0nn0  9761  divfl0  9764  btwnzge0  9768  modqmulnn  9810  zmodfz  9814  modqid  9817  zmodid2  9820  q0mod  9823  modqmuladdnn0  9836  frecfzennn  9894  qexpclz  10037  facdiv  10207  bcval  10218  bcnn  10226  bcm1k  10229  ibcval5  10232  bcpasc  10235  4bc2eq6  10243  hashinfom  10247  rexfiuz  10483  qabsor  10569  nn0abscl  10579  nnabscl  10594  climz  10741  climaddc1  10778  climmulc2  10780  climsubc1  10781  climsubc2  10782  climlec2  10791  binomlem  10938  binom  10939  bcxmas  10944  arisum2  10954  explecnv  10960  ef0lem  11011  dvdsval2  11138  dvdsdc  11143  moddvds  11144  dvds0  11150  0dvds  11155  zdvdsdc  11156  dvdscmulr  11164  dvdsmulcr  11165  dvdslelemd  11183  dvdsabseq  11187  divconjdvds  11189  alzdvds  11194  fzo0dvdseq  11197  odd2np1lem  11211  gcdmndc  11279  gcdsupex  11288  gcdsupcl  11289  gcd0val  11291  gcddvds  11294  gcd0id  11309  gcdid0  11310  gcdid  11316  bezoutlema  11327  bezoutlemb  11328  bezoutlembi  11333  dfgcd3  11338  dfgcd2  11342  gcdmultiplez  11349  dvdssq  11359  algcvgblem  11370  lcmmndc  11383  lcm0val  11386  dvdslcm  11390  lcmeq0  11392  lcmgcd  11399  lcmdvds  11400  lcmid  11401  3lcm2e6woprm  11407  6lcm4e12  11408  cncongr2  11425  sqrt2irrap  11497  dfphi2  11535  phiprmpw  11537  crth  11539  phimullem  11540  hashgcdeq  11543