lawcos

Description: Law of cosines (also known as the Al-Kashi theorem or the generalized Pythagorean theorem, or the cosine formula or cosine rule). Given three distinct points A, B, and C, prove a relationship between their segment lengths. This theorem is expressed using the complex number plane as a plane, where F is the signed angle construct (as used in ang180 ), X is the distance of line segment BC, Y is the distance of line segment AC, Z is the distance of line segment AB, and O is the signed angle m/__ BCA on the complex plane. We translate triangle ABC to move C to the origin (C-C), B to U=(B-C), and A to V=(A-C), then use lemma lawcoslem1 to prove this algebraically simpler case. The Metamath convention is to use a signed angle; in this case the sign doesn't matter because we use the cosine of the angle (see cosneg ). The Pythagorean theorem pythag is a special case of the law of cosines. The theorem's expression and approach were suggested by Mario Carneiro. This is Metamath 100 proof #94. (Contributed by David A. Wheeler, 12-Jun-2015)

	Ref	Expression
Hypotheses	lawcos.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
	lawcos.2	$⊢ X = \|B - C\|$
	lawcos.3	$⊢ Y = \|A - C\|$
	lawcos.4	$⊢ Z = \|A - B\|$
	lawcos.5	$⊢ O = (B - C) F (A - C)$
Assertion	lawcos	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to Z^{2} = X^{2} + Y^{2} - 2 X Y \cos O$

Proof

Step	Hyp	Ref	Expression
1		lawcos.1	$⊢ F = (x \in (ℂ ∖ \{0\}), y \in (ℂ ∖ \{0\}) ⟼ ℑ (\log (\frac{y}{x})))$
2		lawcos.2	$⊢ X = \|B - C\|$
3		lawcos.3	$⊢ Y = \|A - C\|$
4		lawcos.4	$⊢ Z = \|A - B\|$
5		lawcos.5	$⊢ O = (B - C) F (A - C)$
6		subcl	$⊢ (A \in ℂ \land C \in ℂ) \to A - C \in ℂ$
7	6	3adant2	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A - C \in ℂ$
8	7	adantr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to A - C \in ℂ$
9		subcl	$⊢ (B \in ℂ \land C \in ℂ) \to B - C \in ℂ$
10	9	3adant1	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to B - C \in ℂ$
11	10	adantr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to B - C \in ℂ$
12		subeq0	$⊢ (A \in ℂ \land C \in ℂ) \to (A - C = 0 \leftrightarrow A = C)$
13	12	necon3bid	$⊢ (A \in ℂ \land C \in ℂ) \to (A - C \neq 0 \leftrightarrow A \neq C)$
14	13	bicomd	$⊢ (A \in ℂ \land C \in ℂ) \to (A \neq C \leftrightarrow A - C \neq 0)$
15	14	3adant2	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to (A \neq C \leftrightarrow A - C \neq 0)$
16	15	biimpa	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land A \neq C) \to A - C \neq 0$
17	16	adantrr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to A - C \neq 0$
18		subeq0	$⊢ (B \in ℂ \land C \in ℂ) \to (B - C = 0 \leftrightarrow B = C)$
19	18	necon3bid	$⊢ (B \in ℂ \land C \in ℂ) \to (B - C \neq 0 \leftrightarrow B \neq C)$
20	19	bicomd	$⊢ (B \in ℂ \land C \in ℂ) \to (B \neq C \leftrightarrow B - C \neq 0)$
21	20	3adant1	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to (B \neq C \leftrightarrow B - C \neq 0)$
22	21	biimpa	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land B \neq C) \to B - C \neq 0$
23	22	adantrl	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to B - C \neq 0$
24	8 11 17 23	lawcoslem1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to {\|A - C - (B - C)\|}^{2} = {\|A - C\|}^{2} + {\|B - C\|}^{2} - 2 \|A - C\| \|B - C\| (\frac{ℜ (\frac{A - C}{B - C})}{\|\frac{A - C}{B - C}\|})$
25		nnncan2	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A - C - (B - C) = A - B$
26	25	fveq2d	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to \|A - C - (B - C)\| = \|A - B\|$
27	4 26	eqtr4id	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to Z = \|A - C - (B - C)\|$
28	27	oveq1d	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to Z^{2} = {\|A - C - (B - C)\|}^{2}$
29	28	adantr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to Z^{2} = {\|A - C - (B - C)\|}^{2}$
30	2	oveq1i	$⊢ X^{2} = {\|B - C\|}^{2}$
31	3	oveq1i	$⊢ Y^{2} = {\|A - C\|}^{2}$
32	30 31	oveq12i	$⊢ X^{2} + Y^{2} = {\|B - C\|}^{2} + {\|A - C\|}^{2}$
33	8	abscld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \|A - C\| \in ℝ$
34	33	recnd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \|A - C\| \in ℂ$
35	34	sqcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to {\|A - C\|}^{2} \in ℂ$
36	11	abscld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \|B - C\| \in ℝ$
37	36	recnd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \|B - C\| \in ℂ$
38	37	sqcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to {\|B - C\|}^{2} \in ℂ$
39	35 38	addcomd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to {\|A - C\|}^{2} + {\|B - C\|}^{2} = {\|B - C\|}^{2} + {\|A - C\|}^{2}$
40	32 39	eqtr4id	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to X^{2} + Y^{2} = {\|A - C\|}^{2} + {\|B - C\|}^{2}$
41	2 3	oveq12i	$⊢ X Y = \|B - C\| \|A - C\|$
42	34 37	mulcomd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \|A - C\| \|B - C\| = \|B - C\| \|A - C\|$
43	41 42	eqtr4id	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to X Y = \|A - C\| \|B - C\|$
44	5	fveq2i	$⊢ \cos O = \cos ((B - C) F (A - C))$
45	1 11 23 8 17	angvald	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to (B - C) F (A - C) = ℑ (\log (\frac{A - C}{B - C}))$
46	45	fveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \cos ((B - C) F (A - C)) = \cos ℑ (\log (\frac{A - C}{B - C}))$
47	44 46	syl5eq	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \cos O = \cos ℑ (\log (\frac{A - C}{B - C}))$
48	8 11 23	divcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \frac{A - C}{B - C} \in ℂ$
49	8 11 17 23	divne0d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \frac{A - C}{B - C} \neq 0$
50	48 49	logcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \log (\frac{A - C}{B - C}) \in ℂ$
51	50	imcld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to ℑ (\log (\frac{A - C}{B - C})) \in ℝ$
52		recosval	$⊢ ℑ (\log (\frac{A - C}{B - C})) \in ℝ \to \cos ℑ (\log (\frac{A - C}{B - C})) = ℜ (e^{i ℑ (\log (\frac{A - C}{B - C}))})$
53	51 52	syl	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \cos ℑ (\log (\frac{A - C}{B - C})) = ℜ (e^{i ℑ (\log (\frac{A - C}{B - C}))})$
54	47 53	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \cos O = ℜ (e^{i ℑ (\log (\frac{A - C}{B - C}))})$
55		efiarg	$⊢ (\frac{A - C}{B - C} \in ℂ \land \frac{A - C}{B - C} \neq 0) \to e^{i ℑ (\log (\frac{A - C}{B - C}))} = \frac{\frac{A - C}{B - C}}{\|\frac{A - C}{B - C}\|}$
56	48 49 55	syl2anc	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to e^{i ℑ (\log (\frac{A - C}{B - C}))} = \frac{\frac{A - C}{B - C}}{\|\frac{A - C}{B - C}\|}$
57	56	fveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to ℜ (e^{i ℑ (\log (\frac{A - C}{B - C}))}) = ℜ (\frac{\frac{A - C}{B - C}}{\|\frac{A - C}{B - C}\|})$
58	48	abscld	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \|\frac{A - C}{B - C}\| \in ℝ$
59	48 49	absne0d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \|\frac{A - C}{B - C}\| \neq 0$
60	58 48 59	redivd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to ℜ (\frac{\frac{A - C}{B - C}}{\|\frac{A - C}{B - C}\|}) = \frac{ℜ (\frac{A - C}{B - C})}{\|\frac{A - C}{B - C}\|}$
61	54 57 60	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to \cos O = \frac{ℜ (\frac{A - C}{B - C})}{\|\frac{A - C}{B - C}\|}$
62	43 61	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to X Y \cos O = \|A - C\| \|B - C\| (\frac{ℜ (\frac{A - C}{B - C})}{\|\frac{A - C}{B - C}\|})$
63	62	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to 2 X Y \cos O = 2 \|A - C\| \|B - C\| (\frac{ℜ (\frac{A - C}{B - C})}{\|\frac{A - C}{B - C}\|})$
64	40 63	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to X^{2} + Y^{2} - 2 X Y \cos O = {\|A - C\|}^{2} + {\|B - C\|}^{2} - 2 \|A - C\| \|B - C\| (\frac{ℜ (\frac{A - C}{B - C})}{\|\frac{A - C}{B - C}\|})$
65	24 29 64	3eqtr4d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (A \neq C \land B \neq C)) \to Z^{2} = X^{2} + Y^{2} - 2 X Y \cos O$

Metamath Proof Explorer

Theorem lawcos

Proof