Metamath Proof Explorer


Theorem sinkpi

Description: The sine of an integer multiple of _pi is 0. (Contributed by NM, 11-Aug-2008)

Ref Expression
Assertion sinkpi K sin K π = 0

Proof

Step Hyp Ref Expression
1 zcn K K
2 picn π
3 mulcl K π K π
4 1 2 3 sylancl K K π
5 4 addid2d K 0 + K π = K π
6 5 fveq2d K sin 0 + K π = sin K π
7 0cn 0
8 addcl 0 K π 0 + K π
9 7 4 8 sylancr K 0 + K π
10 9 sincld K sin 0 + K π
11 abssinper 0 K sin 0 + K π = sin 0
12 7 11 mpan K sin 0 + K π = sin 0
13 sin0 sin 0 = 0
14 13 fveq2i sin 0 = 0
15 abs0 0 = 0
16 14 15 eqtri sin 0 = 0
17 12 16 eqtrdi K sin 0 + K π = 0
18 10 17 abs00d K sin 0 + K π = 0
19 6 18 eqtr3d K sin K π = 0