This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐾 ∈ ℤ → ( sin ‘ ( 𝐾 · π ) ) = 0 )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
2 picn ⊢ π ∈ ℂ
3 mulcl ⊢ ( ( 𝐾 ∈ ℂ ∧ π ∈ ℂ ) → ( 𝐾 · π ) ∈ ℂ )
4 1 2 3 sylancl ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · π ) ∈ ℂ )
5 4 addlidd ⊢ ( 𝐾 ∈ ℤ → ( 0 + ( 𝐾 · π ) ) = ( 𝐾 · π ) )
6 5 fveq2d ⊢ ( 𝐾 ∈ ℤ → ( sin ‘ ( 0 + ( 𝐾 · π ) ) ) = ( sin ‘ ( 𝐾 · π ) ) )
7 0cn ⊢ 0 ∈ ℂ
8 addcl ⊢ ( ( 0 ∈ ℂ ∧ ( 𝐾 · π ) ∈ ℂ ) → ( 0 + ( 𝐾 · π ) ) ∈ ℂ )
9 7 4 8 sylancr ⊢ ( 𝐾 ∈ ℤ → ( 0 + ( 𝐾 · π ) ) ∈ ℂ )
10 9 sincld ⊢ ( 𝐾 ∈ ℤ → ( sin ‘ ( 0 + ( 𝐾 · π ) ) ) ∈ ℂ )
11 abssinper ⊢ ( ( 0 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( abs ‘ ( sin ‘ ( 0 + ( 𝐾 · π ) ) ) ) = ( abs ‘ ( sin ‘ 0 ) ) )
12 7 11 mpan ⊢ ( 𝐾 ∈ ℤ → ( abs ‘ ( sin ‘ ( 0 + ( 𝐾 · π ) ) ) ) = ( 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 ⊢ ( 𝐾 ∈ ℤ → ( abs ‘ ( sin ‘ ( 0 + ( 𝐾 · π ) ) ) ) = 0 )
18 10 17 abs00d ⊢ ( 𝐾 ∈ ℤ → ( sin ‘ ( 0 + ( 𝐾 · π ) ) ) = 0 )
19 6 18 eqtr3d ⊢ ( 𝐾 ∈ ℤ → ( sin ‘ ( 𝐾 · π ) ) = 0 )