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
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` B ) - ( cos ` A ) ) = ( 2 x. ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 halfaddsubcl
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) / 2 ) e. CC /\ ( ( A - B ) / 2 ) e. CC ) )
2 sincl
 |-  ( ( ( A + B ) / 2 ) e. CC -> ( sin ` ( ( A + B ) / 2 ) ) e. CC )
3 sincl
 |-  ( ( ( A - B ) / 2 ) e. CC -> ( sin ` ( ( A - B ) / 2 ) ) e. CC )
4 mulcl
 |-  ( ( ( sin ` ( ( A + B ) / 2 ) ) e. CC /\ ( sin ` ( ( A - B ) / 2 ) ) e. CC ) -> ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) e. CC )
5 2 3 4 syl2an
 |-  ( ( ( ( A + B ) / 2 ) e. CC /\ ( ( A - B ) / 2 ) e. CC ) -> ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) e. CC )
6 1 5 syl
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) e. CC )
7 6 2timesd
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) = ( ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) + ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )
8 cossub
 |-  ( ( ( ( A + B ) / 2 ) e. CC /\ ( ( A - B ) / 2 ) e. CC ) -> ( cos ` ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) ) = ( ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) + ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )
9 cosadd
 |-  ( ( ( ( A + B ) / 2 ) e. CC /\ ( ( A - B ) / 2 ) e. CC ) -> ( cos ` ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) ) = ( ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) - ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )
10 8 9 oveq12d
 |-  ( ( ( ( A + B ) / 2 ) e. CC /\ ( ( A - B ) / 2 ) e. CC ) -> ( ( cos ` ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) ) - ( cos ` ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) ) ) = ( ( ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) + ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) - ( ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) - ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) ) )
11 1 10 syl
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) ) - ( cos ` ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) ) ) = ( ( ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) + ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) - ( ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) - ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) ) )
12 coscl
 |-  ( ( ( A + B ) / 2 ) e. CC -> ( cos ` ( ( A + B ) / 2 ) ) e. CC )
13 coscl
 |-  ( ( ( A - B ) / 2 ) e. CC -> ( cos ` ( ( A - B ) / 2 ) ) e. CC )
14 mulcl
 |-  ( ( ( cos ` ( ( A + B ) / 2 ) ) e. CC /\ ( cos ` ( ( A - B ) / 2 ) ) e. CC ) -> ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) e. CC )
15 12 13 14 syl2an
 |-  ( ( ( ( A + B ) / 2 ) e. CC /\ ( ( A - B ) / 2 ) e. CC ) -> ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) e. CC )
16 1 15 syl
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) e. CC )
17 16 6 6 pnncand
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) + ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) - ( ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) - ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) ) = ( ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) + ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )
18 11 17 eqtrd
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) ) - ( cos ` ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) ) ) = ( ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) + ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )
19 halfaddsub
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) = A /\ ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) = B ) )
20 19 simprd
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) = B )
21 20 fveq2d
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) ) = ( cos ` B ) )
22 19 simpld
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) = A )
23 22 fveq2d
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) ) = ( cos ` A ) )
24 21 23 oveq12d
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` ( ( ( A + B ) / 2 ) - ( ( A - B ) / 2 ) ) ) - ( cos ` ( ( ( A + B ) / 2 ) + ( ( A - B ) / 2 ) ) ) ) = ( ( cos ` B ) - ( cos ` A ) ) )
25 7 18 24 3eqtr2rd
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` B ) - ( cos ` A ) ) = ( 2 x. ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )