Step | Hyp | Ref
| Expression |
1 | | negcl 11406 |
. . 3
β’ (π΅ β β β -π΅ β
β) |
2 | | cosadd 16052 |
. . 3
β’ ((π΄ β β β§ -π΅ β β) β
(cosβ(π΄ + -π΅)) = (((cosβπ΄) Β· (cosβ-π΅)) β ((sinβπ΄) Β· (sinβ-π΅)))) |
3 | 1, 2 | sylan2 594 |
. 2
β’ ((π΄ β β β§ π΅ β β) β
(cosβ(π΄ + -π΅)) = (((cosβπ΄) Β· (cosβ-π΅)) β ((sinβπ΄) Β· (sinβ-π΅)))) |
4 | | negsub 11454 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β (π΄ + -π΅) = (π΄ β π΅)) |
5 | 4 | fveq2d 6847 |
. 2
β’ ((π΄ β β β§ π΅ β β) β
(cosβ(π΄ + -π΅)) = (cosβ(π΄ β π΅))) |
6 | | cosneg 16034 |
. . . . . 6
β’ (π΅ β β β
(cosβ-π΅) =
(cosβπ΅)) |
7 | 6 | adantl 483 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β
(cosβ-π΅) =
(cosβπ΅)) |
8 | 7 | oveq2d 7374 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β
((cosβπ΄) Β·
(cosβ-π΅)) =
((cosβπ΄) Β·
(cosβπ΅))) |
9 | | sinneg 16033 |
. . . . . . 7
β’ (π΅ β β β
(sinβ-π΅) =
-(sinβπ΅)) |
10 | 9 | adantl 483 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β) β
(sinβ-π΅) =
-(sinβπ΅)) |
11 | 10 | oveq2d 7374 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β
((sinβπ΄) Β·
(sinβ-π΅)) =
((sinβπ΄) Β·
-(sinβπ΅))) |
12 | | sincl 16013 |
. . . . . 6
β’ (π΄ β β β
(sinβπ΄) β
β) |
13 | | sincl 16013 |
. . . . . 6
β’ (π΅ β β β
(sinβπ΅) β
β) |
14 | | mulneg2 11597 |
. . . . . 6
β’
(((sinβπ΄)
β β β§ (sinβπ΅) β β) β ((sinβπ΄) Β· -(sinβπ΅)) = -((sinβπ΄) Β· (sinβπ΅))) |
15 | 12, 13, 14 | syl2an 597 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β
((sinβπ΄) Β·
-(sinβπ΅)) =
-((sinβπ΄) Β·
(sinβπ΅))) |
16 | 11, 15 | eqtrd 2773 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β
((sinβπ΄) Β·
(sinβ-π΅)) =
-((sinβπ΄) Β·
(sinβπ΅))) |
17 | 8, 16 | oveq12d 7376 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
(((cosβπ΄) Β·
(cosβ-π΅)) β
((sinβπ΄) Β·
(sinβ-π΅))) =
(((cosβπ΄) Β·
(cosβπ΅)) β
-((sinβπ΄) Β·
(sinβπ΅)))) |
18 | | coscl 16014 |
. . . . 5
β’ (π΄ β β β
(cosβπ΄) β
β) |
19 | | coscl 16014 |
. . . . 5
β’ (π΅ β β β
(cosβπ΅) β
β) |
20 | | mulcl 11140 |
. . . . 5
β’
(((cosβπ΄)
β β β§ (cosβπ΅) β β) β ((cosβπ΄) Β· (cosβπ΅)) β
β) |
21 | 18, 19, 20 | syl2an 597 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β
((cosβπ΄) Β·
(cosβπ΅)) β
β) |
22 | | mulcl 11140 |
. . . . 5
β’
(((sinβπ΄)
β β β§ (sinβπ΅) β β) β ((sinβπ΄) Β· (sinβπ΅)) β
β) |
23 | 12, 13, 22 | syl2an 597 |
. . . 4
β’ ((π΄ β β β§ π΅ β β) β
((sinβπ΄) Β·
(sinβπ΅)) β
β) |
24 | 21, 23 | subnegd 11524 |
. . 3
β’ ((π΄ β β β§ π΅ β β) β
(((cosβπ΄) Β·
(cosβπ΅)) β
-((sinβπ΄) Β·
(sinβπ΅))) =
(((cosβπ΄) Β·
(cosβπ΅)) +
((sinβπ΄) Β·
(sinβπ΅)))) |
25 | 17, 24 | eqtrd 2773 |
. 2
β’ ((π΄ β β β§ π΅ β β) β
(((cosβπ΄) Β·
(cosβ-π΅)) β
((sinβπ΄) Β·
(sinβ-π΅))) =
(((cosβπ΄) Β·
(cosβπ΅)) +
((sinβπ΄) Β·
(sinβπ΅)))) |
26 | 3, 5, 25 | 3eqtr3d 2781 |
1
β’ ((π΄ β β β§ π΅ β β) β
(cosβ(π΄ β π΅)) = (((cosβπ΄) Β· (cosβπ΅)) + ((sinβπ΄) Β· (sinβπ΅)))) |