Theorem igz

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

	Ref	Expression
Assertion	igz	⊢ i ∈ ℤ[i]

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2		rei	⊢ ( ℜ ‘ i ) = 0
3		0z	⊢ 0 ∈ ℤ
4	2 3	eqeltri	⊢ ( ℜ ‘ i ) ∈ ℤ
5		imi	⊢ ( ℑ ‘ i ) = 1
6		1z	⊢ 1 ∈ ℤ
7	5 6	eqeltri	⊢ ( ℑ ‘ i ) ∈ ℤ
8		elgz	⊢ ( i ∈ ℤ[i] ↔ ( i ∈ ℂ ∧ ( ℜ ‘ i ) ∈ ℤ ∧ ( ℑ ‘ i ) ∈ ℤ ) )
9	1 4 7 8	mpbir3an	⊢ i ∈ ℤ[i]