Metamath Proof Explorer

Theorem angpieqvdlem

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

Ref Expression
Hypotheses angpieqvdlem.A 
|- ( ph -> A e. CC )
angpieqvdlem.B 
|- ( ph -> B e. CC )
angpieqvdlem.C 
|- ( ph -> C e. CC )
angpieqvdlem.AneB 
|- ( ph -> A =/= B )
angpieqvdlem.AneC 
|- ( ph -> A =/= C )
Assertion angpieqvdlem 
|- ( ph -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ <-> ( ( C - B ) / ( C - A ) ) e. ( 0 (,) 1 ) ) )

Proof

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