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 syl6eq 
 |-  ( 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 )