Metamath Proof Explorer


Theorem 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 0 , y 0 log 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 B C A C B C Z 2 = X 2 + Y 2 - 2 X Y cos O

Proof

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