Theorem gzsubrg

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

	Ref	Expression
Assertion	gzsubrg	⊢ ℤ[i] ∈ ( SubRing ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		gzcn	⊢ ( 𝑥 ∈ ℤ[i] → 𝑥 ∈ ℂ )
2		gzaddcl	⊢ ( ( 𝑥 ∈ ℤ[i] ∧ 𝑦 ∈ ℤ[i] ) → ( 𝑥 + 𝑦 ) ∈ ℤ[i] )
3		gznegcl	⊢ ( 𝑥 ∈ ℤ[i] → - 𝑥 ∈ ℤ[i] )
4		1z	⊢ 1 ∈ ℤ
5		zgz	⊢ ( 1 ∈ ℤ → 1 ∈ ℤ[i] )
6	4 5	ax-mp	⊢ 1 ∈ ℤ[i]
7		gzmulcl	⊢ ( ( 𝑥 ∈ ℤ[i] ∧ 𝑦 ∈ ℤ[i] ) → ( 𝑥 · 𝑦 ) ∈ ℤ[i] )
8	1 2 3 6 7	cnsubrglem	⊢ ℤ[i] ∈ ( SubRing ‘ ℂfld )