Theorem angpieqvdlem

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

	Ref	Expression
Hypotheses	angpieqvdlem.A	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	angpieqvdlem.B	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	angpieqvdlem.C	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	angpieqvdlem.AneB	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	angpieqvdlem.AneC	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
Assertion	angpieqvdlem	⊢ ( 𝜑 → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ↔ ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ∈ ( 0 (,) 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		angpieqvdlem.A	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		angpieqvdlem.B	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		angpieqvdlem.C	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4		angpieqvdlem.AneB	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
5		angpieqvdlem.AneC	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
6	3 2	subcld	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ∈ ℂ )
7	1 2	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
8	1 2 4	subne0d	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ≠ 0 )
9	6 7 8	divcld	⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℂ )
10	9	negcld	⊢ ( 𝜑 → - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℂ )
11		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
12	5	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
13	3 1 2 12	subneintr2d	⊢ ( 𝜑 → ( 𝐶 − 𝐵 ) ≠ ( 𝐴 − 𝐵 ) )
14	6 7 8 13	divne1d	⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ≠ 1 )
15	9 11 14	negned	⊢ ( 𝜑 → - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ≠ - 1 )
16	10 15	xov1plusxeqvd	⊢ ( 𝜑 → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ↔ ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) / ( 1 + - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) ) ∈ ( 0 (,) 1 ) ) )
17	6 7 8	divnegd	⊢ ( 𝜑 → - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) = ( - ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) )
18	3 2	negsubdi2d	⊢ ( 𝜑 → - ( 𝐶 − 𝐵 ) = ( 𝐵 − 𝐶 ) )
19	18	oveq1d	⊢ ( 𝜑 → ( - ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) = ( ( 𝐵 − 𝐶 ) / ( 𝐴 − 𝐵 ) ) )
20	17 19	eqtrd	⊢ ( 𝜑 → - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) = ( ( 𝐵 − 𝐶 ) / ( 𝐴 − 𝐵 ) ) )
21	7 8	dividd	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) = 1 )
22	21	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) − ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) = ( 1 − ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) )
23	7 6 7 8	divsubdird	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) − ( 𝐶 − 𝐵 ) ) / ( 𝐴 − 𝐵 ) ) = ( ( ( 𝐴 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) − ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) )
24	11 9	negsubd	⊢ ( 𝜑 → ( 1 + - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) = ( 1 − ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) )
25	22 23 24	3eqtr4rd	⊢ ( 𝜑 → ( 1 + - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) = ( ( ( 𝐴 − 𝐵 ) − ( 𝐶 − 𝐵 ) ) / ( 𝐴 − 𝐵 ) ) )
26	1 3 2	nnncan2d	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) − ( 𝐶 − 𝐵 ) ) = ( 𝐴 − 𝐶 ) )
27	26	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) − ( 𝐶 − 𝐵 ) ) / ( 𝐴 − 𝐵 ) ) = ( ( 𝐴 − 𝐶 ) / ( 𝐴 − 𝐵 ) ) )
28	25 27	eqtrd	⊢ ( 𝜑 → ( 1 + - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) = ( ( 𝐴 − 𝐶 ) / ( 𝐴 − 𝐵 ) ) )
29	20 28	oveq12d	⊢ ( 𝜑 → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) / ( 1 + - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) ) = ( ( ( 𝐵 − 𝐶 ) / ( 𝐴 − 𝐵 ) ) / ( ( 𝐴 − 𝐶 ) / ( 𝐴 − 𝐵 ) ) ) )
30	2 3	subcld	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) ∈ ℂ )
31	1 3	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ∈ ℂ )
32	1 3 5	subne0d	⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) ≠ 0 )
33	30 31 7 32 8	divcan7d	⊢ ( 𝜑 → ( ( ( 𝐵 − 𝐶 ) / ( 𝐴 − 𝐵 ) ) / ( ( 𝐴 − 𝐶 ) / ( 𝐴 − 𝐵 ) ) ) = ( ( 𝐵 − 𝐶 ) / ( 𝐴 − 𝐶 ) ) )
34	2 3 1 3 5	div2subd	⊢ ( 𝜑 → ( ( 𝐵 − 𝐶 ) / ( 𝐴 − 𝐶 ) ) = ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) )
35	29 33 34	3eqtrrd	⊢ ( 𝜑 → ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) = ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) / ( 1 + - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) ) )
36	35	eleq1d	⊢ ( 𝜑 → ( ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ∈ ( 0 (,) 1 ) ↔ ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) / ( 1 + - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ) ) ∈ ( 0 (,) 1 ) ) )
37	16 36	bitr4d	⊢ ( 𝜑 → ( - ( ( 𝐶 − 𝐵 ) / ( 𝐴 − 𝐵 ) ) ∈ ℝ+ ↔ ( ( 𝐶 − 𝐵 ) / ( 𝐶 − 𝐴 ) ) ∈ ( 0 (,) 1 ) ) )