Metamath Proof Explorer

Theorem angpieqvd

Description: The angle ABC is _pi iff B is a nontrivial convex combination of A and C , i.e., iff B is in the interior of the segment AC. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses angpieqvd.angdef 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
angpieqvd.A 
|- ( ph -> A e. CC )
angpieqvd.B 
|- ( ph -> B e. CC )
angpieqvd.C 
|- ( ph -> C e. CC )
angpieqvd.AneB 
|- ( ph -> A =/= B )
angpieqvd.BneC 
|- ( ph -> B =/= C )
Assertion angpieqvd 
|- ( ph -> ( ( ( A - B ) F ( C - B ) ) = _pi <-> E. w e. ( 0 (,) 1 ) B = ( ( w x. A ) + ( ( 1 - w ) x. C ) ) ) )

Proof

Step Hyp Ref Expression
1 angpieqvd.angdef 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 angpieqvd.A 
 |-  ( ph -> A e. CC )
3 angpieqvd.B 
 |-  ( ph -> B e. CC )
4 angpieqvd.C 
 |-  ( ph -> C e. CC )
5 angpieqvd.AneB 
 |-  ( ph -> A =/= B )
6 angpieqvd.BneC 
 |-  ( ph -> B =/= C )
7 1 2 3 4 5 6 angpieqvdlem2 
 |-  ( ph -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ <-> ( ( A - B ) F ( C - B ) ) = _pi ) )
8 7 biimpar 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> -u ( ( C - B ) / ( A - B ) ) e. RR+ )
9 2 adantr 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> A e. CC )
10 3 adantr 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> B e. CC )
11 4 adantr 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> C e. CC )
12 5 adantr 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> A =/= B )
13 1 2 3 4 5 6 angpined 
 |-  ( ph -> ( ( ( A - B ) F ( C - B ) ) = _pi -> A =/= C ) )
14 13 imp 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> A =/= C )
15 9 10 11 12 14 angpieqvdlem 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ <-> ( ( C - B ) / ( C - A ) ) e. ( 0 (,) 1 ) ) )
16 8 15 mpbid 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> ( ( C - B ) / ( C - A ) ) e. ( 0 (,) 1 ) )
17 4 3 subcld 
 |-  ( ph -> ( C - B ) e. CC )
18 17 adantr 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> ( C - B ) e. CC )
19 4 2 subcld 
 |-  ( ph -> ( C - A ) e. CC )
20 19 adantr 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> ( C - A ) e. CC )
21 14 necomd 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> C =/= A )
22 11 9 21 subne0d 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> ( C - A ) =/= 0 )
23 18 20 22 divcan1d 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> ( ( ( C - B ) / ( C - A ) ) x. ( C - A ) ) = ( C - B ) )
24 23 eqcomd 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> ( C - B ) = ( ( ( C - B ) / ( C - A ) ) x. ( C - A ) ) )
25 18 20 22 divcld 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> ( ( C - B ) / ( C - A ) ) e. CC )
26 9 10 11 25 affineequiv 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> ( B = ( ( ( ( C - B ) / ( C - A ) ) x. A ) + ( ( 1 - ( ( C - B ) / ( C - A ) ) ) x. C ) ) <-> ( C - B ) = ( ( ( C - B ) / ( C - A ) ) x. ( C - A ) ) ) )
27 24 26 mpbird 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> B = ( ( ( ( C - B ) / ( C - A ) ) x. A ) + ( ( 1 - ( ( C - B ) / ( C - A ) ) ) x. C ) ) )
28 oveq1 
 |-  ( w = ( ( C - B ) / ( C - A ) ) -> ( w x. A ) = ( ( ( C - B ) / ( C - A ) ) x. A ) )
29 oveq2 
 |-  ( w = ( ( C - B ) / ( C - A ) ) -> ( 1 - w ) = ( 1 - ( ( C - B ) / ( C - A ) ) ) )
30 29 oveq1d 
 |-  ( w = ( ( C - B ) / ( C - A ) ) -> ( ( 1 - w ) x. C ) = ( ( 1 - ( ( C - B ) / ( C - A ) ) ) x. C ) )
31 28 30 oveq12d 
 |-  ( w = ( ( C - B ) / ( C - A ) ) -> ( ( w x. A ) + ( ( 1 - w ) x. C ) ) = ( ( ( ( C - B ) / ( C - A ) ) x. A ) + ( ( 1 - ( ( C - B ) / ( C - A ) ) ) x. C ) ) )
32 31 rspceeqv 
 |-  ( ( ( ( C - B ) / ( C - A ) ) e. ( 0 (,) 1 ) /\ B = ( ( ( ( C - B ) / ( C - A ) ) x. A ) + ( ( 1 - ( ( C - B ) / ( C - A ) ) ) x. C ) ) ) -> E. w e. ( 0 (,) 1 ) B = ( ( w x. A ) + ( ( 1 - w ) x. C ) ) )
33 16 27 32 syl2anc 
 |-  ( ( ph /\ ( ( A - B ) F ( C - B ) ) = _pi ) -> E. w e. ( 0 (,) 1 ) B = ( ( w x. A ) + ( ( 1 - w ) x. C ) ) )
34 33 ex 
 |-  ( ph -> ( ( ( A - B ) F ( C - B ) ) = _pi -> E. w e. ( 0 (,) 1 ) B = ( ( w x. A ) + ( ( 1 - w ) x. C ) ) ) )
35 2 adantr 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) ) -> A e. CC )
36 3 adantr 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) ) -> B e. CC )
37 4 adantr 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) ) -> C e. CC )
38 simpr 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) ) -> w e. ( 0 (,) 1 ) )
39 elioore 
 |-  ( w e. ( 0 (,) 1 ) -> w e. RR )
40 recn 
 |-  ( w e. RR -> w e. CC )
41 38 39 40 3syl 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) ) -> w e. CC )
42 35 36 37 41 affineequiv 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) ) -> ( B = ( ( w x. A ) + ( ( 1 - w ) x. C ) ) <-> ( C - B ) = ( w x. ( C - A ) ) ) )
43 simp3 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> ( C - B ) = ( w x. ( C - A ) ) )
44 17 3ad2ant1 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> ( C - B ) e. CC )
45 41 3adant3 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> w e. CC )
46 19 3ad2ant1 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> ( C - A ) e. CC )
47 6 necomd 
 |-  ( ph -> C =/= B )
48 4 3 47 subne0d 
 |-  ( ph -> ( C - B ) =/= 0 )
49 48 3ad2ant1 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> ( C - B ) =/= 0 )
50 43 49 eqnetrrd 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> ( w x. ( C - A ) ) =/= 0 )
51 45 46 50 mulne0bbd 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> ( C - A ) =/= 0 )
52 44 45 46 51 divmul3d 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> ( ( ( C - B ) / ( C - A ) ) = w <-> ( C - B ) = ( w x. ( C - A ) ) ) )
53 43 52 mpbird 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> ( ( C - B ) / ( C - A ) ) = w )
54 simp2 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> w e. ( 0 (,) 1 ) )
55 53 54 eqeltrd 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> ( ( C - B ) / ( C - A ) ) e. ( 0 (,) 1 ) )
56 2 3ad2ant1 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> A e. CC )
57 3 3ad2ant1 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> B e. CC )
58 4 3ad2ant1 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> C e. CC )
59 5 3ad2ant1 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> A =/= B )
60 58 56 51 subne0ad 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> C =/= A )
61 60 necomd 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> A =/= C )
62 56 57 58 59 61 angpieqvdlem 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ <-> ( ( C - B ) / ( C - A ) ) e. ( 0 (,) 1 ) ) )
63 55 62 mpbird 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> -u ( ( C - B ) / ( A - B ) ) e. RR+ )
64 6 3ad2ant1 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> B =/= C )
65 1 56 57 58 59 64 angpieqvdlem2 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ <-> ( ( A - B ) F ( C - B ) ) = _pi ) )
66 63 65 mpbid 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) /\ ( C - B ) = ( w x. ( C - A ) ) ) -> ( ( A - B ) F ( C - B ) ) = _pi )
67 66 3expia 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) ) -> ( ( C - B ) = ( w x. ( C - A ) ) -> ( ( A - B ) F ( C - B ) ) = _pi ) )
68 42 67 sylbid 
 |-  ( ( ph /\ w e. ( 0 (,) 1 ) ) -> ( B = ( ( w x. A ) + ( ( 1 - w ) x. C ) ) -> ( ( A - B ) F ( C - B ) ) = _pi ) )
69 68 rexlimdva 
 |-  ( ph -> ( E. w e. ( 0 (,) 1 ) B = ( ( w x. A ) + ( ( 1 - w ) x. C ) ) -> ( ( A - B ) F ( C - B ) ) = _pi ) )
70 34 69 impbid 
 |-  ( ph -> ( ( ( A - B ) F ( C - B ) ) = _pi <-> E. w e. ( 0 (,) 1 ) B = ( ( w x. A ) + ( ( 1 - w ) x. C ) ) ) )