This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cossub

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

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

Proof

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