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‾