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 โŠข ๐น = ( ๐‘ฅ โˆˆ ( โ„‚ โˆ– { 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 โ€˜ ( ( ๐ท โˆ’ ๐ธ ) ๐น ( ๐บ โˆ’ ๐ธ ) ) ) )

Proof

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 โ€˜ ( ( ๐ท โˆ’ ๐ธ ) ๐น ( ๐บ โˆ’ ๐ธ ) ) ) )