Step | Hyp | Ref
| Expression |
1 | | halfaddsubcl 12390 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β (((π΄ + π΅) / 2) β β β§ ((π΄ β π΅) / 2) β β)) |
2 | | sincl 16013 |
. . . . 5
β’ (((π΄ + π΅) / 2) β β β
(sinβ((π΄ + π΅) / 2)) β
β) |
3 | | sincl 16013 |
. . . . 5
β’ (((π΄ β π΅) / 2) β β β
(sinβ((π΄ β
π΅) / 2)) β
β) |
4 | | mulcl 11140 |
. . . . 5
β’
(((sinβ((π΄ +
π΅) / 2)) β β
β§ (sinβ((π΄
β π΅) / 2)) β
β) β ((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))) β β) |
5 | 2, 3, 4 | syl2an 597 |
. . . 4
β’ ((((π΄ + π΅) / 2) β β β§ ((π΄ β π΅) / 2) β β) β
((sinβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2))) β
β) |
6 | 1, 5 | syl 17 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
((sinβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2))) β
β) |
7 | 6 | 2timesd 12401 |
. 2
β’ ((π΄ β β β§ π΅ β β) β (2
Β· ((sinβ((π΄ +
π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2)))) =
(((sinβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2))) +
((sinβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) /
2))))) |
8 | | cossub 16056 |
. . . . 5
β’ ((((π΄ + π΅) / 2) β β β§ ((π΄ β π΅) / 2) β β) β
(cosβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2))) = (((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) + ((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) |
9 | | cosadd 16052 |
. . . . 5
β’ ((((π΄ + π΅) / 2) β β β§ ((π΄ β π΅) / 2) β β) β
(cosβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2))) = (((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) β ((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) |
10 | 8, 9 | oveq12d 7376 |
. . . 4
β’ ((((π΄ + π΅) / 2) β β β§ ((π΄ β π΅) / 2) β β) β
((cosβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2))) β (cosβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2)))) = ((((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) + ((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2)))) β (((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) β ((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2)))))) |
11 | 1, 10 | syl 17 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
((cosβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2))) β (cosβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2)))) = ((((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) + ((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2)))) β (((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) β ((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2)))))) |
12 | | coscl 16014 |
. . . . . 6
β’ (((π΄ + π΅) / 2) β β β
(cosβ((π΄ + π΅) / 2)) β
β) |
13 | | coscl 16014 |
. . . . . 6
β’ (((π΄ β π΅) / 2) β β β
(cosβ((π΄ β
π΅) / 2)) β
β) |
14 | | mulcl 11140 |
. . . . . 6
β’
(((cosβ((π΄ +
π΅) / 2)) β β
β§ (cosβ((π΄
β π΅) / 2)) β
β) β ((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) β β) |
15 | 12, 13, 14 | syl2an 597 |
. . . . 5
β’ ((((π΄ + π΅) / 2) β β β§ ((π΄ β π΅) / 2) β β) β
((cosβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) β
β) |
16 | 1, 15 | syl 17 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β
((cosβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) β
β) |
17 | 16, 6, 6 | pnncand 11556 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
((((cosβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) +
((sinβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2)))) β
(((cosβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) β
((sinβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2))))) =
(((sinβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2))) +
((sinβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) /
2))))) |
18 | 11, 17 | eqtrd 2773 |
. 2
β’ ((π΄ β β β§ π΅ β β) β
((cosβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2))) β (cosβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2)))) = (((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))) + ((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) |
19 | | halfaddsub 12391 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β
((((π΄ + π΅) / 2) + ((π΄ β π΅) / 2)) = π΄ β§ (((π΄ + π΅) / 2) β ((π΄ β π΅) / 2)) = π΅)) |
20 | 19 | simprd 497 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β (((π΄ + π΅) / 2) β ((π΄ β π΅) / 2)) = π΅) |
21 | 20 | fveq2d 6847 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
(cosβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2))) = (cosβπ΅)) |
22 | 19 | simpld 496 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β (((π΄ + π΅) / 2) + ((π΄ β π΅) / 2)) = π΄) |
23 | 22 | fveq2d 6847 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
(cosβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2))) = (cosβπ΄)) |
24 | 21, 23 | oveq12d 7376 |
. 2
β’ ((π΄ β β β§ π΅ β β) β
((cosβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2))) β (cosβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2)))) = ((cosβπ΅) β (cosβπ΄))) |
25 | 7, 18, 24 | 3eqtr2rd 2780 |
1
β’ ((π΄ β β β§ π΅ β β) β
((cosβπ΅) β
(cosβπ΄)) = (2
Β· ((sinβ((π΄ +
π΅) / 2)) Β·
(sinβ((π΄ β
π΅) /
2))))) |