Metamath Proof Explorer

Theorem cos2t

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

Ref Expression
Assertion cos2t 
|- ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( ( 2 x. ( ( cos ` A ) ^ 2 ) ) - 1 ) )

Proof

Step Hyp Ref Expression
1 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
2 1 sqcld 
 |-  ( A e. CC -> ( ( cos ` A ) ^ 2 ) e. CC )
3 ax-1cn 
 |-  1 e. CC
4 subsub3 
 |-  ( ( ( ( cos ` A ) ^ 2 ) e. CC /\ 1 e. CC /\ ( ( cos ` A ) ^ 2 ) e. CC ) -> ( ( ( cos ` A ) ^ 2 ) - ( 1 - ( ( cos ` A ) ^ 2 ) ) ) = ( ( ( ( cos ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) - 1 ) )
5 3 4 mp3an2 
 |-  ( ( ( ( cos ` A ) ^ 2 ) e. CC /\ ( ( cos ` A ) ^ 2 ) e. CC ) -> ( ( ( cos ` A ) ^ 2 ) - ( 1 - ( ( cos ` A ) ^ 2 ) ) ) = ( ( ( ( cos ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) - 1 ) )
6 2 2 5 syl2anc 
 |-  ( A e. CC -> ( ( ( cos ` A ) ^ 2 ) - ( 1 - ( ( cos ` A ) ^ 2 ) ) ) = ( ( ( ( cos ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) - 1 ) )
7 cosadd 
 |-  ( ( A e. CC /\ A e. CC ) -> ( cos ` ( A + A ) ) = ( ( ( cos ` A ) x. ( cos ` A ) ) - ( ( sin ` A ) x. ( sin ` A ) ) ) )
8 7 anidms 
 |-  ( A e. CC -> ( cos ` ( A + A ) ) = ( ( ( cos ` A ) x. ( cos ` A ) ) - ( ( sin ` A ) x. ( sin ` A ) ) ) )
9 2times 
 |-  ( A e. CC -> ( 2 x. A ) = ( A + A ) )
10 9 fveq2d 
 |-  ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( cos ` ( A + A ) ) )
11 1 sqvald 
 |-  ( A e. CC -> ( ( cos ` A ) ^ 2 ) = ( ( cos ` A ) x. ( cos ` A ) ) )
12 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
13 12 sqvald 
 |-  ( A e. CC -> ( ( sin ` A ) ^ 2 ) = ( ( sin ` A ) x. ( sin ` A ) ) )
14 11 13 oveq12d 
 |-  ( A e. CC -> ( ( ( cos ` A ) ^ 2 ) - ( ( sin ` A ) ^ 2 ) ) = ( ( ( cos ` A ) x. ( cos ` A ) ) - ( ( sin ` A ) x. ( sin ` A ) ) ) )
15 8 10 14 3eqtr4d 
 |-  ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( ( ( cos ` A ) ^ 2 ) - ( ( sin ` A ) ^ 2 ) ) )
16 12 sqcld 
 |-  ( A e. CC -> ( ( sin ` A ) ^ 2 ) e. CC )
17 16 2 addcomd 
 |-  ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) )
18 sincossq 
 |-  ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
19 17 18 eqtr3d 
 |-  ( A e. CC -> ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) = 1 )
20 subadd 
 |-  ( ( 1 e. CC /\ ( ( cos ` A ) ^ 2 ) e. CC /\ ( ( sin ` A ) ^ 2 ) e. CC ) -> ( ( 1 - ( ( cos ` A ) ^ 2 ) ) = ( ( sin ` A ) ^ 2 ) <-> ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) = 1 ) )
21 3 2 16 20 mp3an2i 
 |-  ( A e. CC -> ( ( 1 - ( ( cos ` A ) ^ 2 ) ) = ( ( sin ` A ) ^ 2 ) <-> ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) = 1 ) )
22 19 21 mpbird 
 |-  ( A e. CC -> ( 1 - ( ( cos ` A ) ^ 2 ) ) = ( ( sin ` A ) ^ 2 ) )
23 22 oveq2d 
 |-  ( A e. CC -> ( ( ( cos ` A ) ^ 2 ) - ( 1 - ( ( cos ` A ) ^ 2 ) ) ) = ( ( ( cos ` A ) ^ 2 ) - ( ( sin ` A ) ^ 2 ) ) )
24 15 23 eqtr4d 
 |-  ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( ( ( cos ` A ) ^ 2 ) - ( 1 - ( ( cos ` A ) ^ 2 ) ) ) )
25 2 2timesd 
 |-  ( A e. CC -> ( 2 x. ( ( cos ` A ) ^ 2 ) ) = ( ( ( cos ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) )
26 25 oveq1d 
 |-  ( A e. CC -> ( ( 2 x. ( ( cos ` A ) ^ 2 ) ) - 1 ) = ( ( ( ( cos ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) - 1 ) )
27 6 24 26 3eqtr4d 
 |-  ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( ( 2 x. ( ( cos ` A ) ^ 2 ) ) - 1 ) )