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

Metamath Proof Explorer

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