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