Metamath Proof Explorer

Theorem angneg

Description: Cancel a negative sign in the angle function. (Contributed by Mario Carneiro, 23-Sep-2014)

Ref Expression
Hypothesis ang.1 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
Assertion angneg 
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( -u A F -u B ) = ( A F B ) )

Proof

Step Hyp Ref Expression
1 ang.1 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 mulm1 
 |-  ( A e. CC -> ( -u 1 x. A ) = -u A )
3 2 ad2antrr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( -u 1 x. A ) = -u A )
4 mulm1 
 |-  ( B e. CC -> ( -u 1 x. B ) = -u B )
5 4 ad2antrl 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( -u 1 x. B ) = -u B )
6 3 5 oveq12d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( -u 1 x. A ) F ( -u 1 x. B ) ) = ( -u A F -u B ) )
7 neg1cn 
 |-  -u 1 e. CC
8 neg1ne0 
 |-  -u 1 =/= 0
9 7 8 pm3.2i 
 |-  ( -u 1 e. CC /\ -u 1 =/= 0 )
10 1 angcan 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ ( -u 1 e. CC /\ -u 1 =/= 0 ) ) -> ( ( -u 1 x. A ) F ( -u 1 x. B ) ) = ( A F B ) )
11 9 10 mp3an3 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( -u 1 x. A ) F ( -u 1 x. B ) ) = ( A F B ) )
12 6 11 eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( -u A F -u B ) = ( A F B ) )