sinkpi

Description: The sine of an integer multiple of _pi is 0. (Contributed by NM, 11-Aug-2008)

		Ref	Expression
	Assertion	sinkpi	$⊢ K \in ℤ \to \sin K π = 0$

Step	Hyp	Ref	Expression
1		zcn	$⊢ K \in ℤ \to K \in ℂ$
2		picn	$⊢ π \in ℂ$
3		mulcl	$⊢ (K \in ℂ \land π \in ℂ) \to K π \in ℂ$
4	1 2 3	sylancl	$⊢ K \in ℤ \to K π \in ℂ$
5	4	addlidd	$⊢ K \in ℤ \to 0 + K π = K π$
6	5	fveq2d	$⊢ K \in ℤ \to \sin (0 + K π) = \sin K π$
7		0cn	$⊢ 0 \in ℂ$
8		addcl	$⊢ (0 \in ℂ \land K π \in ℂ) \to 0 + K π \in ℂ$
9	7 4 8	sylancr	$⊢ K \in ℤ \to 0 + K π \in ℂ$
10	9	sincld	$⊢ K \in ℤ \to \sin (0 + K π) \in ℂ$
11		abssinper	$⊢ (0 \in ℂ \land K \in ℤ) \to \|\sin (0 + K π)\| = \|\sin 0\|$
12	7 11	mpan	$⊢ K \in ℤ \to \|\sin (0 + K π)\| = \|\sin 0\|$
13		sin0	$⊢ \sin 0 = 0$
14	13	fveq2i	$⊢ \|\sin 0\| = \|0\|$
15		abs0	$⊢ \|0\| = 0$
16	14 15	eqtri	$⊢ \|\sin 0\| = 0$
17	12 16	eqtrdi	$⊢ K \in ℤ \to \|\sin (0 + K π)\| = 0$
18	10 17	abs00d	$⊢ K \in ℤ \to \sin (0 + K π) = 0$
19	6 18	eqtr3d	$⊢ K \in ℤ \to \sin K π = 0$

Metamath Proof Explorer