# 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}=\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)$
lawcos.2 ${⊢}{X}=\left|{B}-{C}\right|$
lawcos.3 ${⊢}{Y}=\left|{A}-{C}\right|$
lawcos.4 ${⊢}{Z}=\left|{A}-{B}\right|$
lawcos.5 ${⊢}{O}=\left({B}-{C}\right){F}\left({A}-{C}\right)$
Assertion lawcos ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left({A}\ne {C}\wedge {B}\ne {C}\right)\right)\to {{Z}}^{2}={{X}}^{2}+{{Y}}^{2}-2{X}{Y}\mathrm{cos}{O}$

### Proof

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