Theorem gzcn

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

	Ref	Expression
Assertion	gzcn	⊢ ( 𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		elgz	⊢ ( 𝐴 ∈ ℤ[i] ↔ ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) )
2	1	simp1bi	⊢ ( 𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ )