Theorem gzcjcl

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

	Ref	Expression
Assertion	gzcjcl	⊢ ( 𝐴 ∈ ℤ[i] → ( ∗ ‘ 𝐴 ) ∈ ℤ[i] )

Proof

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