This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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]