Theorem zgz

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

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

Proof

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
2		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
3	2	rered	⊢ ( 𝐴 ∈ ℤ → ( ℜ ‘ 𝐴 ) = 𝐴 )
4		id	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℤ )
5	3 4	eqeltrd	⊢ ( 𝐴 ∈ ℤ → ( ℜ ‘ 𝐴 ) ∈ ℤ )
6	2	reim0d	⊢ ( 𝐴 ∈ ℤ → ( ℑ ‘ 𝐴 ) = 0 )
7		0z	⊢ 0 ∈ ℤ
8	6 7	eqeltrdi	⊢ ( 𝐴 ∈ ℤ → ( ℑ ‘ 𝐴 ) ∈ ℤ )
9		elgz	⊢ ( 𝐴 ∈ ℤ[i] ↔ ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) )
10	1 5 8 9	syl3anbrc	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℤ[i] )