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 )