Metamath Proof Explorer

Theorem ang180

Description: The sum of angles m A B C + m B C A + m C A B in a triangle adds up to either _pi or -u _pi , i.e. 180 degrees. (The sign is due to the two possible orientations of vertex arrangement and our signed notion of angle). This is Metamath 100 proof #27. (Contributed by Mario Carneiro, 23-Sep-2014)

Ref Expression
Hypothesis ang.1 
|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
Assertion ang180 
|- ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( ( ( ( C - B ) F ( A - B ) ) + ( ( A - C ) F ( B - C ) ) ) + ( ( B - A ) F ( C - A ) ) ) e. { -u _pi , _pi } )

Proof

Step Hyp Ref Expression
1 ang.1 
 |-  F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2 simpl3 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> C e. CC )
3 simpl2 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> B e. CC )
4 2 3 subcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( C - B ) e. CC )
5 simpr2 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> B =/= C )
6 5 necomd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> C =/= B )
7 2 3 6 subne0d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( C - B ) =/= 0 )
8 simpl1 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> A e. CC )
9 8 3 subcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( A - B ) e. CC )
10 simpr1 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> A =/= B )
11 8 3 10 subne0d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( A - B ) =/= 0 )
12 1 angneg 
 |-  ( ( ( ( C - B ) e. CC /\ ( C - B ) =/= 0 ) /\ ( ( A - B ) e. CC /\ ( A - B ) =/= 0 ) ) -> ( -u ( C - B ) F -u ( A - B ) ) = ( ( C - B ) F ( A - B ) ) )
13 4 7 9 11 12 syl22anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( -u ( C - B ) F -u ( A - B ) ) = ( ( C - B ) F ( A - B ) ) )
14 2 3 negsubdi2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> -u ( C - B ) = ( B - C ) )
15 3 2 8 nnncan2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( ( B - A ) - ( C - A ) ) = ( B - C ) )
16 14 15 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> -u ( C - B ) = ( ( B - A ) - ( C - A ) ) )
17 8 3 negsubdi2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> -u ( A - B ) = ( B - A ) )
18 16 17 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( -u ( C - B ) F -u ( A - B ) ) = ( ( ( B - A ) - ( C - A ) ) F ( B - A ) ) )
19 13 18 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( ( C - B ) F ( A - B ) ) = ( ( ( B - A ) - ( C - A ) ) F ( B - A ) ) )
20 8 2 subcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( A - C ) e. CC )
21 simpr3 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> A =/= C )
22 8 2 21 subne0d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( A - C ) =/= 0 )
23 3 2 subcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( B - C ) e. CC )
24 3 2 5 subne0d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( B - C ) =/= 0 )
25 1 angneg 
 |-  ( ( ( ( A - C ) e. CC /\ ( A - C ) =/= 0 ) /\ ( ( B - C ) e. CC /\ ( B - C ) =/= 0 ) ) -> ( -u ( A - C ) F -u ( B - C ) ) = ( ( A - C ) F ( B - C ) ) )
26 20 22 23 24 25 syl22anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( -u ( A - C ) F -u ( B - C ) ) = ( ( A - C ) F ( B - C ) ) )
27 8 2 negsubdi2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> -u ( A - C ) = ( C - A ) )
28 3 2 negsubdi2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> -u ( B - C ) = ( C - B ) )
29 2 3 8 nnncan2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( ( C - A ) - ( B - A ) ) = ( C - B ) )
30 28 29 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> -u ( B - C ) = ( ( C - A ) - ( B - A ) ) )
31 27 30 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( -u ( A - C ) F -u ( B - C ) ) = ( ( C - A ) F ( ( C - A ) - ( B - A ) ) ) )
32 26 31 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( ( A - C ) F ( B - C ) ) = ( ( C - A ) F ( ( C - A ) - ( B - A ) ) ) )
33 19 32 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( ( ( C - B ) F ( A - B ) ) + ( ( A - C ) F ( B - C ) ) ) = ( ( ( ( B - A ) - ( C - A ) ) F ( B - A ) ) + ( ( C - A ) F ( ( C - A ) - ( B - A ) ) ) ) )
34 33 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( ( ( ( C - B ) F ( A - B ) ) + ( ( A - C ) F ( B - C ) ) ) + ( ( B - A ) F ( C - A ) ) ) = ( ( ( ( ( B - A ) - ( C - A ) ) F ( B - A ) ) + ( ( C - A ) F ( ( C - A ) - ( B - A ) ) ) ) + ( ( B - A ) F ( C - A ) ) ) )
35 3 8 subcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( B - A ) e. CC )
36 10 necomd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> B =/= A )
37 3 8 36 subne0d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( B - A ) =/= 0 )
38 2 8 subcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( C - A ) e. CC )
39 21 necomd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> C =/= A )
40 2 8 39 subne0d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( C - A ) =/= 0 )
41 3 2 8 5 subneintr2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( B - A ) =/= ( C - A ) )
42 1 ang180lem5 
 |-  ( ( ( ( B - A ) e. CC /\ ( B - A ) =/= 0 ) /\ ( ( C - A ) e. CC /\ ( C - A ) =/= 0 ) /\ ( B - A ) =/= ( C - A ) ) -> ( ( ( ( ( B - A ) - ( C - A ) ) F ( B - A ) ) + ( ( C - A ) F ( ( C - A ) - ( B - A ) ) ) ) + ( ( B - A ) F ( C - A ) ) ) e. { -u _pi , _pi } )
43 35 37 38 40 41 42 syl221anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( ( ( ( ( B - A ) - ( C - A ) ) F ( B - A ) ) + ( ( C - A ) F ( ( C - A ) - ( B - A ) ) ) ) + ( ( B - A ) F ( C - A ) ) ) e. { -u _pi , _pi } )
44 34 43 eqeltrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ C e. CC ) /\ ( A =/= B /\ B =/= C /\ A =/= C ) ) -> ( ( ( ( C - B ) F ( A - B ) ) + ( ( A - C ) F ( B - C ) ) ) + ( ( B - A ) F ( C - A ) ) ) e. { -u _pi , _pi } )