Metamath Proof Explorer

Theorem gznegcl

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

Ref Expression
Assertion gznegcl ⊢ A ∈ ℤ i → − A ∈ ℤ i

Proof

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