Metamath Proof Explorer

Theorem cjneg

Description: Complex conjugate of negative. (Contributed by NM, 27-Feb-2005) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion cjneg ⊢ 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 neg2subd ⊢ A ∈ ℂ → - ℜ ⁡ A - − i ⁢ ℑ ⁡ A = i ⁢ ℑ ⁡ A − ℜ ⁡ A
9 reneg ⊢ A ∈ ℂ → ℜ ⁡ − A = − ℜ ⁡ A
10 imneg ⊢ A ∈ ℂ → ℑ ⁡ − A = − ℑ ⁡ A
11 10 oveq2d ⊢ A ∈ ℂ → i ⁢ ℑ ⁡ − A = i ⁢ − ℑ ⁡ A
12 mulneg2 ⊢ i ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ → i ⁢ − ℑ ⁡ A = − i ⁢ ℑ ⁡ A
13 3 5 12 sylancr ⊢ A ∈ ℂ → i ⁢ − ℑ ⁡ A = − i ⁢ ℑ ⁡ A
14 11 13 eqtrd ⊢ A ∈ ℂ → i ⁢ ℑ ⁡ − A = − i ⁢ ℑ ⁡ A
15 9 14 oveq12d ⊢ A ∈ ℂ → ℜ ⁡ − A − i ⁢ ℑ ⁡ − A = - ℜ ⁡ A - − i ⁢ ℑ ⁡ A
16 2 7 negsubdi2d ⊢ A ∈ ℂ → − ℜ ⁡ A − i ⁢ ℑ ⁡ A = i ⁢ ℑ ⁡ A − ℜ ⁡ A
17 8 15 16 3eqtr4d ⊢ A ∈ ℂ → ℜ ⁡ − A − i ⁢ ℑ ⁡ − A = − ℜ ⁡ A − i ⁢ ℑ ⁡ A
18 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
19 remim ⊢ − A ∈ ℂ → − A ‾ = ℜ ⁡ − A − i ⁢ ℑ ⁡ − A
20 18 19 syl ⊢ A ∈ ℂ → − A ‾ = ℜ ⁡ − A − i ⁢ ℑ ⁡ − A
21 remim ⊢ A ∈ ℂ → A ‾ = ℜ ⁡ A − i ⁢ ℑ ⁡ A
22 21 negeqd ⊢ A ∈ ℂ → − A ‾ = − ℜ ⁡ A − i ⁢ ℑ ⁡ A
23 17 20 22 3eqtr4d ⊢ A ∈ ℂ → − A ‾ = − A ‾