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 ‘ 𝐵 ) ) ) )