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] )