Metamath Proof Explorer


Theorem cos2tsin

Description: Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008)

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

Proof

Step Hyp Ref Expression
1 cos2t
 |-  ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( ( 2 x. ( ( cos ` A ) ^ 2 ) ) - 1 ) )
2 2cn
 |-  2 e. CC
3 sincl
 |-  ( A e. CC -> ( sin ` A ) e. CC )
4 3 sqcld
 |-  ( A e. CC -> ( ( sin ` A ) ^ 2 ) e. CC )
5 coscl
 |-  ( A e. CC -> ( cos ` A ) e. CC )
6 5 sqcld
 |-  ( A e. CC -> ( ( cos ` A ) ^ 2 ) e. CC )
7 adddi
 |-  ( ( 2 e. CC /\ ( ( sin ` A ) ^ 2 ) e. CC /\ ( ( cos ` A ) ^ 2 ) e. CC ) -> ( 2 x. ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) ) = ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) + ( 2 x. ( ( cos ` A ) ^ 2 ) ) ) )
8 2 4 6 7 mp3an2i
 |-  ( A e. CC -> ( 2 x. ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) ) = ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) + ( 2 x. ( ( cos ` A ) ^ 2 ) ) ) )
9 sincossq
 |-  ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
10 9 oveq2d
 |-  ( A e. CC -> ( 2 x. ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) ) = ( 2 x. 1 ) )
11 8 10 eqtr3d
 |-  ( A e. CC -> ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) + ( 2 x. ( ( cos ` A ) ^ 2 ) ) ) = ( 2 x. 1 ) )
12 2t1e2
 |-  ( 2 x. 1 ) = 2
13 11 12 eqtrdi
 |-  ( A e. CC -> ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) + ( 2 x. ( ( cos ` A ) ^ 2 ) ) ) = 2 )
14 mulcl
 |-  ( ( 2 e. CC /\ ( ( sin ` A ) ^ 2 ) e. CC ) -> ( 2 x. ( ( sin ` A ) ^ 2 ) ) e. CC )
15 2 4 14 sylancr
 |-  ( A e. CC -> ( 2 x. ( ( sin ` A ) ^ 2 ) ) e. CC )
16 mulcl
 |-  ( ( 2 e. CC /\ ( ( cos ` A ) ^ 2 ) e. CC ) -> ( 2 x. ( ( cos ` A ) ^ 2 ) ) e. CC )
17 2 6 16 sylancr
 |-  ( A e. CC -> ( 2 x. ( ( cos ` A ) ^ 2 ) ) e. CC )
18 subadd
 |-  ( ( 2 e. CC /\ ( 2 x. ( ( sin ` A ) ^ 2 ) ) e. CC /\ ( 2 x. ( ( cos ` A ) ^ 2 ) ) e. CC ) -> ( ( 2 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) = ( 2 x. ( ( cos ` A ) ^ 2 ) ) <-> ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) + ( 2 x. ( ( cos ` A ) ^ 2 ) ) ) = 2 ) )
19 2 15 17 18 mp3an2i
 |-  ( A e. CC -> ( ( 2 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) = ( 2 x. ( ( cos ` A ) ^ 2 ) ) <-> ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) + ( 2 x. ( ( cos ` A ) ^ 2 ) ) ) = 2 ) )
20 13 19 mpbird
 |-  ( A e. CC -> ( 2 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) = ( 2 x. ( ( cos ` A ) ^ 2 ) ) )
21 20 oveq1d
 |-  ( A e. CC -> ( ( 2 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) - 1 ) = ( ( 2 x. ( ( cos ` A ) ^ 2 ) ) - 1 ) )
22 ax-1cn
 |-  1 e. CC
23 sub32
 |-  ( ( 2 e. CC /\ ( 2 x. ( ( sin ` A ) ^ 2 ) ) e. CC /\ 1 e. CC ) -> ( ( 2 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) - 1 ) = ( ( 2 - 1 ) - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) )
24 2 22 23 mp3an13
 |-  ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) e. CC -> ( ( 2 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) - 1 ) = ( ( 2 - 1 ) - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) )
25 15 24 syl
 |-  ( A e. CC -> ( ( 2 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) - 1 ) = ( ( 2 - 1 ) - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) )
26 2m1e1
 |-  ( 2 - 1 ) = 1
27 26 oveq1i
 |-  ( ( 2 - 1 ) - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) = ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) )
28 25 27 eqtrdi
 |-  ( A e. CC -> ( ( 2 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) - 1 ) = ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) )
29 1 21 28 3eqtr2d
 |-  ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) )