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 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ) ) → ( ( ( ( 𝐶 − 𝐵 ) 𝐹 ( 𝐴 − 𝐵 ) ) + ( ( 𝐴 − 𝐶 ) 𝐹 ( 𝐵 − 𝐶 ) ) ) + ( ( 𝐵 − 𝐴 ) 𝐹 ( 𝐶 − 𝐴 ) ) ) ∈ { - π , π } )