Metamath Proof Explorer

Theorem angpined

Description: If the angle at ABC is _pi , then A is not equal to C . (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 angpined 
|- ( ph -> ( ( ( A - B ) F ( C - B ) ) = _pi -> A =/= 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 1rp 
 |-  1 e. RR+
9 1re 
 |-  1 e. RR
10 ax-1ne0 
 |-  1 =/= 0
11 rpneg 
 |-  ( ( 1 e. RR /\ 1 =/= 0 ) -> ( 1 e. RR+ <-> -. -u 1 e. RR+ ) )
12 9 10 11 mp2an 
 |-  ( 1 e. RR+ <-> -. -u 1 e. RR+ )
13 8 12 mpbi 
 |-  -. -u 1 e. RR+
14 2 3 subcld 
 |-  ( ph -> ( A - B ) e. CC )
15 14 adantr 
 |-  ( ( ph /\ C = A ) -> ( A - B ) e. CC )
16 2 3 5 subne0d 
 |-  ( ph -> ( A - B ) =/= 0 )
17 16 adantr 
 |-  ( ( ph /\ C = A ) -> ( A - B ) =/= 0 )
18 simpr 
 |-  ( ( ph /\ C = A ) -> C = A )
19 18 oveq1d 
 |-  ( ( ph /\ C = A ) -> ( C - B ) = ( A - B ) )
20 15 17 19 diveq1bd 
 |-  ( ( ph /\ C = A ) -> ( ( C - B ) / ( A - B ) ) = 1 )
21 20 adantlr 
 |-  ( ( ( ph /\ -u ( ( C - B ) / ( A - B ) ) e. RR+ ) /\ C = A ) -> ( ( C - B ) / ( A - B ) ) = 1 )
22 21 negeqd 
 |-  ( ( ( ph /\ -u ( ( C - B ) / ( A - B ) ) e. RR+ ) /\ C = A ) -> -u ( ( C - B ) / ( A - B ) ) = -u 1 )
23 simplr 
 |-  ( ( ( ph /\ -u ( ( C - B ) / ( A - B ) ) e. RR+ ) /\ C = A ) -> -u ( ( C - B ) / ( A - B ) ) e. RR+ )
24 22 23 eqeltrrd 
 |-  ( ( ( ph /\ -u ( ( C - B ) / ( A - B ) ) e. RR+ ) /\ C = A ) -> -u 1 e. RR+ )
25 24 ex 
 |-  ( ( ph /\ -u ( ( C - B ) / ( A - B ) ) e. RR+ ) -> ( C = A -> -u 1 e. RR+ ) )
26 25 necon3bd 
 |-  ( ( ph /\ -u ( ( C - B ) / ( A - B ) ) e. RR+ ) -> ( -. -u 1 e. RR+ -> C =/= A ) )
27 13 26 mpi 
 |-  ( ( ph /\ -u ( ( C - B ) / ( A - B ) ) e. RR+ ) -> C =/= A )
28 27 ex 
 |-  ( ph -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ -> C =/= A ) )
29 necom 
 |-  ( C =/= A <-> A =/= C )
30 28 29 imbitrdi 
 |-  ( ph -> ( -u ( ( C - B ) / ( A - B ) ) e. RR+ -> A =/= C ) )
31 7 30 sylbird 
 |-  ( ph -> ( ( ( A - B ) F ( C - B ) ) = _pi -> A =/= C ) )