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	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
	cosangneg2d.1	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	cosangneg2d.2	⊢ ( 𝜑 → 𝑋 ≠ 0 )
	cosangneg2d.3	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
	cosangneg2d.4	⊢ ( 𝜑 → 𝑌 ≠ 0 )
Assertion	cosangneg2d	⊢ ( 𝜑 → ( cos ‘ ( 𝑋 𝐹 - 𝑌 ) ) = - ( cos ‘ ( 𝑋 𝐹 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ang.1	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2		cosangneg2d.1	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
3		cosangneg2d.2	⊢ ( 𝜑 → 𝑋 ≠ 0 )
4		cosangneg2d.3	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
5		cosangneg2d.4	⊢ ( 𝜑 → 𝑌 ≠ 0 )
6	4 2 3	divcld	⊢ ( 𝜑 → ( 𝑌 / 𝑋 ) ∈ ℂ )
7	6	recld	⊢ ( 𝜑 → ( ℜ ‘ ( 𝑌 / 𝑋 ) ) ∈ ℝ )
8	7	recnd	⊢ ( 𝜑 → ( ℜ ‘ ( 𝑌 / 𝑋 ) ) ∈ ℂ )
9	6	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝑌 / 𝑋 ) ) ∈ ℝ )
10	9	recnd	⊢ ( 𝜑 → ( abs ‘ ( 𝑌 / 𝑋 ) ) ∈ ℂ )
11	4 2 5 3	divne0d	⊢ ( 𝜑 → ( 𝑌 / 𝑋 ) ≠ 0 )
12	6 11	absne0d	⊢ ( 𝜑 → ( abs ‘ ( 𝑌 / 𝑋 ) ) ≠ 0 )
13	8 10 12	divnegd	⊢ ( 𝜑 → - ( ( ℜ ‘ ( 𝑌 / 𝑋 ) ) / ( abs ‘ ( 𝑌 / 𝑋 ) ) ) = ( - ( ℜ ‘ ( 𝑌 / 𝑋 ) ) / ( abs ‘ ( 𝑌 / 𝑋 ) ) ) )
14	1 2 3 4 5	angvald	⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) )
15	14	fveq2d	⊢ ( 𝜑 → ( cos ‘ ( 𝑋 𝐹 𝑌 ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) ) )
16	6 11	cosargd	⊢ ( 𝜑 → ( cos ‘ ( ℑ ‘ ( log ‘ ( 𝑌 / 𝑋 ) ) ) ) = ( ( ℜ ‘ ( 𝑌 / 𝑋 ) ) / ( abs ‘ ( 𝑌 / 𝑋 ) ) ) )
17	15 16	eqtrd	⊢ ( 𝜑 → ( cos ‘ ( 𝑋 𝐹 𝑌 ) ) = ( ( ℜ ‘ ( 𝑌 / 𝑋 ) ) / ( abs ‘ ( 𝑌 / 𝑋 ) ) ) )
18	17	negeqd	⊢ ( 𝜑 → - ( cos ‘ ( 𝑋 𝐹 𝑌 ) ) = - ( ( ℜ ‘ ( 𝑌 / 𝑋 ) ) / ( abs ‘ ( 𝑌 / 𝑋 ) ) ) )
19	4	negcld	⊢ ( 𝜑 → - 𝑌 ∈ ℂ )
20	4 5	negne0d	⊢ ( 𝜑 → - 𝑌 ≠ 0 )
21	1 2 3 19 20	angvald	⊢ ( 𝜑 → ( 𝑋 𝐹 - 𝑌 ) = ( ℑ ‘ ( log ‘ ( - 𝑌 / 𝑋 ) ) ) )
22	21	fveq2d	⊢ ( 𝜑 → ( cos ‘ ( 𝑋 𝐹 - 𝑌 ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ ( - 𝑌 / 𝑋 ) ) ) ) )
23	19 2 3	divcld	⊢ ( 𝜑 → ( - 𝑌 / 𝑋 ) ∈ ℂ )
24	19 2 20 3	divne0d	⊢ ( 𝜑 → ( - 𝑌 / 𝑋 ) ≠ 0 )
25	23 24	cosargd	⊢ ( 𝜑 → ( cos ‘ ( ℑ ‘ ( log ‘ ( - 𝑌 / 𝑋 ) ) ) ) = ( ( ℜ ‘ ( - 𝑌 / 𝑋 ) ) / ( abs ‘ ( - 𝑌 / 𝑋 ) ) ) )
26	4 2 3	divnegd	⊢ ( 𝜑 → - ( 𝑌 / 𝑋 ) = ( - 𝑌 / 𝑋 ) )
27	26	fveq2d	⊢ ( 𝜑 → ( ℜ ‘ - ( 𝑌 / 𝑋 ) ) = ( ℜ ‘ ( - 𝑌 / 𝑋 ) ) )
28	6	renegd	⊢ ( 𝜑 → ( ℜ ‘ - ( 𝑌 / 𝑋 ) ) = - ( ℜ ‘ ( 𝑌 / 𝑋 ) ) )
29	27 28	eqtr3d	⊢ ( 𝜑 → ( ℜ ‘ ( - 𝑌 / 𝑋 ) ) = - ( ℜ ‘ ( 𝑌 / 𝑋 ) ) )
30	26	fveq2d	⊢ ( 𝜑 → ( abs ‘ - ( 𝑌 / 𝑋 ) ) = ( abs ‘ ( - 𝑌 / 𝑋 ) ) )
31	6	absnegd	⊢ ( 𝜑 → ( abs ‘ - ( 𝑌 / 𝑋 ) ) = ( abs ‘ ( 𝑌 / 𝑋 ) ) )
32	30 31	eqtr3d	⊢ ( 𝜑 → ( abs ‘ ( - 𝑌 / 𝑋 ) ) = ( abs ‘ ( 𝑌 / 𝑋 ) ) )
33	29 32	oveq12d	⊢ ( 𝜑 → ( ( ℜ ‘ ( - 𝑌 / 𝑋 ) ) / ( abs ‘ ( - 𝑌 / 𝑋 ) ) ) = ( - ( ℜ ‘ ( 𝑌 / 𝑋 ) ) / ( abs ‘ ( 𝑌 / 𝑋 ) ) ) )
34	22 25 33	3eqtrd	⊢ ( 𝜑 → ( cos ‘ ( 𝑋 𝐹 - 𝑌 ) ) = ( - ( ℜ ‘ ( 𝑌 / 𝑋 ) ) / ( abs ‘ ( 𝑌 / 𝑋 ) ) ) )
35	13 18 34	3eqtr4rd	⊢ ( 𝜑 → ( cos ‘ ( 𝑋 𝐹 - 𝑌 ) ) = - ( cos ‘ ( 𝑋 𝐹 𝑌 ) ) )