Theorem gzcn

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

	Ref	Expression
Assertion	gzcn	$$⊢A\in \mathbb{Z}\left[i\right]\to A\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		elgz	$$⊢A\in \mathbb{Z}\left[i\right]\leftrightarrow \left(A\in ℂ\wedge \Re \left(A\right)\in \mathbb{Z}\wedge \Im \left(A\right)\in \mathbb{Z}\right)$$
2	1	simp1bi	$$⊢A\in \mathbb{Z}\left[i\right]\to A\in ℂ$$