Step | Hyp | Ref
| Expression |
1 | | coscl 16014 |
. . 3
β’ (π΄ β β β
(cosβπ΄) β
β) |
2 | | coscl 16014 |
. . 3
β’ (π΅ β β β
(cosβπ΅) β
β) |
3 | | addcom 11346 |
. . 3
β’
(((cosβπ΄)
β β β§ (cosβπ΅) β β) β ((cosβπ΄) + (cosβπ΅)) = ((cosβπ΅) + (cosβπ΄))) |
4 | 1, 2, 3 | syl2an 597 |
. 2
β’ ((π΄ β β β§ π΅ β β) β
((cosβπ΄) +
(cosβπ΅)) =
((cosβπ΅) +
(cosβπ΄))) |
5 | | halfaddsub 12391 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β
((((π΄ + π΅) / 2) + ((π΄ β π΅) / 2)) = π΄ β§ (((π΄ + π΅) / 2) β ((π΄ β π΅) / 2)) = π΅)) |
6 | 5 | simprd 497 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β (((π΄ + π΅) / 2) β ((π΄ β π΅) / 2)) = π΅) |
7 | 6 | fveq2d 6847 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
(cosβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2))) = (cosβπ΅)) |
8 | 5 | simpld 496 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β (((π΄ + π΅) / 2) + ((π΄ β π΅) / 2)) = π΄) |
9 | 8 | fveq2d 6847 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
(cosβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2))) = (cosβπ΄)) |
10 | 7, 9 | oveq12d 7376 |
. 2
β’ ((π΄ β β β§ π΅ β β) β
((cosβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2))) + (cosβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2)))) = ((cosβπ΅) + (cosβπ΄))) |
11 | | halfaddsubcl 12390 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β (((π΄ + π΅) / 2) β β β§ ((π΄ β π΅) / 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 | 11, 15 | syl 17 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β
((cosβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) β
β) |
17 | | sincl 16013 |
. . . . . 6
β’ (((π΄ + π΅) / 2) β β β
(sinβ((π΄ + π΅) / 2)) β
β) |
18 | | sincl 16013 |
. . . . . 6
β’ (((π΄ β π΅) / 2) β β β
(sinβ((π΄ β
π΅) / 2)) β
β) |
19 | | mulcl 11140 |
. . . . . 6
β’
(((sinβ((π΄ +
π΅) / 2)) β β
β§ (sinβ((π΄
β π΅) / 2)) β
β) β ((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))) β β) |
20 | 17, 18, 19 | syl2an 597 |
. . . . 5
β’ ((((π΄ + π΅) / 2) β β β§ ((π΄ β π΅) / 2) β β) β
((sinβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2))) β
β) |
21 | 11, 20 | syl 17 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β
((sinβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2))) β
β) |
22 | 16, 21, 16 | ppncand 11557 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
((((cosβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) +
((sinβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2)))) +
(((cosβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) β
((sinβ((π΄ + π΅) / 2)) Β·
(sinβ((π΄ β
π΅) / 2))))) =
(((cosβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) +
((cosβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) /
2))))) |
23 | | cossub 16056 |
. . . . 5
β’ ((((π΄ + π΅) / 2) β β β§ ((π΄ β π΅) / 2) β β) β
(cosβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2))) = (((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) + ((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) |
24 | | cosadd 16052 |
. . . . 5
β’ ((((π΄ + π΅) / 2) β β β§ ((π΄ β π΅) / 2) β β) β
(cosβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2))) = (((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))) β ((sinβ((π΄ + π΅) / 2)) Β· (sinβ((π΄ β π΅) / 2))))) |
25 | 23, 24 | 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)))))) |
26 | 11, 25 | 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)))))) |
27 | 16 | 2timesd 12401 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β (2
Β· ((cosβ((π΄ +
π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2)))) =
(((cosβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) / 2))) +
((cosβ((π΄ + π΅) / 2)) Β·
(cosβ((π΄ β
π΅) /
2))))) |
28 | 22, 26, 27 | 3eqtr4d 2783 |
. 2
β’ ((π΄ β β β§ π΅ β β) β
((cosβ(((π΄ + π΅) / 2) β ((π΄ β π΅) / 2))) + (cosβ(((π΄ + π΅) / 2) + ((π΄ β π΅) / 2)))) = (2 Β· ((cosβ((π΄ + π΅) / 2)) Β· (cosβ((π΄ β π΅) / 2))))) |
29 | 4, 10, 28 | 3eqtr2d 2779 |
1
β’ ((π΄ β β β§ π΅ β β) β
((cosβπ΄) +
(cosβπ΅)) = (2
Β· ((cosβ((π΄ +
π΅) / 2)) Β·
(cosβ((π΄ β
π΅) /
2))))) |