Metamath Proof Explorer

Theorem cosangneg2d

Description: The cosine of the angle between X and -u Y is the negative of that between X and Y . If A, B and C are collinear points, this implies that the cosines of DBA and DBC sum to zero, i.e., that DBA and DBC are supplementary. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses ang.1 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
cosangneg2d.1 
|- ( ph -> X e. CC )
cosangneg2d.2 
|- ( ph -> X =/= 0 )
cosangneg2d.3 
|- ( ph -> Y e. CC )
cosangneg2d.4 
|- ( ph -> Y =/= 0 )
Assertion cosangneg2d 
|- ( ph -> ( cos ` ( X F -u Y ) ) = -u ( cos ` ( X F Y ) ) )

Proof

Step Hyp Ref Expression
1 ang.1 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 cosangneg2d.1 
 |-  ( ph -> X e. CC )
3 cosangneg2d.2 
 |-  ( ph -> X =/= 0 )
4 cosangneg2d.3 
 |-  ( ph -> Y e. CC )
5 cosangneg2d.4 
 |-  ( ph -> Y =/= 0 )
6 4 2 3 divcld 
 |-  ( ph -> ( Y / X ) e. CC )
7 6 recld 
 |-  ( ph -> ( Re ` ( Y / X ) ) e. RR )
8 7 recnd 
 |-  ( ph -> ( Re ` ( Y / X ) ) e. CC )
9 6 abscld 
 |-  ( ph -> ( abs ` ( Y / X ) ) e. RR )
10 9 recnd 
 |-  ( ph -> ( abs ` ( Y / X ) ) e. CC )
11 4 2 5 3 divne0d 
 |-  ( ph -> ( Y / X ) =/= 0 )
12 6 11 absne0d 
 |-  ( ph -> ( abs ` ( Y / X ) ) =/= 0 )
13 8 10 12 divnegd 
 |-  ( ph -> -u ( ( Re ` ( Y / X ) ) / ( abs ` ( Y / X ) ) ) = ( -u ( Re ` ( Y / X ) ) / ( abs ` ( Y / X ) ) ) )
14 1 2 3 4 5 angvald 
 |-  ( ph -> ( X F Y ) = ( Im ` ( log ` ( Y / X ) ) ) )
15 14 fveq2d 
 |-  ( ph -> ( cos ` ( X F Y ) ) = ( cos ` ( Im ` ( log ` ( Y / X ) ) ) ) )
16 6 11 cosargd 
 |-  ( ph -> ( cos ` ( Im ` ( log ` ( Y / X ) ) ) ) = ( ( Re ` ( Y / X ) ) / ( abs ` ( Y / X ) ) ) )
17 15 16 eqtrd 
 |-  ( ph -> ( cos ` ( X F Y ) ) = ( ( Re ` ( Y / X ) ) / ( abs ` ( Y / X ) ) ) )
18 17 negeqd 
 |-  ( ph -> -u ( cos ` ( X F Y ) ) = -u ( ( Re ` ( Y / X ) ) / ( abs ` ( Y / X ) ) ) )
19 4 negcld 
 |-  ( ph -> -u Y e. CC )
20 4 5 negne0d 
 |-  ( ph -> -u Y =/= 0 )
21 1 2 3 19 20 angvald 
 |-  ( ph -> ( X F -u Y ) = ( Im ` ( log ` ( -u Y / X ) ) ) )
22 21 fveq2d 
 |-  ( ph -> ( cos ` ( X F -u Y ) ) = ( cos ` ( Im ` ( log ` ( -u Y / X ) ) ) ) )
23 19 2 3 divcld 
 |-  ( ph -> ( -u Y / X ) e. CC )
24 19 2 20 3 divne0d 
 |-  ( ph -> ( -u Y / X ) =/= 0 )
25 23 24 cosargd 
 |-  ( ph -> ( cos ` ( Im ` ( log ` ( -u Y / X ) ) ) ) = ( ( Re ` ( -u Y / X ) ) / ( abs ` ( -u Y / X ) ) ) )
26 4 2 3 divnegd 
 |-  ( ph -> -u ( Y / X ) = ( -u Y / X ) )
27 26 fveq2d 
 |-  ( ph -> ( Re ` -u ( Y / X ) ) = ( Re ` ( -u Y / X ) ) )
28 6 renegd 
 |-  ( ph -> ( Re ` -u ( Y / X ) ) = -u ( Re ` ( Y / X ) ) )
29 27 28 eqtr3d 
 |-  ( ph -> ( Re ` ( -u Y / X ) ) = -u ( Re ` ( Y / X ) ) )
30 26 fveq2d 
 |-  ( ph -> ( abs ` -u ( Y / X ) ) = ( abs ` ( -u Y / X ) ) )
31 6 absnegd 
 |-  ( ph -> ( abs ` -u ( Y / X ) ) = ( abs ` ( Y / X ) ) )
32 30 31 eqtr3d 
 |-  ( ph -> ( abs ` ( -u Y / X ) ) = ( abs ` ( Y / X ) ) )
33 29 32 oveq12d 
 |-  ( ph -> ( ( Re ` ( -u Y / X ) ) / ( abs ` ( -u Y / X ) ) ) = ( -u ( Re ` ( Y / X ) ) / ( abs ` ( Y / X ) ) ) )
34 22 25 33 3eqtrd 
 |-  ( ph -> ( cos ` ( X F -u Y ) ) = ( -u ( Re ` ( Y / X ) ) / ( abs ` ( Y / X ) ) ) )
35 13 18 34 3eqtr4rd 
 |-  ( ph -> ( cos ` ( X F -u Y ) ) = -u ( cos ` ( X F Y ) ) )