Metamath Proof Explorer

Theorem gzcjcl

Description: The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion gzcjcl ⊢ A ∈ ℤ i → A ‾ ∈ ℤ i

Proof

Step Hyp Ref Expression
1 gzcn ⊢ A ∈ ℤ i → A ∈ ℂ
2 1 cjcld ⊢ A ∈ ℤ i → A ‾ ∈ ℂ
3 1 recjd ⊢ A ∈ ℤ i → ℜ ⁡ A ‾ = ℜ ⁡ A
4 elgz ⊢ A ∈ ℤ i ↔ A ∈ ℂ ∧ ℜ ⁡ A ∈ ℤ ∧ ℑ ⁡ A ∈ ℤ
5 4 simp2bi ⊢ A ∈ ℤ i → ℜ ⁡ A ∈ ℤ
6 3 5 eqeltrd ⊢ A ∈ ℤ i → ℜ ⁡ A ‾ ∈ ℤ
7 1 imcjd ⊢ A ∈ ℤ i → ℑ ⁡ A ‾ = − ℑ ⁡ A
8 4 simp3bi ⊢ A ∈ ℤ i → ℑ ⁡ A ∈ ℤ
9 8 znegcld ⊢ A ∈ ℤ i → − ℑ ⁡ A ∈ ℤ
10 7 9 eqeltrd ⊢ A ∈ ℤ i → ℑ ⁡ A ‾ ∈ ℤ
11 elgz ⊢ A ‾ ∈ ℤ i ↔ A ‾ ∈ ℂ ∧ ℜ ⁡ A ‾ ∈ ℤ ∧ ℑ ⁡ A ‾ ∈ ℤ
12 2 6 10 11 syl3anbrc ⊢ A ∈ ℤ i → A ‾ ∈ ℤ i