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