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 )