Metamath Proof Explorer


Theorem sin2kpi

Description: If K is an integer, then the sine of 2 K _pi is 0. (Contributed by Paul Chapman, 23-Jan-2008) (Revised by Mario Carneiro, 10-May-2014)

Ref Expression
Assertion sin2kpi ( 𝐾 ∈ ℤ → ( sin ‘ ( 𝐾 · ( 2 · π ) ) ) = 0 )

Proof

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 )