# Metamath Proof Explorer

## Theorem ssscongptld

Description: If two triangles have equal sides, one angle in one triangle has the same cosine as the corresponding angle in the other triangle. This is a partial form of the SSS congruence theorem.

This theorem is proven by using lawcos on both triangles to express one side in terms of the other two, and then equating these expressions and reducing this algebraically to get an equality of cosines of angles. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses ssscongptld.angdef ${⊢}{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)$
ssscongptld.1 ${⊢}{\phi }\to {A}\in ℂ$
ssscongptld.2 ${⊢}{\phi }\to {B}\in ℂ$
ssscongptld.3 ${⊢}{\phi }\to {C}\in ℂ$
ssscongptld.4 ${⊢}{\phi }\to {D}\in ℂ$
ssscongptld.5 ${⊢}{\phi }\to {E}\in ℂ$
ssscongptld.6 ${⊢}{\phi }\to {G}\in ℂ$
ssscongptld.7 ${⊢}{\phi }\to {A}\ne {B}$
ssscongptld.8 ${⊢}{\phi }\to {B}\ne {C}$
ssscongptld.9 ${⊢}{\phi }\to {D}\ne {E}$
ssscongptld.10 ${⊢}{\phi }\to {E}\ne {G}$
ssscongptld.11 ${⊢}{\phi }\to \left|{A}-{B}\right|=\left|{D}-{E}\right|$
ssscongptld.12 ${⊢}{\phi }\to \left|{B}-{C}\right|=\left|{E}-{G}\right|$
ssscongptld.13 ${⊢}{\phi }\to \left|{C}-{A}\right|=\left|{G}-{D}\right|$
Assertion ssscongptld ${⊢}{\phi }\to \mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)=\mathrm{cos}\left(\left({D}-{E}\right){F}\left({G}-{E}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ssscongptld.angdef ${⊢}{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 ssscongptld.1 ${⊢}{\phi }\to {A}\in ℂ$
3 ssscongptld.2 ${⊢}{\phi }\to {B}\in ℂ$
4 ssscongptld.3 ${⊢}{\phi }\to {C}\in ℂ$
5 ssscongptld.4 ${⊢}{\phi }\to {D}\in ℂ$
6 ssscongptld.5 ${⊢}{\phi }\to {E}\in ℂ$
7 ssscongptld.6 ${⊢}{\phi }\to {G}\in ℂ$
8 ssscongptld.7 ${⊢}{\phi }\to {A}\ne {B}$
9 ssscongptld.8 ${⊢}{\phi }\to {B}\ne {C}$
10 ssscongptld.9 ${⊢}{\phi }\to {D}\ne {E}$
11 ssscongptld.10 ${⊢}{\phi }\to {E}\ne {G}$
12 ssscongptld.11 ${⊢}{\phi }\to \left|{A}-{B}\right|=\left|{D}-{E}\right|$
13 ssscongptld.12 ${⊢}{\phi }\to \left|{B}-{C}\right|=\left|{E}-{G}\right|$
14 ssscongptld.13 ${⊢}{\phi }\to \left|{C}-{A}\right|=\left|{G}-{D}\right|$
15 negpitopissre ${⊢}\left(-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℝ$
16 ax-resscn ${⊢}ℝ\subseteq ℂ$
17 15 16 sstri ${⊢}\left(-\mathrm{\pi },\mathrm{\pi }\right]\subseteq ℂ$
18 2 3 subcld ${⊢}{\phi }\to {A}-{B}\in ℂ$
19 2 3 8 subne0d ${⊢}{\phi }\to {A}-{B}\ne 0$
20 4 3 subcld ${⊢}{\phi }\to {C}-{B}\in ℂ$
21 9 necomd ${⊢}{\phi }\to {C}\ne {B}$
22 4 3 21 subne0d ${⊢}{\phi }\to {C}-{B}\ne 0$
23 1 18 19 20 22 angcld ${⊢}{\phi }\to \left({A}-{B}\right){F}\left({C}-{B}\right)\in \left(-\mathrm{\pi },\mathrm{\pi }\right]$
24 17 23 sseldi ${⊢}{\phi }\to \left({A}-{B}\right){F}\left({C}-{B}\right)\in ℂ$
25 24 coscld ${⊢}{\phi }\to \mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)\in ℂ$
26 5 6 subcld ${⊢}{\phi }\to {D}-{E}\in ℂ$
27 5 6 10 subne0d ${⊢}{\phi }\to {D}-{E}\ne 0$
28 7 6 subcld ${⊢}{\phi }\to {G}-{E}\in ℂ$
29 11 necomd ${⊢}{\phi }\to {G}\ne {E}$
30 7 6 29 subne0d ${⊢}{\phi }\to {G}-{E}\ne 0$
31 1 26 27 28 30 angcld ${⊢}{\phi }\to \left({D}-{E}\right){F}\left({G}-{E}\right)\in \left(-\mathrm{\pi },\mathrm{\pi }\right]$
32 17 31 sseldi ${⊢}{\phi }\to \left({D}-{E}\right){F}\left({G}-{E}\right)\in ℂ$
33 32 coscld ${⊢}{\phi }\to \mathrm{cos}\left(\left({D}-{E}\right){F}\left({G}-{E}\right)\right)\in ℂ$
34 26 abscld ${⊢}{\phi }\to \left|{D}-{E}\right|\in ℝ$
35 34 recnd ${⊢}{\phi }\to \left|{D}-{E}\right|\in ℂ$
36 28 abscld ${⊢}{\phi }\to \left|{G}-{E}\right|\in ℝ$
37 36 recnd ${⊢}{\phi }\to \left|{G}-{E}\right|\in ℂ$
38 35 37 mulcld ${⊢}{\phi }\to \left|{D}-{E}\right|\left|{G}-{E}\right|\in ℂ$
39 26 27 absne0d ${⊢}{\phi }\to \left|{D}-{E}\right|\ne 0$
40 28 30 absne0d ${⊢}{\phi }\to \left|{G}-{E}\right|\ne 0$
41 35 37 39 40 mulne0d ${⊢}{\phi }\to \left|{D}-{E}\right|\left|{G}-{E}\right|\ne 0$
42 4 3 abssubd ${⊢}{\phi }\to \left|{C}-{B}\right|=\left|{B}-{C}\right|$
43 7 6 abssubd ${⊢}{\phi }\to \left|{G}-{E}\right|=\left|{E}-{G}\right|$
44 13 42 43 3eqtr4d ${⊢}{\phi }\to \left|{C}-{B}\right|=\left|{G}-{E}\right|$
45 12 44 oveq12d ${⊢}{\phi }\to \left|{A}-{B}\right|\left|{C}-{B}\right|=\left|{D}-{E}\right|\left|{G}-{E}\right|$
46 45 oveq1d ${⊢}{\phi }\to \left|{A}-{B}\right|\left|{C}-{B}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)=\left|{D}-{E}\right|\left|{G}-{E}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)$
47 12 35 eqeltrd ${⊢}{\phi }\to \left|{A}-{B}\right|\in ℂ$
48 44 37 eqeltrd ${⊢}{\phi }\to \left|{C}-{B}\right|\in ℂ$
49 47 48 mulcld ${⊢}{\phi }\to \left|{A}-{B}\right|\left|{C}-{B}\right|\in ℂ$
50 49 25 mulcld ${⊢}{\phi }\to \left|{A}-{B}\right|\left|{C}-{B}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)\in ℂ$
51 38 33 mulcld ${⊢}{\phi }\to \left|{D}-{E}\right|\left|{G}-{E}\right|\mathrm{cos}\left(\left({D}-{E}\right){F}\left({G}-{E}\right)\right)\in ℂ$
52 2cnd ${⊢}{\phi }\to 2\in ℂ$
53 2ne0 ${⊢}2\ne 0$
54 53 a1i ${⊢}{\phi }\to 2\ne 0$
55 35 sqcld ${⊢}{\phi }\to {\left|{D}-{E}\right|}^{2}\in ℂ$
56 37 sqcld ${⊢}{\phi }\to {\left|{G}-{E}\right|}^{2}\in ℂ$
57 55 56 addcld ${⊢}{\phi }\to {\left|{D}-{E}\right|}^{2}+{\left|{G}-{E}\right|}^{2}\in ℂ$
58 52 50 mulcld ${⊢}{\phi }\to 2\left|{A}-{B}\right|\left|{C}-{B}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)\in ℂ$
59 52 51 mulcld ${⊢}{\phi }\to 2\left|{D}-{E}\right|\left|{G}-{E}\right|\mathrm{cos}\left(\left({D}-{E}\right){F}\left({G}-{E}\right)\right)\in ℂ$
60 12 oveq1d ${⊢}{\phi }\to {\left|{A}-{B}\right|}^{2}={\left|{D}-{E}\right|}^{2}$
61 44 oveq1d ${⊢}{\phi }\to {\left|{C}-{B}\right|}^{2}={\left|{G}-{E}\right|}^{2}$
62 60 61 oveq12d ${⊢}{\phi }\to {\left|{A}-{B}\right|}^{2}+{\left|{C}-{B}\right|}^{2}={\left|{D}-{E}\right|}^{2}+{\left|{G}-{E}\right|}^{2}$
63 62 oveq1d ${⊢}{\phi }\to {\left|{A}-{B}\right|}^{2}+{\left|{C}-{B}\right|}^{2}-2\left|{A}-{B}\right|\left|{C}-{B}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)={\left|{D}-{E}\right|}^{2}+{\left|{G}-{E}\right|}^{2}-2\left|{A}-{B}\right|\left|{C}-{B}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)$
64 14 oveq1d ${⊢}{\phi }\to {\left|{C}-{A}\right|}^{2}={\left|{G}-{D}\right|}^{2}$
65 eqid ${⊢}\left|{A}-{B}\right|=\left|{A}-{B}\right|$
66 eqid ${⊢}\left|{C}-{B}\right|=\left|{C}-{B}\right|$
67 eqid ${⊢}\left|{C}-{A}\right|=\left|{C}-{A}\right|$
68 eqid ${⊢}\left({A}-{B}\right){F}\left({C}-{B}\right)=\left({A}-{B}\right){F}\left({C}-{B}\right)$
69 1 65 66 67 68 lawcos ${⊢}\left(\left({C}\in ℂ\wedge {A}\in ℂ\wedge {B}\in ℂ\right)\wedge \left({C}\ne {B}\wedge {A}\ne {B}\right)\right)\to {\left|{C}-{A}\right|}^{2}={\left|{A}-{B}\right|}^{2}+{\left|{C}-{B}\right|}^{2}-2\left|{A}-{B}\right|\left|{C}-{B}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)$
70 4 2 3 21 8 69 syl32anc ${⊢}{\phi }\to {\left|{C}-{A}\right|}^{2}={\left|{A}-{B}\right|}^{2}+{\left|{C}-{B}\right|}^{2}-2\left|{A}-{B}\right|\left|{C}-{B}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)$
71 eqid ${⊢}\left|{D}-{E}\right|=\left|{D}-{E}\right|$
72 eqid ${⊢}\left|{G}-{E}\right|=\left|{G}-{E}\right|$
73 eqid ${⊢}\left|{G}-{D}\right|=\left|{G}-{D}\right|$
74 eqid ${⊢}\left({D}-{E}\right){F}\left({G}-{E}\right)=\left({D}-{E}\right){F}\left({G}-{E}\right)$
75 1 71 72 73 74 lawcos ${⊢}\left(\left({G}\in ℂ\wedge {D}\in ℂ\wedge {E}\in ℂ\right)\wedge \left({G}\ne {E}\wedge {D}\ne {E}\right)\right)\to {\left|{G}-{D}\right|}^{2}={\left|{D}-{E}\right|}^{2}+{\left|{G}-{E}\right|}^{2}-2\left|{D}-{E}\right|\left|{G}-{E}\right|\mathrm{cos}\left(\left({D}-{E}\right){F}\left({G}-{E}\right)\right)$
76 7 5 6 29 10 75 syl32anc ${⊢}{\phi }\to {\left|{G}-{D}\right|}^{2}={\left|{D}-{E}\right|}^{2}+{\left|{G}-{E}\right|}^{2}-2\left|{D}-{E}\right|\left|{G}-{E}\right|\mathrm{cos}\left(\left({D}-{E}\right){F}\left({G}-{E}\right)\right)$
77 64 70 76 3eqtr3d ${⊢}{\phi }\to {\left|{A}-{B}\right|}^{2}+{\left|{C}-{B}\right|}^{2}-2\left|{A}-{B}\right|\left|{C}-{B}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)={\left|{D}-{E}\right|}^{2}+{\left|{G}-{E}\right|}^{2}-2\left|{D}-{E}\right|\left|{G}-{E}\right|\mathrm{cos}\left(\left({D}-{E}\right){F}\left({G}-{E}\right)\right)$
78 63 77 eqtr3d ${⊢}{\phi }\to {\left|{D}-{E}\right|}^{2}+{\left|{G}-{E}\right|}^{2}-2\left|{A}-{B}\right|\left|{C}-{B}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)={\left|{D}-{E}\right|}^{2}+{\left|{G}-{E}\right|}^{2}-2\left|{D}-{E}\right|\left|{G}-{E}\right|\mathrm{cos}\left(\left({D}-{E}\right){F}\left({G}-{E}\right)\right)$
79 57 58 59 78 subcand ${⊢}{\phi }\to 2\left|{A}-{B}\right|\left|{C}-{B}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)=2\left|{D}-{E}\right|\left|{G}-{E}\right|\mathrm{cos}\left(\left({D}-{E}\right){F}\left({G}-{E}\right)\right)$
80 50 51 52 54 79 mulcanad ${⊢}{\phi }\to \left|{A}-{B}\right|\left|{C}-{B}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)=\left|{D}-{E}\right|\left|{G}-{E}\right|\mathrm{cos}\left(\left({D}-{E}\right){F}\left({G}-{E}\right)\right)$
81 46 80 eqtr3d ${⊢}{\phi }\to \left|{D}-{E}\right|\left|{G}-{E}\right|\mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)=\left|{D}-{E}\right|\left|{G}-{E}\right|\mathrm{cos}\left(\left({D}-{E}\right){F}\left({G}-{E}\right)\right)$
82 25 33 38 41 81 mulcanad ${⊢}{\phi }\to \mathrm{cos}\left(\left({A}-{B}\right){F}\left({C}-{B}\right)\right)=\mathrm{cos}\left(\left({D}-{E}\right){F}\left({G}-{E}\right)\right)$