Metamath Proof Explorer

Theorem subcos

Description: Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007) (Revised by Mario Carneiro, 10-May-2014)

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

Proof

Step Hyp Ref Expression
1 halfaddsubcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) )
2 sincl ⊢ ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ → ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ )
3 sincl ⊢ ( ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ → ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ∈ ℂ )
4 mulcl ⊢ ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ ∧ ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ∈ ℂ ) → ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
5 2 3 4 syl2an ⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) → ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
6 1 5 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
7 6 2timesd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
8 cossub ⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) → ( cos ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) = ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
9 cosadd ⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) → ( cos ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) = ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
10 8 9 oveq12d ⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) → ( ( cos ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( cos ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) − ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) ) )
11 1 10 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( cos ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) − ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) ) )
12 coscl ⊢ ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ → ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ )
13 coscl ⊢ ( ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ → ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ∈ ℂ )
14 mulcl ⊢ ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ ∧ ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ∈ ℂ ) → ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
15 12 13 14 syl2an ⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) → ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
16 1 15 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
17 16 6 6 pnncand ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) − ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) ) = ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
18 11 17 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( cos ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
19 halfaddsub ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) = 𝐴 ∧ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) = 𝐵 ) )
20 19 simprd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) = 𝐵 )
21 20 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) = ( cos ‘ 𝐵 ) )
22 19 simpld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) = 𝐴 )
23 22 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) = ( cos ‘ 𝐴 ) )
24 21 23 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( cos ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( cos ‘ 𝐵 ) − ( cos ‘ 𝐴 ) ) )
25 7 18 24 3eqtr2rd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐵 ) − ( cos ‘ 𝐴 ) ) = ( 2 · ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )