Step | Hyp | Ref
| Expression |
1 | | addcl 11138 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β) β (π΄ + π΅) β β) |
2 | 1 | halfcld 12403 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β ((π΄ + π΅) / 2) β β) |
3 | 2 | sincld 16017 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β
(sinβ((π΄ + π΅) / 2)) β
β) |
4 | | subcl 11405 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β) β (π΄ β π΅) β β) |
5 | 4 | halfcld 12403 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β ((π΄ β π΅) / 2) β β) |
6 | 5 | coscld 16018 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β
(cosβ((π΄ β
π΅) / 2)) β
β) |
7 | 3, 6 | mulcld 11180 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
((sinβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) β
β) |
8 | 7 | 2timesd 12401 |
. 2
β’ ((π΄ β β β§ π΅ β β) β (2
Β· ((sinβ((π΄ +
π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2)))) =
(((sinβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) +
((sinβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) /
2))))) |
9 | | sinadd 16051 |
. . . . 5
β’ ((((π΄ + π΅) / 2) β β β§ ((π΄ β π΅) / 2) β β) β
(sinβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2))) = (((sinβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) + ((cosβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) |
10 | 2, 5, 9 | syl2anc 585 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β
(sinβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2))) = (((sinβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) + ((cosβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) |
11 | | sinsub 16055 |
. . . . 5
β’ ((((π΄ + π΅) / 2) β β β§ ((π΄ β π΅) / 2) β β) β
(sinβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2))) = (((sinβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) β ((cosβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) |
12 | 2, 5, 11 | syl2anc 585 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β
(sinβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2))) = (((sinβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) β ((cosβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) |
13 | 10, 12 | oveq12d 7376 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
((sinβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2))) + (sinβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2)))) = ((((sinβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) + ((cosβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2)))) + (((sinβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) β ((cosβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2)))))) |
14 | 2 | coscld 16018 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β
(cosβ((π΄ + π΅) / 2)) β
β) |
15 | 5 | sincld 16017 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β
(sinβ((π΄ β
π΅) / 2)) β
β) |
16 | 14, 15 | mulcld 11180 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β
((cosβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2))) β
β) |
17 | 7, 16, 7 | ppncand 11557 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
((((sinβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) +
((cosβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2)))) +
(((sinβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) β
((cosβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2))))) =
(((sinβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) +
((sinβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) /
2))))) |
18 | 13, 17 | eqtrd 2773 |
. 2
β’ ((π΄ β β β§ π΅ β β) β
((sinβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2))) + (sinβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2)))) = (((sinβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) + ((sinβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 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 | 8, 18, 24 | 3eqtr2rd 2780 |
1
β’ ((π΄ β β β§ π΅ β β) β
((sinβπ΄) +
(sinβπ΅)) = (2
Β· ((sinβ((π΄ +
π΅) / 2)) Β·
(cosβ((π΄ β
π΅) /
2))))) |