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