Metamath Proof Explorer


Theorem sin2t

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

Ref Expression
Assertion sin2t A sin 2 A = 2 sin A cos A

Proof

Step Hyp Ref Expression
1 2times A 2 A = A + A
2 1 fveq2d A sin 2 A = sin A + A
3 coscl A cos A
4 sincl A sin A
5 3 4 mulcomd A cos A sin A = sin A cos A
6 5 oveq2d A sin A cos A + cos A sin A = sin A cos A + sin A cos A
7 sinadd A A sin A + A = sin A cos A + cos A sin A
8 7 anidms A sin A + A = sin A cos A + cos A sin A
9 4 3 mulcld A sin A cos A
10 9 2timesd A 2 sin A cos A = sin A cos A + sin A cos A
11 6 8 10 3eqtr4d A sin A + A = 2 sin A cos A
12 2 11 eqtrd A sin 2 A = 2 sin A cos A