This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zsubrg

Description: The integers form a subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Assertion zsubrg ℤ ∈ ( SubRing ‘ ℂfld )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
2 zaddcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 + 𝑦 ) ∈ ℤ )
3 znegcl ⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ )
4 1z ⊢ 1 ∈ ℤ
5 zmulcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
6 1 2 3 4 5 cnsubrglem ⊢ ℤ ∈ ( SubRing ‘ ℂfld )