Metamath Proof Explorer


Theorem sinsub

Description: Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007)

Ref Expression
Assertion sinsub ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( 𝐴𝐵 ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 negcl ( 𝐵 ∈ ℂ → - 𝐵 ∈ ℂ )
2 sinadd ( ( 𝐴 ∈ ℂ ∧ - 𝐵 ∈ ℂ ) → ( sin ‘ ( 𝐴 + - 𝐵 ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ - 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ - 𝐵 ) ) ) )
3 1 2 sylan2 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( 𝐴 + - 𝐵 ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ - 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ - 𝐵 ) ) ) )
4 negsub ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴𝐵 ) )
5 4 fveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( 𝐴 + - 𝐵 ) ) = ( sin ‘ ( 𝐴𝐵 ) ) )
6 cosneg ( 𝐵 ∈ ℂ → ( cos ‘ - 𝐵 ) = ( cos ‘ 𝐵 ) )
7 6 adantl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ - 𝐵 ) = ( cos ‘ 𝐵 ) )
8 7 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐴 ) · ( cos ‘ - 𝐵 ) ) = ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) )
9 sinneg ( 𝐵 ∈ ℂ → ( sin ‘ - 𝐵 ) = - ( sin ‘ 𝐵 ) )
10 9 adantl ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ - 𝐵 ) = - ( sin ‘ 𝐵 ) )
11 10 oveq2d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( sin ‘ - 𝐵 ) ) = ( ( cos ‘ 𝐴 ) · - ( sin ‘ 𝐵 ) ) )
12 coscl ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
13 sincl ( 𝐵 ∈ ℂ → ( sin ‘ 𝐵 ) ∈ ℂ )
14 mulneg2 ( ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ ( sin ‘ 𝐵 ) ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · - ( sin ‘ 𝐵 ) ) = - ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
15 12 13 14 syl2an ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · - ( sin ‘ 𝐵 ) ) = - ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
16 11 15 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( sin ‘ - 𝐵 ) ) = - ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
17 8 16 oveq12d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( sin ‘ 𝐴 ) · ( cos ‘ - 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ - 𝐵 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + - ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
18 sincl ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
19 coscl ( 𝐵 ∈ ℂ → ( cos ‘ 𝐵 ) ∈ ℂ )
20 mulcl ( ( ( sin ‘ 𝐴 ) ∈ ℂ ∧ ( cos ‘ 𝐵 ) ∈ ℂ ) → ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ )
21 18 19 20 syl2an ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ )
22 mulcl ( ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ ( sin ‘ 𝐵 ) ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ )
23 12 13 22 syl2an ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ )
24 21 23 negsubd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + - ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
25 17 24 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( sin ‘ 𝐴 ) · ( cos ‘ - 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ - 𝐵 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
26 3 5 25 3eqtr3d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( 𝐴𝐵 ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )