Metamath Proof Explorer


Theorem sinmpi

Description: Sine of a number less _pi . (Contributed by Paul Chapman, 15-Mar-2008)

Ref Expression
Assertion sinmpi A sin A π = sin A

Proof

Step Hyp Ref Expression
1 picn π
2 sinsub A π sin A π = sin A cos π cos A sin π
3 1 2 mpan2 A sin A π = sin A cos π cos A sin π
4 cospi cos π = 1
5 4 oveq2i sin A cos π = sin A -1
6 sincl A sin A
7 neg1cn 1
8 mulcom sin A 1 sin A -1 = -1 sin A
9 7 8 mpan2 sin A sin A -1 = -1 sin A
10 mulm1 sin A -1 sin A = sin A
11 9 10 eqtrd sin A sin A -1 = sin A
12 6 11 syl A sin A -1 = sin A
13 5 12 syl5eq A sin A cos π = sin A
14 sinpi sin π = 0
15 14 oveq2i cos A sin π = cos A 0
16 coscl A cos A
17 16 mul01d A cos A 0 = 0
18 15 17 syl5eq A cos A sin π = 0
19 13 18 oveq12d A sin A cos π cos A sin π = - sin A - 0
20 6 negcld A sin A
21 20 subid1d A - sin A - 0 = sin A
22 19 21 eqtrd A sin A cos π cos A sin π = sin A
23 3 22 eqtrd A sin A π = sin A