gzsubrg

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

		Ref	Expression
	Assertion	gzsubrg	$⊢ ℤ [i] \in SubRing (ℂ_{fld})$

Step	Hyp	Ref	Expression
1		gzcn	$⊢ x \in ℤ [i] \to x \in ℂ$
2		gzaddcl	$⊢ (x \in ℤ [i] \land y \in ℤ [i]) \to x + y \in ℤ [i]$
3		gznegcl	$⊢ x \in ℤ [i] \to - x \in ℤ [i]$
4		1z	$⊢ 1 \in ℤ$
5		zgz	$⊢ 1 \in ℤ \to 1 \in ℤ [i]$
6	4 5	ax-mp	$⊢ 1 \in ℤ [i]$
7		gzmulcl	$⊢ (x \in ℤ [i] \land y \in ℤ [i]) \to x y \in ℤ [i]$
8	1 2 3 6 7	cnsubrglem	$⊢ ℤ [i] \in SubRing (ℂ_{fld})$

Metamath Proof Explorer