# 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}=\left({x}\in \left(ℂ\setminus \left\{0\right\}\right),{y}\in \left(ℂ\setminus \left\{0\right\}\right)⟼\Im \left(\mathrm{log}\left(\frac{{y}}{{x}}\right)\right)\right)$
Assertion ang180 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {B}\wedge {B}\ne {C}\wedge {A}\ne {C}\right)\right)\to \left(\left({C}-{B}\right){F}\left({A}-{B}\right)\right)+\left(\left({A}-{C}\right){F}\left({B}-{C}\right)\right)+\left(\left({B}-{A}\right){F}\left({C}-{A}\right)\right)\in \left\{-\mathrm{\pi },\mathrm{\pi }\right\}$

### Proof

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