Theorem 0z 9072

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 7773	. 2 ⊢ 0 ∈ ℝ
2		eqid 2139	. . 3 ⊢ 0 = 0
3	2	3mix1i 1153	. 2 ⊢ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)
4		elz 9063	. 2 ⊢ (0 ∈ ℤ ↔ (0 ∈ ℝ ∧ (0 = 0 ∨ 0 ∈ ℕ ∨ -0 ∈ ℕ)))
5	1, 3, 4	mpbir2an 926	1 ⊢ 0 ∈ ℤ

Syntax hints:   ∨ w3o 961   = wceq 1331   ∈ wcel 1480  ℝcr 7626  0cc0 7627  -cneg 7941  ℕcn 8727  ℤcz 9061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-1re 7721  ax-addrcl 7724  ax-rnegex 7736

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-rab 2425  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777  df-neg 7943  df-z 9062

This theorem is referenced by:  0zd  9073  nn0ssz  9079  znegcl  9092  zgt0ge1  9119  nn0n0n1ge2b  9137  nn0lt10b  9138  nnm1ge0  9144  gtndiv  9153  msqznn  9158  zeo  9163  nn0ind  9172  fnn0ind  9174  nn0uz  9367  1eluzge0  9376  eqreznegel  9413  qreccl  9441  qdivcl  9442  irrmul  9446  fz10  9833  fz01en  9840  fzpreddisj  9858  fzshftral  9895  fznn0  9900  fz1ssfz0  9904  fz0tp  9908  elfz0ubfz0  9909  1fv  9923  lbfzo0  9965  elfzonlteqm1  9994  fzo01  10000  fzo0to2pr  10002  fzo0to3tp  10003  flqge0nn0  10073  divfl0  10076  btwnzge0  10080  modqmulnn  10122  zmodfz  10126  modqid  10129  zmodid2  10132  q0mod  10135  modqmuladdnn0  10148  frecfzennn  10206  qexpclz  10321  facdiv  10491  bcval  10502  bcnn  10510  bcm1k  10513  bcval5  10516  bcpasc  10519  4bc2eq6  10527  hashinfom  10531  rexfiuz  10768  qabsor  10854  nn0abscl  10864  nnabscl  10879  climz  11068  climaddc1  11105  climmulc2  11107  climsubc1  11108  climsubc2  11109  climlec2  11117  binomlem  11259  binom  11260  bcxmas  11265  arisum2  11275  explecnv  11281  ef0lem  11373  dvdsval2  11503  dvdsdc  11508  moddvds  11509  dvds0  11515  0dvds  11520  zdvdsdc  11521  dvdscmulr  11529  dvdsmulcr  11530  dvdslelemd  11548  dvdsabseq  11552  divconjdvds  11554  alzdvds  11559  fzo0dvdseq  11562  odd2np1lem  11576  gcdmndc  11644  gcdsupex  11653  gcdsupcl  11654  gcd0val  11656  gcddvds  11659  gcd0id  11674  gcdid0  11675  gcdid  11681  bezoutlema  11694  bezoutlemb  11695  bezoutlembi  11700  dfgcd3  11705  dfgcd2  11709  gcdmultiplez  11716  dvdssq  11726  algcvgblem  11737  lcmmndc  11750  lcm0val  11753  dvdslcm  11757  lcmeq0  11759  lcmgcd  11766  lcmdvds  11767  lcmid  11768  3lcm2e6woprm  11774  6lcm4e12  11775  cncongr2  11792  sqrt2irrap  11865  dfphi2  11903  phiprmpw  11905  crth  11907  phimullem  11908  hashgcdeq  11911  ennnfonelemjn  11922  ennnfonelem1  11927