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

Metamath Proof Explorer

Theorem gznegcl

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

Ref Expression
Assertion gznegcl ( 𝐴 ∈ ℤ[i] → - 𝐴 ∈ ℤ[i] )

Proof

Step Hyp Ref Expression
1 gzcn ⊢ ( 𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ )
2 1 negcld ⊢ ( 𝐴 ∈ ℤ[i] → - 𝐴 ∈ ℂ )
3 1 renegd ⊢ ( 𝐴 ∈ ℤ[i] → ( ℜ ‘ - 𝐴 ) = - ( ℜ ‘ 𝐴 ) )
4 elgz ⊢ ( 𝐴 ∈ ℤ[i] ↔ ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) )
5 4 simp2bi ⊢ ( 𝐴 ∈ ℤ[i] → ( ℜ ‘ 𝐴 ) ∈ ℤ )
6 5 znegcld ⊢ ( 𝐴 ∈ ℤ[i] → - ( ℜ ‘ 𝐴 ) ∈ ℤ )
7 3 6 eqeltrd ⊢ ( 𝐴 ∈ ℤ[i] → ( ℜ ‘ - 𝐴 ) ∈ ℤ )
8 1 imnegd ⊢ ( 𝐴 ∈ ℤ[i] → ( ℑ ‘ - 𝐴 ) = - ( ℑ ‘ 𝐴 ) )
9 4 simp3bi ⊢ ( 𝐴 ∈ ℤ[i] → ( ℑ ‘ 𝐴 ) ∈ ℤ )
10 9 znegcld ⊢ ( 𝐴 ∈ ℤ[i] → - ( ℑ ‘ 𝐴 ) ∈ ℤ )
11 8 10 eqeltrd ⊢ ( 𝐴 ∈ ℤ[i] → ( ℑ ‘ - 𝐴 ) ∈ ℤ )
12 elgz ⊢ ( - 𝐴 ∈ ℤ[i] ↔ ( - 𝐴 ∈ ℂ ∧ ( ℜ ‘ - 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ - 𝐴 ) ∈ ℤ ) )
13 2 7 11 12 syl3anbrc ⊢ ( 𝐴 ∈ ℤ[i] → - 𝐴 ∈ ℤ[i] )