Step |
Hyp |
Ref |
Expression |
1 |
|
zcn |
|- ( K e. ZZ -> K e. CC ) |
2 |
|
2cn |
|- 2 e. CC |
3 |
|
picn |
|- _pi e. CC |
4 |
2 3
|
mulcli |
|- ( 2 x. _pi ) e. CC |
5 |
|
mulcl |
|- ( ( K e. CC /\ ( 2 x. _pi ) e. CC ) -> ( K x. ( 2 x. _pi ) ) e. CC ) |
6 |
1 4 5
|
sylancl |
|- ( K e. ZZ -> ( K x. ( 2 x. _pi ) ) e. CC ) |
7 |
6
|
addid2d |
|- ( K e. ZZ -> ( 0 + ( K x. ( 2 x. _pi ) ) ) = ( K x. ( 2 x. _pi ) ) ) |
8 |
7
|
fveq2d |
|- ( K e. ZZ -> ( sin ` ( 0 + ( K x. ( 2 x. _pi ) ) ) ) = ( sin ` ( K x. ( 2 x. _pi ) ) ) ) |
9 |
|
0cn |
|- 0 e. CC |
10 |
|
sinper |
|- ( ( 0 e. CC /\ K e. ZZ ) -> ( sin ` ( 0 + ( K x. ( 2 x. _pi ) ) ) ) = ( sin ` 0 ) ) |
11 |
9 10
|
mpan |
|- ( K e. ZZ -> ( sin ` ( 0 + ( K x. ( 2 x. _pi ) ) ) ) = ( sin ` 0 ) ) |
12 |
|
sin0 |
|- ( sin ` 0 ) = 0 |
13 |
11 12
|
eqtrdi |
|- ( K e. ZZ -> ( sin ` ( 0 + ( K x. ( 2 x. _pi ) ) ) ) = 0 ) |
14 |
8 13
|
eqtr3d |
|- ( K e. ZZ -> ( sin ` ( K x. ( 2 x. _pi ) ) ) = 0 ) |