Theorem sinkpi

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

	Ref	Expression
Assertion	sinkpi	$$⊢K\in \mathbb{Z}\to \sin K\mathrm{\pi }=0$$

Proof

Step	Hyp	Ref	Expression
1		zcn	$$⊢K\in \mathbb{Z}\to K\in ℂ$$
2		picn	$$⊢\mathrm{\pi }\in ℂ$$
3		mulcl	$$⊢\left(K\in ℂ\wedge \mathrm{\pi }\in ℂ\right)\to K\mathrm{\pi }\in ℂ$$
4	1 2 3	sylancl	$$⊢K\in \mathbb{Z}\to K\mathrm{\pi }\in ℂ$$
5	4	addid2d	$$⊢K\in \mathbb{Z}\to 0+K\mathrm{\pi }=K\mathrm{\pi }$$
6	5	fveq2d	$$⊢K\in \mathbb{Z}\to \sin \left(0+K\mathrm{\pi }\right)=\sin K\mathrm{\pi }$$
7		0cn	$$⊢0\in ℂ$$
8		addcl	$$⊢\left(0\in ℂ\wedge K\mathrm{\pi }\in ℂ\right)\to 0+K\mathrm{\pi }\in ℂ$$
9	7 4 8	sylancr	$$⊢K\in \mathbb{Z}\to 0+K\mathrm{\pi }\in ℂ$$
10	9	sincld	$$⊢K\in \mathbb{Z}\to \sin \left(0+K\mathrm{\pi }\right)\in ℂ$$
11		abssinper	$$⊢\left(0\in ℂ\wedge K\in \mathbb{Z}\right)\to \left|\sin \left(0+K\mathrm{\pi }\right)\right|=\left|\sin 0\right|$$
12	7 11	mpan	$$⊢K\in \mathbb{Z}\to \left|\sin \left(0+K\mathrm{\pi }\right)\right|=\left|\sin 0\right|$$
13		sin0	$$⊢\sin 0=0$$
14	13	fveq2i	$$⊢\left|\sin 0\right|=\left|0\right|$$
15		abs0	$$⊢\left|0\right|=0$$
16	14 15	eqtri	$$⊢\left|\sin 0\right|=0$$
17	12 16	eqtrdi	$$⊢K\in \mathbb{Z}\to \left|\sin \left(0+K\mathrm{\pi }\right)\right|=0$$
18	10 17	abs00d	$$⊢K\in \mathbb{Z}\to \sin \left(0+K\mathrm{\pi }\right)=0$$
19	6 18	eqtr3d	$$⊢K\in \mathbb{Z}\to \sin K\mathrm{\pi }=0$$