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 syl6eq 
 |-  ( 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 syl6eq 
 |-  ( 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 ) ) ) )