Metamath Proof Explorer

Theorem zgz

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

Ref Expression
Assertion zgz ⊢ A ∈ ℤ → A ∈ ℤ i

Proof

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