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 | โข ๐น = ( ๐ฅ โ ( โ โ { 0 } ) , ๐ฆ โ ( โ โ { 0 } ) โฆ ( โ โ ( log โ ( ๐ฆ / ๐ฅ ) ) ) ) | |
ssscongptld.1 | โข ( ๐ โ ๐ด โ โ ) | ||
ssscongptld.2 | โข ( ๐ โ ๐ต โ โ ) | ||
ssscongptld.3 | โข ( ๐ โ ๐ถ โ โ ) | ||
ssscongptld.4 | โข ( ๐ โ ๐ท โ โ ) | ||
ssscongptld.5 | โข ( ๐ โ ๐ธ โ โ ) | ||
ssscongptld.6 | โข ( ๐ โ ๐บ โ โ ) | ||
ssscongptld.7 | โข ( ๐ โ ๐ด โ ๐ต ) | ||
ssscongptld.8 | โข ( ๐ โ ๐ต โ ๐ถ ) | ||
ssscongptld.9 | โข ( ๐ โ ๐ท โ ๐ธ ) | ||
ssscongptld.10 | โข ( ๐ โ ๐ธ โ ๐บ ) | ||
ssscongptld.11 | โข ( ๐ โ ( abs โ ( ๐ด โ ๐ต ) ) = ( abs โ ( ๐ท โ ๐ธ ) ) ) | ||
ssscongptld.12 | โข ( ๐ โ ( abs โ ( ๐ต โ ๐ถ ) ) = ( abs โ ( ๐ธ โ ๐บ ) ) ) | ||
ssscongptld.13 | โข ( ๐ โ ( abs โ ( ๐ถ โ ๐ด ) ) = ( abs โ ( ๐บ โ ๐ท ) ) ) | ||
Assertion | ssscongptld | โข ( ๐ โ ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) = ( cos โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssscongptld.angdef | โข ๐น = ( ๐ฅ โ ( โ โ { 0 } ) , ๐ฆ โ ( โ โ { 0 } ) โฆ ( โ โ ( log โ ( ๐ฆ / ๐ฅ ) ) ) ) | |
2 | ssscongptld.1 | โข ( ๐ โ ๐ด โ โ ) | |
3 | ssscongptld.2 | โข ( ๐ โ ๐ต โ โ ) | |
4 | ssscongptld.3 | โข ( ๐ โ ๐ถ โ โ ) | |
5 | ssscongptld.4 | โข ( ๐ โ ๐ท โ โ ) | |
6 | ssscongptld.5 | โข ( ๐ โ ๐ธ โ โ ) | |
7 | ssscongptld.6 | โข ( ๐ โ ๐บ โ โ ) | |
8 | ssscongptld.7 | โข ( ๐ โ ๐ด โ ๐ต ) | |
9 | ssscongptld.8 | โข ( ๐ โ ๐ต โ ๐ถ ) | |
10 | ssscongptld.9 | โข ( ๐ โ ๐ท โ ๐ธ ) | |
11 | ssscongptld.10 | โข ( ๐ โ ๐ธ โ ๐บ ) | |
12 | ssscongptld.11 | โข ( ๐ โ ( abs โ ( ๐ด โ ๐ต ) ) = ( abs โ ( ๐ท โ ๐ธ ) ) ) | |
13 | ssscongptld.12 | โข ( ๐ โ ( abs โ ( ๐ต โ ๐ถ ) ) = ( abs โ ( ๐ธ โ ๐บ ) ) ) | |
14 | ssscongptld.13 | โข ( ๐ โ ( abs โ ( ๐ถ โ ๐ด ) ) = ( abs โ ( ๐บ โ ๐ท ) ) ) | |
15 | negpitopissre | โข ( - ฯ (,] ฯ ) โ โ | |
16 | ax-resscn | โข โ โ โ | |
17 | 15 16 | sstri | โข ( - ฯ (,] ฯ ) โ โ |
18 | 2 3 | subcld | โข ( ๐ โ ( ๐ด โ ๐ต ) โ โ ) |
19 | 2 3 8 | subne0d | โข ( ๐ โ ( ๐ด โ ๐ต ) โ 0 ) |
20 | 4 3 | subcld | โข ( ๐ โ ( ๐ถ โ ๐ต ) โ โ ) |
21 | 9 | necomd | โข ( ๐ โ ๐ถ โ ๐ต ) |
22 | 4 3 21 | subne0d | โข ( ๐ โ ( ๐ถ โ ๐ต ) โ 0 ) |
23 | 1 18 19 20 22 | angcld | โข ( ๐ โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) โ ( - ฯ (,] ฯ ) ) |
24 | 17 23 | sselid | โข ( ๐ โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) โ โ ) |
25 | 24 | coscld | โข ( ๐ โ ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) โ โ ) |
26 | 5 6 | subcld | โข ( ๐ โ ( ๐ท โ ๐ธ ) โ โ ) |
27 | 5 6 10 | subne0d | โข ( ๐ โ ( ๐ท โ ๐ธ ) โ 0 ) |
28 | 7 6 | subcld | โข ( ๐ โ ( ๐บ โ ๐ธ ) โ โ ) |
29 | 11 | necomd | โข ( ๐ โ ๐บ โ ๐ธ ) |
30 | 7 6 29 | subne0d | โข ( ๐ โ ( ๐บ โ ๐ธ ) โ 0 ) |
31 | 1 26 27 28 30 | angcld | โข ( ๐ โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) โ ( - ฯ (,] ฯ ) ) |
32 | 17 31 | sselid | โข ( ๐ โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) โ โ ) |
33 | 32 | coscld | โข ( ๐ โ ( cos โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) ) โ โ ) |
34 | 26 | abscld | โข ( ๐ โ ( abs โ ( ๐ท โ ๐ธ ) ) โ โ ) |
35 | 34 | recnd | โข ( ๐ โ ( abs โ ( ๐ท โ ๐ธ ) ) โ โ ) |
36 | 28 | abscld | โข ( ๐ โ ( abs โ ( ๐บ โ ๐ธ ) ) โ โ ) |
37 | 36 | recnd | โข ( ๐ โ ( abs โ ( ๐บ โ ๐ธ ) ) โ โ ) |
38 | 35 37 | mulcld | โข ( ๐ โ ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) โ โ ) |
39 | 26 27 | absne0d | โข ( ๐ โ ( abs โ ( ๐ท โ ๐ธ ) ) โ 0 ) |
40 | 28 30 | absne0d | โข ( ๐ โ ( abs โ ( ๐บ โ ๐ธ ) ) โ 0 ) |
41 | 35 37 39 40 | mulne0d | โข ( ๐ โ ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) โ 0 ) |
42 | 4 3 | abssubd | โข ( ๐ โ ( abs โ ( ๐ถ โ ๐ต ) ) = ( abs โ ( ๐ต โ ๐ถ ) ) ) |
43 | 7 6 | abssubd | โข ( ๐ โ ( abs โ ( ๐บ โ ๐ธ ) ) = ( abs โ ( ๐ธ โ ๐บ ) ) ) |
44 | 13 42 43 | 3eqtr4d | โข ( ๐ โ ( abs โ ( ๐ถ โ ๐ต ) ) = ( abs โ ( ๐บ โ ๐ธ ) ) ) |
45 | 12 44 | oveq12d | โข ( ๐ โ ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) = ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) ) |
46 | 45 | oveq1d | โข ( ๐ โ ( ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) = ( ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) ) |
47 | 12 35 | eqeltrd | โข ( ๐ โ ( abs โ ( ๐ด โ ๐ต ) ) โ โ ) |
48 | 44 37 | eqeltrd | โข ( ๐ โ ( abs โ ( ๐ถ โ ๐ต ) ) โ โ ) |
49 | 47 48 | mulcld | โข ( ๐ โ ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) โ โ ) |
50 | 49 25 | mulcld | โข ( ๐ โ ( ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) โ โ ) |
51 | 38 33 | mulcld | โข ( ๐ โ ( ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) ยท ( cos โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) ) ) โ โ ) |
52 | 2cnd | โข ( ๐ โ 2 โ โ ) | |
53 | 2ne0 | โข 2 โ 0 | |
54 | 53 | a1i | โข ( ๐ โ 2 โ 0 ) |
55 | 35 | sqcld | โข ( ๐ โ ( ( abs โ ( ๐ท โ ๐ธ ) ) โ 2 ) โ โ ) |
56 | 37 | sqcld | โข ( ๐ โ ( ( abs โ ( ๐บ โ ๐ธ ) ) โ 2 ) โ โ ) |
57 | 55 56 | addcld | โข ( ๐ โ ( ( ( abs โ ( ๐ท โ ๐ธ ) ) โ 2 ) + ( ( abs โ ( ๐บ โ ๐ธ ) ) โ 2 ) ) โ โ ) |
58 | 52 50 | mulcld | โข ( ๐ โ ( 2 ยท ( ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) ) โ โ ) |
59 | 52 51 | mulcld | โข ( ๐ โ ( 2 ยท ( ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) ยท ( cos โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) ) ) ) โ โ ) |
60 | 12 | oveq1d | โข ( ๐ โ ( ( abs โ ( ๐ด โ ๐ต ) ) โ 2 ) = ( ( abs โ ( ๐ท โ ๐ธ ) ) โ 2 ) ) |
61 | 44 | oveq1d | โข ( ๐ โ ( ( abs โ ( ๐ถ โ ๐ต ) ) โ 2 ) = ( ( abs โ ( ๐บ โ ๐ธ ) ) โ 2 ) ) |
62 | 60 61 | oveq12d | โข ( ๐ โ ( ( ( abs โ ( ๐ด โ ๐ต ) ) โ 2 ) + ( ( abs โ ( ๐ถ โ ๐ต ) ) โ 2 ) ) = ( ( ( abs โ ( ๐ท โ ๐ธ ) ) โ 2 ) + ( ( abs โ ( ๐บ โ ๐ธ ) ) โ 2 ) ) ) |
63 | 62 | oveq1d | โข ( ๐ โ ( ( ( ( abs โ ( ๐ด โ ๐ต ) ) โ 2 ) + ( ( abs โ ( ๐ถ โ ๐ต ) ) โ 2 ) ) โ ( 2 ยท ( ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) ) ) = ( ( ( ( abs โ ( ๐ท โ ๐ธ ) ) โ 2 ) + ( ( abs โ ( ๐บ โ ๐ธ ) ) โ 2 ) ) โ ( 2 ยท ( ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) ) ) ) |
64 | 14 | oveq1d | โข ( ๐ โ ( ( abs โ ( ๐ถ โ ๐ด ) ) โ 2 ) = ( ( abs โ ( ๐บ โ ๐ท ) ) โ 2 ) ) |
65 | eqid | โข ( abs โ ( ๐ด โ ๐ต ) ) = ( abs โ ( ๐ด โ ๐ต ) ) | |
66 | eqid | โข ( abs โ ( ๐ถ โ ๐ต ) ) = ( abs โ ( ๐ถ โ ๐ต ) ) | |
67 | eqid | โข ( abs โ ( ๐ถ โ ๐ด ) ) = ( abs โ ( ๐ถ โ ๐ด ) ) | |
68 | eqid | โข ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) = ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) | |
69 | 1 65 66 67 68 | lawcos | โข ( ( ( ๐ถ โ โ โง ๐ด โ โ โง ๐ต โ โ ) โง ( ๐ถ โ ๐ต โง ๐ด โ ๐ต ) ) โ ( ( abs โ ( ๐ถ โ ๐ด ) ) โ 2 ) = ( ( ( ( abs โ ( ๐ด โ ๐ต ) ) โ 2 ) + ( ( abs โ ( ๐ถ โ ๐ต ) ) โ 2 ) ) โ ( 2 ยท ( ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) ) ) ) |
70 | 4 2 3 21 8 69 | syl32anc | โข ( ๐ โ ( ( abs โ ( ๐ถ โ ๐ด ) ) โ 2 ) = ( ( ( ( abs โ ( ๐ด โ ๐ต ) ) โ 2 ) + ( ( abs โ ( ๐ถ โ ๐ต ) ) โ 2 ) ) โ ( 2 ยท ( ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) ) ) ) |
71 | eqid | โข ( abs โ ( ๐ท โ ๐ธ ) ) = ( abs โ ( ๐ท โ ๐ธ ) ) | |
72 | eqid | โข ( abs โ ( ๐บ โ ๐ธ ) ) = ( abs โ ( ๐บ โ ๐ธ ) ) | |
73 | eqid | โข ( abs โ ( ๐บ โ ๐ท ) ) = ( abs โ ( ๐บ โ ๐ท ) ) | |
74 | eqid | โข ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) = ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) | |
75 | 1 71 72 73 74 | lawcos | โข ( ( ( ๐บ โ โ โง ๐ท โ โ โง ๐ธ โ โ ) โง ( ๐บ โ ๐ธ โง ๐ท โ ๐ธ ) ) โ ( ( abs โ ( ๐บ โ ๐ท ) ) โ 2 ) = ( ( ( ( abs โ ( ๐ท โ ๐ธ ) ) โ 2 ) + ( ( abs โ ( ๐บ โ ๐ธ ) ) โ 2 ) ) โ ( 2 ยท ( ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) ยท ( cos โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) ) ) ) ) ) |
76 | 7 5 6 29 10 75 | syl32anc | โข ( ๐ โ ( ( abs โ ( ๐บ โ ๐ท ) ) โ 2 ) = ( ( ( ( abs โ ( ๐ท โ ๐ธ ) ) โ 2 ) + ( ( abs โ ( ๐บ โ ๐ธ ) ) โ 2 ) ) โ ( 2 ยท ( ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) ยท ( cos โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) ) ) ) ) ) |
77 | 64 70 76 | 3eqtr3d | โข ( ๐ โ ( ( ( ( abs โ ( ๐ด โ ๐ต ) ) โ 2 ) + ( ( abs โ ( ๐ถ โ ๐ต ) ) โ 2 ) ) โ ( 2 ยท ( ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) ) ) = ( ( ( ( abs โ ( ๐ท โ ๐ธ ) ) โ 2 ) + ( ( abs โ ( ๐บ โ ๐ธ ) ) โ 2 ) ) โ ( 2 ยท ( ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) ยท ( cos โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) ) ) ) ) ) |
78 | 63 77 | eqtr3d | โข ( ๐ โ ( ( ( ( abs โ ( ๐ท โ ๐ธ ) ) โ 2 ) + ( ( abs โ ( ๐บ โ ๐ธ ) ) โ 2 ) ) โ ( 2 ยท ( ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) ) ) = ( ( ( ( abs โ ( ๐ท โ ๐ธ ) ) โ 2 ) + ( ( abs โ ( ๐บ โ ๐ธ ) ) โ 2 ) ) โ ( 2 ยท ( ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) ยท ( cos โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) ) ) ) ) ) |
79 | 57 58 59 78 | subcand | โข ( ๐ โ ( 2 ยท ( ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) ) = ( 2 ยท ( ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) ยท ( cos โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) ) ) ) ) |
80 | 50 51 52 54 79 | mulcanad | โข ( ๐ โ ( ( ( abs โ ( ๐ด โ ๐ต ) ) ยท ( abs โ ( ๐ถ โ ๐ต ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) = ( ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) ยท ( cos โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) ) ) ) |
81 | 46 80 | eqtr3d | โข ( ๐ โ ( ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) ยท ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) ) = ( ( ( abs โ ( ๐ท โ ๐ธ ) ) ยท ( abs โ ( ๐บ โ ๐ธ ) ) ) ยท ( cos โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) ) ) ) |
82 | 25 33 38 41 81 | mulcanad | โข ( ๐ โ ( cos โ ( ( ๐ด โ ๐ต ) ๐น ( ๐ถ โ ๐ต ) ) ) = ( cos โ ( ( ๐ท โ ๐ธ ) ๐น ( ๐บ โ ๐ธ ) ) ) ) |