Step |
Hyp |
Ref |
Expression |
1 |
|
zcn |
⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ ) |
2 |
|
2cn |
⊢ 2 ∈ ℂ |
3 |
|
picn |
⊢ π ∈ ℂ |
4 |
2 3
|
mulcli |
⊢ ( 2 · π ) ∈ ℂ |
5 |
|
mulcl |
⊢ ( ( 𝐾 ∈ ℂ ∧ ( 2 · π ) ∈ ℂ ) → ( 𝐾 · ( 2 · π ) ) ∈ ℂ ) |
6 |
1 4 5
|
sylancl |
⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · ( 2 · π ) ) ∈ ℂ ) |
7 |
6
|
addid2d |
⊢ ( 𝐾 ∈ ℤ → ( 0 + ( 𝐾 · ( 2 · π ) ) ) = ( 𝐾 · ( 2 · π ) ) ) |
8 |
7
|
fveq2d |
⊢ ( 𝐾 ∈ ℤ → ( sin ‘ ( 0 + ( 𝐾 · ( 2 · π ) ) ) ) = ( sin ‘ ( 𝐾 · ( 2 · π ) ) ) ) |
9 |
|
0cn |
⊢ 0 ∈ ℂ |
10 |
|
sinper |
⊢ ( ( 0 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( sin ‘ ( 0 + ( 𝐾 · ( 2 · π ) ) ) ) = ( sin ‘ 0 ) ) |
11 |
9 10
|
mpan |
⊢ ( 𝐾 ∈ ℤ → ( sin ‘ ( 0 + ( 𝐾 · ( 2 · π ) ) ) ) = ( sin ‘ 0 ) ) |
12 |
|
sin0 |
⊢ ( sin ‘ 0 ) = 0 |
13 |
11 12
|
eqtrdi |
⊢ ( 𝐾 ∈ ℤ → ( sin ‘ ( 0 + ( 𝐾 · ( 2 · π ) ) ) ) = 0 ) |
14 |
8 13
|
eqtr3d |
⊢ ( 𝐾 ∈ ℤ → ( sin ‘ ( 𝐾 · ( 2 · π ) ) ) = 0 ) |