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 Acos2A=12sinA2

Proof

Step Hyp Ref Expression
1 cos2t Acos2A=2cosA21
2 2cn 2
3 sincl AsinA
4 3 sqcld AsinA2
5 coscl AcosA
6 5 sqcld AcosA2
7 adddi 2sinA2cosA22sinA2+cosA2=2sinA2+2cosA2
8 2 4 6 7 mp3an2i A2sinA2+cosA2=2sinA2+2cosA2
9 sincossq AsinA2+cosA2=1
10 9 oveq2d A2sinA2+cosA2=21
11 8 10 eqtr3d A2sinA2+2cosA2=21
12 2t1e2 21=2
13 11 12 eqtrdi A2sinA2+2cosA2=2
14 mulcl 2sinA22sinA2
15 2 4 14 sylancr A2sinA2
16 mulcl 2cosA22cosA2
17 2 6 16 sylancr A2cosA2
18 subadd 22sinA22cosA222sinA2=2cosA22sinA2+2cosA2=2
19 2 15 17 18 mp3an2i A22sinA2=2cosA22sinA2+2cosA2=2
20 13 19 mpbird A22sinA2=2cosA2
21 20 oveq1d A2-2sinA2-1=2cosA21
22 ax-1cn 1
23 sub32 22sinA212-2sinA2-1=2-1-2sinA2
24 2 22 23 mp3an13 2sinA22-2sinA2-1=2-1-2sinA2
25 15 24 syl A2-2sinA2-1=2-1-2sinA2
26 2m1e1 21=1
27 26 oveq1i 2-1-2sinA2=12sinA2
28 25 27 eqtrdi A2-2sinA2-1=12sinA2
29 1 21 28 3eqtr2d Acos2A=12sinA2