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 cos 2 A = 1 2 sin A 2

Proof

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