# 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 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
Assertion ang180 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( ( ( ( 𝐶𝐵 ) 𝐹 ( 𝐴𝐵 ) ) + ( ( 𝐴𝐶 ) 𝐹 ( 𝐵𝐶 ) ) ) + ( ( 𝐵𝐴 ) 𝐹 ( 𝐶𝐴 ) ) ) ∈ { - π , π } )

### Proof

Step Hyp Ref Expression
1 ang.1 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) )
2 simpl3 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → 𝐶 ∈ ℂ )
3 simpl2 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → 𝐵 ∈ ℂ )
4 2 3 subcld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐶𝐵 ) ∈ ℂ )
5 simpr2 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → 𝐵𝐶 )
6 5 necomd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → 𝐶𝐵 )
7 2 3 6 subne0d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐶𝐵 ) ≠ 0 )
8 simpl1 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → 𝐴 ∈ ℂ )
9 8 3 subcld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐴𝐵 ) ∈ ℂ )
10 simpr1 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → 𝐴𝐵 )
11 8 3 10 subne0d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐴𝐵 ) ≠ 0 )
12 1 angneg ( ( ( ( 𝐶𝐵 ) ∈ ℂ ∧ ( 𝐶𝐵 ) ≠ 0 ) ∧ ( ( 𝐴𝐵 ) ∈ ℂ ∧ ( 𝐴𝐵 ) ≠ 0 ) ) → ( - ( 𝐶𝐵 ) 𝐹 - ( 𝐴𝐵 ) ) = ( ( 𝐶𝐵 ) 𝐹 ( 𝐴𝐵 ) ) )
13 4 7 9 11 12 syl22anc ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( - ( 𝐶𝐵 ) 𝐹 - ( 𝐴𝐵 ) ) = ( ( 𝐶𝐵 ) 𝐹 ( 𝐴𝐵 ) ) )
14 2 3 negsubdi2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → - ( 𝐶𝐵 ) = ( 𝐵𝐶 ) )
15 3 2 8 nnncan2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( ( 𝐵𝐴 ) − ( 𝐶𝐴 ) ) = ( 𝐵𝐶 ) )
16 14 15 eqtr4d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → - ( 𝐶𝐵 ) = ( ( 𝐵𝐴 ) − ( 𝐶𝐴 ) ) )
17 8 3 negsubdi2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → - ( 𝐴𝐵 ) = ( 𝐵𝐴 ) )
18 16 17 oveq12d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( - ( 𝐶𝐵 ) 𝐹 - ( 𝐴𝐵 ) ) = ( ( ( 𝐵𝐴 ) − ( 𝐶𝐴 ) ) 𝐹 ( 𝐵𝐴 ) ) )
19 13 18 eqtr3d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( ( 𝐶𝐵 ) 𝐹 ( 𝐴𝐵 ) ) = ( ( ( 𝐵𝐴 ) − ( 𝐶𝐴 ) ) 𝐹 ( 𝐵𝐴 ) ) )
20 8 2 subcld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐴𝐶 ) ∈ ℂ )
21 simpr3 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → 𝐴𝐶 )
22 8 2 21 subne0d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐴𝐶 ) ≠ 0 )
23 3 2 subcld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐵𝐶 ) ∈ ℂ )
24 3 2 5 subne0d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐵𝐶 ) ≠ 0 )
25 1 angneg ( ( ( ( 𝐴𝐶 ) ∈ ℂ ∧ ( 𝐴𝐶 ) ≠ 0 ) ∧ ( ( 𝐵𝐶 ) ∈ ℂ ∧ ( 𝐵𝐶 ) ≠ 0 ) ) → ( - ( 𝐴𝐶 ) 𝐹 - ( 𝐵𝐶 ) ) = ( ( 𝐴𝐶 ) 𝐹 ( 𝐵𝐶 ) ) )
26 20 22 23 24 25 syl22anc ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( - ( 𝐴𝐶 ) 𝐹 - ( 𝐵𝐶 ) ) = ( ( 𝐴𝐶 ) 𝐹 ( 𝐵𝐶 ) ) )
27 8 2 negsubdi2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → - ( 𝐴𝐶 ) = ( 𝐶𝐴 ) )
28 3 2 negsubdi2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → - ( 𝐵𝐶 ) = ( 𝐶𝐵 ) )
29 2 3 8 nnncan2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( ( 𝐶𝐴 ) − ( 𝐵𝐴 ) ) = ( 𝐶𝐵 ) )
30 28 29 eqtr4d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → - ( 𝐵𝐶 ) = ( ( 𝐶𝐴 ) − ( 𝐵𝐴 ) ) )
31 27 30 oveq12d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( - ( 𝐴𝐶 ) 𝐹 - ( 𝐵𝐶 ) ) = ( ( 𝐶𝐴 ) 𝐹 ( ( 𝐶𝐴 ) − ( 𝐵𝐴 ) ) ) )
32 26 31 eqtr3d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( ( 𝐴𝐶 ) 𝐹 ( 𝐵𝐶 ) ) = ( ( 𝐶𝐴 ) 𝐹 ( ( 𝐶𝐴 ) − ( 𝐵𝐴 ) ) ) )
33 19 32 oveq12d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( ( ( 𝐶𝐵 ) 𝐹 ( 𝐴𝐵 ) ) + ( ( 𝐴𝐶 ) 𝐹 ( 𝐵𝐶 ) ) ) = ( ( ( ( 𝐵𝐴 ) − ( 𝐶𝐴 ) ) 𝐹 ( 𝐵𝐴 ) ) + ( ( 𝐶𝐴 ) 𝐹 ( ( 𝐶𝐴 ) − ( 𝐵𝐴 ) ) ) ) )
34 33 oveq1d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( ( ( ( 𝐶𝐵 ) 𝐹 ( 𝐴𝐵 ) ) + ( ( 𝐴𝐶 ) 𝐹 ( 𝐵𝐶 ) ) ) + ( ( 𝐵𝐴 ) 𝐹 ( 𝐶𝐴 ) ) ) = ( ( ( ( ( 𝐵𝐴 ) − ( 𝐶𝐴 ) ) 𝐹 ( 𝐵𝐴 ) ) + ( ( 𝐶𝐴 ) 𝐹 ( ( 𝐶𝐴 ) − ( 𝐵𝐴 ) ) ) ) + ( ( 𝐵𝐴 ) 𝐹 ( 𝐶𝐴 ) ) ) )
35 3 8 subcld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐵𝐴 ) ∈ ℂ )
36 10 necomd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → 𝐵𝐴 )
37 3 8 36 subne0d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐵𝐴 ) ≠ 0 )
38 2 8 subcld ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐶𝐴 ) ∈ ℂ )
39 21 necomd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → 𝐶𝐴 )
40 2 8 39 subne0d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐶𝐴 ) ≠ 0 )
41 3 2 8 5 subneintr2d ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( 𝐵𝐴 ) ≠ ( 𝐶𝐴 ) )
42 1 ang180lem5 ( ( ( ( 𝐵𝐴 ) ∈ ℂ ∧ ( 𝐵𝐴 ) ≠ 0 ) ∧ ( ( 𝐶𝐴 ) ∈ ℂ ∧ ( 𝐶𝐴 ) ≠ 0 ) ∧ ( 𝐵𝐴 ) ≠ ( 𝐶𝐴 ) ) → ( ( ( ( ( 𝐵𝐴 ) − ( 𝐶𝐴 ) ) 𝐹 ( 𝐵𝐴 ) ) + ( ( 𝐶𝐴 ) 𝐹 ( ( 𝐶𝐴 ) − ( 𝐵𝐴 ) ) ) ) + ( ( 𝐵𝐴 ) 𝐹 ( 𝐶𝐴 ) ) ) ∈ { - π , π } )
43 35 37 38 40 41 42 syl221anc ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( ( ( ( ( 𝐵𝐴 ) − ( 𝐶𝐴 ) ) 𝐹 ( 𝐵𝐴 ) ) + ( ( 𝐶𝐴 ) 𝐹 ( ( 𝐶𝐴 ) − ( 𝐵𝐴 ) ) ) ) + ( ( 𝐵𝐴 ) 𝐹 ( 𝐶𝐴 ) ) ) ∈ { - π , π } )
44 34 43 eqeltrd ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴𝐵𝐵𝐶𝐴𝐶 ) ) → ( ( ( ( 𝐶𝐵 ) 𝐹 ( 𝐴𝐵 ) ) + ( ( 𝐴𝐶 ) 𝐹 ( 𝐵𝐶 ) ) ) + ( ( 𝐵𝐴 ) 𝐹 ( 𝐶𝐴 ) ) ) ∈ { - π , π } )