Metamath Proof Explorer

Theorem imcj

Description: Imaginary part of a complex conjugate. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion imcj ⊢ A ∈ ℂ → ℑ ⁡ A ‾ = − ℑ ⁡ A

Proof

Step Hyp Ref Expression
1 recl ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
2 1 recnd ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℂ
3 ax-icn ⊢ i ∈ ℂ
4 imcl ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℝ
5 4 recnd ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℂ
6 mulcl ⊢ i ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ → i ⁢ ℑ ⁡ A ∈ ℂ
7 3 5 6 sylancr ⊢ A ∈ ℂ → i ⁢ ℑ ⁡ A ∈ ℂ
8 2 7 negsubd ⊢ A ∈ ℂ → ℜ ⁡ A + − i ⁢ ℑ ⁡ A = ℜ ⁡ A − i ⁢ ℑ ⁡ A
9 mulneg2 ⊢ i ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ → i ⁢ − ℑ ⁡ A = − i ⁢ ℑ ⁡ A
10 3 5 9 sylancr ⊢ A ∈ ℂ → i ⁢ − ℑ ⁡ A = − i ⁢ ℑ ⁡ A
11 10 oveq2d ⊢ A ∈ ℂ → ℜ ⁡ A + i ⁢ − ℑ ⁡ A = ℜ ⁡ A + − i ⁢ ℑ ⁡ A
12 remim ⊢ A ∈ ℂ → A ‾ = ℜ ⁡ A − i ⁢ ℑ ⁡ A
13 8 11 12 3eqtr4rd ⊢ A ∈ ℂ → A ‾ = ℜ ⁡ A + i ⁢ − ℑ ⁡ A
14 13 fveq2d ⊢ A ∈ ℂ → ℑ ⁡ A ‾ = ℑ ⁡ ℜ ⁡ A + i ⁢ − ℑ ⁡ A
15 4 renegcld ⊢ A ∈ ℂ → − ℑ ⁡ A ∈ ℝ
16 crim ⊢ ℜ ⁡ A ∈ ℝ ∧ − ℑ ⁡ A ∈ ℝ → ℑ ⁡ ℜ ⁡ A + i ⁢ − ℑ ⁡ A = − ℑ ⁡ A
17 1 15 16 syl2anc ⊢ A ∈ ℂ → ℑ ⁡ ℜ ⁡ A + i ⁢ − ℑ ⁡ A = − ℑ ⁡ A
18 14 17 eqtrd ⊢ A ∈ ℂ → ℑ ⁡ A ‾ = − ℑ ⁡ A