Metamath Proof Explorer

Theorem imneg

Description: The imaginary part of a negative number. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion imneg ⊢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 negdid ⊢A∈ℂ→−ℜ⁡A+i⁢ℑ⁡A=-ℜ⁡A+−i⁢ℑ⁡A
9 replim ⊢A∈ℂ→A=ℜ⁡A+i⁢ℑ⁡A
10 9 negeqd ⊢A∈ℂ→−A=−ℜ⁡A+i⁢ℑ⁡A
11 mulneg2 ⊢i∈ℂ∧ℑ⁡A∈ℂ→i⁢−ℑ⁡A=−i⁢ℑ⁡A
12 3 5 11 sylancr ⊢A∈ℂ→i⁢−ℑ⁡A=−i⁢ℑ⁡A
13 12 oveq2d ⊢A∈ℂ→-ℜ⁡A+i⁢−ℑ⁡A=-ℜ⁡A+−i⁢ℑ⁡A
14 8 10 13 3eqtr4d ⊢A∈ℂ→−A=-ℜ⁡A+i⁢−ℑ⁡A
15 14 fveq2d ⊢A∈ℂ→ℑ⁡−A=ℑ⁡-ℜ⁡A+i⁢−ℑ⁡A
16 1 renegcld ⊢A∈ℂ→−ℜ⁡A∈ℝ
17 4 renegcld ⊢A∈ℂ→−ℑ⁡A∈ℝ
18 crim ⊢−ℜ⁡A∈ℝ∧−ℑ⁡A∈ℝ→ℑ⁡-ℜ⁡A+i⁢−ℑ⁡A=−ℑ⁡A
19 16 17 18 syl2anc ⊢A∈ℂ→ℑ⁡-ℜ⁡A+i⁢−ℑ⁡A=−ℑ⁡A
20 15 19 eqtrd ⊢A∈ℂ→ℑ⁡−A=−ℑ⁡A