gzreim

Description: Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014)

		Ref	Expression
	Assertion	gzreim	$⊢ (A \in ℤ \land B \in ℤ) \to A + i B \in ℤ [i]$

Step	Hyp	Ref	Expression
1		zgz	$⊢ A \in ℤ \to A \in ℤ [i]$
2		igz	$⊢ i \in ℤ [i]$
3		zgz	$⊢ B \in ℤ \to B \in ℤ [i]$
4		gzmulcl	$⊢ (i \in ℤ [i] \land B \in ℤ [i]) \to i B \in ℤ [i]$
5	2 3 4	sylancr	$⊢ B \in ℤ \to i B \in ℤ [i]$
6		gzaddcl	$⊢ (A \in ℤ [i] \land i B \in ℤ [i]) \to A + i B \in ℤ [i]$
7	1 5 6	syl2an	$⊢ (A \in ℤ \land B \in ℤ) \to A + i B \in ℤ [i]$

Metamath Proof Explorer