Metamath Proof Explorer

Theorem sin2t

Description: Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008)

Ref Expression
Assertion sin2t 
|- ( A e. CC -> ( sin ` ( 2 x. A ) ) = ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 2times 
 |-  ( A e. CC -> ( 2 x. A ) = ( A + A ) )
2 1 fveq2d 
 |-  ( A e. CC -> ( sin ` ( 2 x. A ) ) = ( sin ` ( A + A ) ) )
3 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
4 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
5 3 4 mulcomd 
 |-  ( A e. CC -> ( ( cos ` A ) x. ( sin ` A ) ) = ( ( sin ` A ) x. ( cos ` A ) ) )
6 5 oveq2d 
 |-  ( A e. CC -> ( ( ( sin ` A ) x. ( cos ` A ) ) + ( ( cos ` A ) x. ( sin ` A ) ) ) = ( ( ( sin ` A ) x. ( cos ` A ) ) + ( ( sin ` A ) x. ( cos ` A ) ) ) )
7 sinadd 
 |-  ( ( A e. CC /\ A e. CC ) -> ( sin ` ( A + A ) ) = ( ( ( sin ` A ) x. ( cos ` A ) ) + ( ( cos ` A ) x. ( sin ` A ) ) ) )
8 7 anidms 
 |-  ( A e. CC -> ( sin ` ( A + A ) ) = ( ( ( sin ` A ) x. ( cos ` A ) ) + ( ( cos ` A ) x. ( sin ` A ) ) ) )
9 4 3 mulcld 
 |-  ( A e. CC -> ( ( sin ` A ) x. ( cos ` A ) ) e. CC )
10 9 2timesd 
 |-  ( A e. CC -> ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) = ( ( ( sin ` A ) x. ( cos ` A ) ) + ( ( sin ` A ) x. ( cos ` A ) ) ) )
11 6 8 10 3eqtr4d 
 |-  ( A e. CC -> ( sin ` ( A + A ) ) = ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) )
12 2 11 eqtrd 
 |-  ( A e. CC -> ( sin ` ( 2 x. A ) ) = ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) )