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=\left(x\in \left(ℂ\setminus \left\{0\right\}\right),y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\log \left(\frac{y}{x}\right)\right)\right)$$
	cosangneg2d.1	$$⊢\phi \to X\in ℂ$$
	cosangneg2d.2	$$⊢\phi \to X\ne 0$$
	cosangneg2d.3	$$⊢\phi \to Y\in ℂ$$
	cosangneg2d.4	$$⊢\phi \to Y\ne 0$$
Assertion	cosangneg2d	$$⊢\phi \to \cos \left(XF\left(-Y\right)\right)=-\cos \left(XFY\right)$$

Proof

Step	Hyp	Ref	Expression
1		ang.1	$$⊢F=\left(x\in \left(ℂ\setminus \left\{0\right\}\right),y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\log \left(\frac{y}{x}\right)\right)\right)$$
2		cosangneg2d.1	$$⊢\phi \to X\in ℂ$$
3		cosangneg2d.2	$$⊢\phi \to X\ne 0$$
4		cosangneg2d.3	$$⊢\phi \to Y\in ℂ$$
5		cosangneg2d.4	$$⊢\phi \to Y\ne 0$$
6	4 2 3	divcld	$$⊢\phi \to \frac{Y}{X}\in ℂ$$
7	6	recld	$$⊢\phi \to \Re \left(\frac{Y}{X}\right)\in ℝ$$
8	7	recnd	$$⊢\phi \to \Re \left(\frac{Y}{X}\right)\in ℂ$$
9	6	abscld	$$⊢\phi \to \left|\frac{Y}{X}\right|\in ℝ$$
10	9	recnd	$$⊢\phi \to \left|\frac{Y}{X}\right|\in ℂ$$
11	4 2 5 3	divne0d	$$⊢\phi \to \frac{Y}{X}\ne 0$$
12	6 11	absne0d	$$⊢\phi \to \left|\frac{Y}{X}\right|\ne 0$$
13	8 10 12	divnegd	$$⊢\phi \to -\frac{\Re \left(\frac{Y}{X}\right)}{\left|\frac{Y}{X}\right|}=\frac{-\Re \left(\frac{Y}{X}\right)}{\left|\frac{Y}{X}\right|}$$
14	1 2 3 4 5	angvald	$$⊢\phi \to XFY=\Im \left(\log \left(\frac{Y}{X}\right)\right)$$
15	14	fveq2d	$$⊢\phi \to \cos \left(XFY\right)=\cos \Im \left(\log \left(\frac{Y}{X}\right)\right)$$
16	6 11	cosargd	$$⊢\phi \to \cos \Im \left(\log \left(\frac{Y}{X}\right)\right)=\frac{\Re \left(\frac{Y}{X}\right)}{\left|\frac{Y}{X}\right|}$$
17	15 16	eqtrd	$$⊢\phi \to \cos \left(XFY\right)=\frac{\Re \left(\frac{Y}{X}\right)}{\left|\frac{Y}{X}\right|}$$
18	17	negeqd	$$⊢\phi \to -\cos \left(XFY\right)=-\frac{\Re \left(\frac{Y}{X}\right)}{\left|\frac{Y}{X}\right|}$$
19	4	negcld	$$⊢\phi \to -Y\in ℂ$$
20	4 5	negne0d	$$⊢\phi \to -Y\ne 0$$
21	1 2 3 19 20	angvald	$$⊢\phi \to XF\left(-Y\right)=\Im \left(\log \left(\frac{-Y}{X}\right)\right)$$
22	21	fveq2d	$$⊢\phi \to \cos \left(XF\left(-Y\right)\right)=\cos \Im \left(\log \left(\frac{-Y}{X}\right)\right)$$
23	19 2 3	divcld	$$⊢\phi \to \frac{-Y}{X}\in ℂ$$
24	19 2 20 3	divne0d	$$⊢\phi \to \frac{-Y}{X}\ne 0$$
25	23 24	cosargd	$$⊢\phi \to \cos \Im \left(\log \left(\frac{-Y}{X}\right)\right)=\frac{\Re \left(\frac{-Y}{X}\right)}{\left|\frac{-Y}{X}\right|}$$
26	4 2 3	divnegd	$$⊢\phi \to -\frac{Y}{X}=\frac{-Y}{X}$$
27	26	fveq2d	$$⊢\phi \to \Re \left(-\frac{Y}{X}\right)=\Re \left(\frac{-Y}{X}\right)$$
28	6	renegd	$$⊢\phi \to \Re \left(-\frac{Y}{X}\right)=-\Re \left(\frac{Y}{X}\right)$$
29	27 28	eqtr3d	$$⊢\phi \to \Re \left(\frac{-Y}{X}\right)=-\Re \left(\frac{Y}{X}\right)$$
30	26	fveq2d	$$⊢\phi \to \left|-\frac{Y}{X}\right|=\left|\frac{-Y}{X}\right|$$
31	6	absnegd	$$⊢\phi \to \left|-\frac{Y}{X}\right|=\left|\frac{Y}{X}\right|$$
32	30 31	eqtr3d	$$⊢\phi \to \left|\frac{-Y}{X}\right|=\left|\frac{Y}{X}\right|$$
33	29 32	oveq12d	$$⊢\phi \to \frac{\Re \left(\frac{-Y}{X}\right)}{\left|\frac{-Y}{X}\right|}=\frac{-\Re \left(\frac{Y}{X}\right)}{\left|\frac{Y}{X}\right|}$$
34	22 25 33	3eqtrd	$$⊢\phi \to \cos \left(XF\left(-Y\right)\right)=\frac{-\Re \left(\frac{Y}{X}\right)}{\left|\frac{Y}{X}\right|}$$
35	13 18 34	3eqtr4rd	$$⊢\phi \to \cos \left(XF\left(-Y\right)\right)=-\cos \left(XFY\right)$$