Step |
Hyp |
Ref |
Expression |
1 |
|
negcl |
|- ( B e. CC -> -u B e. CC ) |
2 |
|
sinadd |
|- ( ( A e. CC /\ -u B e. CC ) -> ( sin ` ( A + -u B ) ) = ( ( ( sin ` A ) x. ( cos ` -u B ) ) + ( ( cos ` A ) x. ( sin ` -u B ) ) ) ) |
3 |
1 2
|
sylan2 |
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` ( A + -u B ) ) = ( ( ( sin ` A ) x. ( cos ` -u B ) ) + ( ( cos ` A ) x. ( sin ` -u B ) ) ) ) |
4 |
|
negsub |
|- ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) ) |
5 |
4
|
fveq2d |
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` ( A + -u B ) ) = ( sin ` ( A - B ) ) ) |
6 |
|
cosneg |
|- ( B e. CC -> ( cos ` -u B ) = ( cos ` B ) ) |
7 |
6
|
adantl |
|- ( ( A e. CC /\ B e. CC ) -> ( cos ` -u B ) = ( cos ` B ) ) |
8 |
7
|
oveq2d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( cos ` -u B ) ) = ( ( sin ` A ) x. ( cos ` B ) ) ) |
9 |
|
sinneg |
|- ( B e. CC -> ( sin ` -u B ) = -u ( sin ` B ) ) |
10 |
9
|
adantl |
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` -u B ) = -u ( sin ` B ) ) |
11 |
10
|
oveq2d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( sin ` -u B ) ) = ( ( cos ` A ) x. -u ( sin ` B ) ) ) |
12 |
|
coscl |
|- ( A e. CC -> ( cos ` A ) e. CC ) |
13 |
|
sincl |
|- ( B e. CC -> ( sin ` B ) e. CC ) |
14 |
|
mulneg2 |
|- ( ( ( cos ` A ) e. CC /\ ( sin ` B ) e. CC ) -> ( ( cos ` A ) x. -u ( sin ` B ) ) = -u ( ( cos ` A ) x. ( sin ` B ) ) ) |
15 |
12 13 14
|
syl2an |
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. -u ( sin ` B ) ) = -u ( ( cos ` A ) x. ( sin ` B ) ) ) |
16 |
11 15
|
eqtrd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( sin ` -u B ) ) = -u ( ( cos ` A ) x. ( sin ` B ) ) ) |
17 |
8 16
|
oveq12d |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( sin ` A ) x. ( cos ` -u B ) ) + ( ( cos ` A ) x. ( sin ` -u B ) ) ) = ( ( ( sin ` A ) x. ( cos ` B ) ) + -u ( ( cos ` A ) x. ( sin ` B ) ) ) ) |
18 |
|
sincl |
|- ( A e. CC -> ( sin ` A ) e. CC ) |
19 |
|
coscl |
|- ( B e. CC -> ( cos ` B ) e. CC ) |
20 |
|
mulcl |
|- ( ( ( sin ` A ) e. CC /\ ( cos ` B ) e. CC ) -> ( ( sin ` A ) x. ( cos ` B ) ) e. CC ) |
21 |
18 19 20
|
syl2an |
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( cos ` B ) ) e. CC ) |
22 |
|
mulcl |
|- ( ( ( cos ` A ) e. CC /\ ( sin ` B ) e. CC ) -> ( ( cos ` A ) x. ( sin ` B ) ) e. CC ) |
23 |
12 13 22
|
syl2an |
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( sin ` B ) ) e. CC ) |
24 |
21 23
|
negsubd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( sin ` A ) x. ( cos ` B ) ) + -u ( ( cos ` A ) x. ( sin ` B ) ) ) = ( ( ( sin ` A ) x. ( cos ` B ) ) - ( ( cos ` A ) x. ( sin ` B ) ) ) ) |
25 |
17 24
|
eqtrd |
|- ( ( A e. CC /\ B e. CC ) -> ( ( ( sin ` A ) x. ( cos ` -u B ) ) + ( ( cos ` A ) x. ( sin ` -u B ) ) ) = ( ( ( sin ` A ) x. ( cos ` B ) ) - ( ( cos ` A ) x. ( sin ` B ) ) ) ) |
26 |
3 5 25
|
3eqtr3d |
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` ( A - B ) ) = ( ( ( sin ` A ) x. ( cos ` B ) ) - ( ( cos ` A ) x. ( sin ` B ) ) ) ) |