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 e. ZZ -> ( sin ` ( K x. _pi ) ) = 0 )

Proof

Step Hyp Ref Expression
1 zcn
 |-  ( K e. ZZ -> K e. CC )
2 picn
 |-  _pi e. CC
3 mulcl
 |-  ( ( K e. CC /\ _pi e. CC ) -> ( K x. _pi ) e. CC )
4 1 2 3 sylancl
 |-  ( K e. ZZ -> ( K x. _pi ) e. CC )
5 4 addid2d
 |-  ( K e. ZZ -> ( 0 + ( K x. _pi ) ) = ( K x. _pi ) )
6 5 fveq2d
 |-  ( K e. ZZ -> ( sin ` ( 0 + ( K x. _pi ) ) ) = ( sin ` ( K x. _pi ) ) )
7 0cn
 |-  0 e. CC
8 addcl
 |-  ( ( 0 e. CC /\ ( K x. _pi ) e. CC ) -> ( 0 + ( K x. _pi ) ) e. CC )
9 7 4 8 sylancr
 |-  ( K e. ZZ -> ( 0 + ( K x. _pi ) ) e. CC )
10 9 sincld
 |-  ( K e. ZZ -> ( sin ` ( 0 + ( K x. _pi ) ) ) e. CC )
11 abssinper
 |-  ( ( 0 e. CC /\ K e. ZZ ) -> ( abs ` ( sin ` ( 0 + ( K x. _pi ) ) ) ) = ( abs ` ( sin ` 0 ) ) )
12 7 11 mpan
 |-  ( K e. ZZ -> ( abs ` ( sin ` ( 0 + ( K x. _pi ) ) ) ) = ( abs ` ( sin ` 0 ) ) )
13 sin0
 |-  ( sin ` 0 ) = 0
14 13 fveq2i
 |-  ( abs ` ( sin ` 0 ) ) = ( abs ` 0 )
15 abs0
 |-  ( abs ` 0 ) = 0
16 14 15 eqtri
 |-  ( abs ` ( sin ` 0 ) ) = 0
17 12 16 eqtrdi
 |-  ( K e. ZZ -> ( abs ` ( sin ` ( 0 + ( K x. _pi ) ) ) ) = 0 )
18 10 17 abs00d
 |-  ( K e. ZZ -> ( sin ` ( 0 + ( K x. _pi ) ) ) = 0 )
19 6 18 eqtr3d
 |-  ( K e. ZZ -> ( sin ` ( K x. _pi ) ) = 0 )