zgz

Description: An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014)

		Ref	Expression
	Assertion	zgz	$⊢ A \in ℤ \to A \in ℤ [i]$

Step	Hyp	Ref	Expression
1		zcn	$⊢ A \in ℤ \to A \in ℂ$
2		zre	$⊢ A \in ℤ \to A \in ℝ$
3	2	rered	$⊢ A \in ℤ \to ℜ (A) = A$
4		id	$⊢ A \in ℤ \to A \in ℤ$
5	3 4	eqeltrd	$⊢ A \in ℤ \to ℜ (A) \in ℤ$
6	2	reim0d	$⊢ A \in ℤ \to ℑ (A) = 0$
7		0z	$⊢ 0 \in ℤ$
8	6 7	eqeltrdi	$⊢ A \in ℤ \to ℑ (A) \in ℤ$
9		elgz	$⊢ A \in ℤ [i] \leftrightarrow (A \in ℂ \land ℜ (A) \in ℤ \land ℑ (A) \in ℤ)$
10	1 5 8 9	syl3anbrc	$⊢ A \in ℤ \to A \in ℤ [i]$

Metamath Proof Explorer