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 \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
	Assertion	ang180	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq B \land B \neq C \land A \neq C)) \to ((C - B) F (A - B)) + ((A - C) F (B - C)) + ((B - A) F (C - A)) \in \{- π, π\}$

Proof

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

Metamath Proof Explorer

Theorem ang180

Proof