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