Theorem angpieqvdlem

Description: Equivalence used in the proof of angpieqvd . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	angpieqvdlem.A	$$⊢\phi \to A\in ℂ$$
	angpieqvdlem.B	$$⊢\phi \to B\in ℂ$$
	angpieqvdlem.C	$$⊢\phi \to C\in ℂ$$
	angpieqvdlem.AneB	$$⊢\phi \to A\ne B$$
	angpieqvdlem.AneC	$$⊢\phi \to A\ne C$$
Assertion	angpieqvdlem	$$⊢\phi \to \left(-\frac{C-B}{A-B}\in {ℝ}^{+}\leftrightarrow \frac{C-B}{C-A}\in \left(0,1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		angpieqvdlem.A	$$⊢\phi \to A\in ℂ$$
2		angpieqvdlem.B	$$⊢\phi \to B\in ℂ$$
3		angpieqvdlem.C	$$⊢\phi \to C\in ℂ$$
4		angpieqvdlem.AneB	$$⊢\phi \to A\ne B$$
5		angpieqvdlem.AneC	$$⊢\phi \to A\ne C$$
6	3 2	subcld	$$⊢\phi \to C-B\in ℂ$$
7	1 2	subcld	$$⊢\phi \to A-B\in ℂ$$
8	1 2 4	subne0d	$$⊢\phi \to A-B\ne 0$$
9	6 7 8	divcld	$$⊢\phi \to \frac{C-B}{A-B}\in ℂ$$
10	9	negcld	$$⊢\phi \to -\frac{C-B}{A-B}\in ℂ$$
11		1cnd	$$⊢\phi \to 1\in ℂ$$
12	5	necomd	$$⊢\phi \to C\ne A$$
13	3 1 2 12	subneintr2d	$$⊢\phi \to C-B\ne A-B$$
14	6 7 8 13	divne1d	$$⊢\phi \to \frac{C-B}{A-B}\ne 1$$
15	9 11 14	negned	$$⊢\phi \to -\frac{C-B}{A-B}\ne -1$$
16	10 15	xov1plusxeqvd	$$⊢\phi \to \left(-\frac{C-B}{A-B}\in {ℝ}^{+}\leftrightarrow \frac{-\frac{C-B}{A-B}}{1+\left(-\frac{C-B}{A-B}\right)}\in \left(0,1\right)\right)$$
17	6 7 8	divnegd	$$⊢\phi \to -\frac{C-B}{A-B}=\frac{-\left(C-B\right)}{A-B}$$
18	3 2	negsubdi2d	$$⊢\phi \to -\left(C-B\right)=B-C$$
19	18	oveq1d	$$⊢\phi \to \frac{-\left(C-B\right)}{A-B}=\frac{B-C}{A-B}$$
20	17 19	eqtrd	$$⊢\phi \to -\frac{C-B}{A-B}=\frac{B-C}{A-B}$$
21	7 8	dividd	$$⊢\phi \to \frac{A-B}{A-B}=1$$
22	21	oveq1d	$$⊢\phi \to \left(\frac{A-B}{A-B}\right)-\left(\frac{C-B}{A-B}\right)=1-\left(\frac{C-B}{A-B}\right)$$
23	7 6 7 8	divsubdird	$$⊢\phi \to \frac{A-B-\left(C-B\right)}{A-B}=\left(\frac{A-B}{A-B}\right)-\left(\frac{C-B}{A-B}\right)$$
24	11 9	negsubd	$$⊢\phi \to 1+\left(-\frac{C-B}{A-B}\right)=1-\left(\frac{C-B}{A-B}\right)$$
25	22 23 24	3eqtr4rd	$$⊢\phi \to 1+\left(-\frac{C-B}{A-B}\right)=\frac{A-B-\left(C-B\right)}{A-B}$$
26	1 3 2	nnncan2d	$$⊢\phi \to A-B-\left(C-B\right)=A-C$$
27	26	oveq1d	$$⊢\phi \to \frac{A-B-\left(C-B\right)}{A-B}=\frac{A-C}{A-B}$$
28	25 27	eqtrd	$$⊢\phi \to 1+\left(-\frac{C-B}{A-B}\right)=\frac{A-C}{A-B}$$
29	20 28	oveq12d	$$⊢\phi \to \frac{-\frac{C-B}{A-B}}{1+\left(-\frac{C-B}{A-B}\right)}=\frac{\frac{B-C}{A-B}}{\frac{A-C}{A-B}}$$
30	2 3	subcld	$$⊢\phi \to B-C\in ℂ$$
31	1 3	subcld	$$⊢\phi \to A-C\in ℂ$$
32	1 3 5	subne0d	$$⊢\phi \to A-C\ne 0$$
33	30 31 7 32 8	divcan7d	$$⊢\phi \to \frac{\frac{B-C}{A-B}}{\frac{A-C}{A-B}}=\frac{B-C}{A-C}$$
34	2 3 1 3 5	div2subd	$$⊢\phi \to \frac{B-C}{A-C}=\frac{C-B}{C-A}$$
35	29 33 34	3eqtrrd	$$⊢\phi \to \frac{C-B}{C-A}=\frac{-\frac{C-B}{A-B}}{1+\left(-\frac{C-B}{A-B}\right)}$$
36	35	eleq1d	$$⊢\phi \to \left(\frac{C-B}{C-A}\in \left(0,1\right)\leftrightarrow \frac{-\frac{C-B}{A-B}}{1+\left(-\frac{C-B}{A-B}\right)}\in \left(0,1\right)\right)$$
37	16 36	bitr4d	$$⊢\phi \to \left(-\frac{C-B}{A-B}\in {ℝ}^{+}\leftrightarrow \frac{C-B}{C-A}\in \left(0,1\right)\right)$$