Theorem sin2pi

Description: The sine of 2 _pi is 0. (Contributed by Paul Chapman, 23-Jan-2008)

	Ref	Expression
Assertion	sin2pi	$$⊢\sin 2\mathrm{\pi }=0$$

Proof

Step	Hyp	Ref	Expression
1		picn	$$⊢\mathrm{\pi }\in ℂ$$
2		sin2t	$$⊢\mathrm{\pi }\in ℂ\to \sin 2\mathrm{\pi }=2\sin \mathrm{\pi }\cos \mathrm{\pi }$$
3	1 2	ax-mp	$$⊢\sin 2\mathrm{\pi }=2\sin \mathrm{\pi }\cos \mathrm{\pi }$$
4		sinpi	$$⊢\sin \mathrm{\pi }=0$$
5		cospi	$$⊢\cos \mathrm{\pi }=-1$$
6	4 5	oveq12i	$$⊢\sin \mathrm{\pi }\cos \mathrm{\pi }=0\cdot -1$$
7		neg1cn	$$⊢-1\in ℂ$$
8	7	mul02i	$$⊢0\cdot -1=0$$
9	6 8	eqtri	$$⊢\sin \mathrm{\pi }\cos \mathrm{\pi }=0$$
10	9	oveq2i	$$⊢2\sin \mathrm{\pi }\cos \mathrm{\pi }=2\cdot 0$$
11		2t0e0	$$⊢2\cdot 0=0$$
12	10 11	eqtri	$$⊢2\sin \mathrm{\pi }\cos \mathrm{\pi }=0$$
13	3 12	eqtri	$$⊢\sin 2\mathrm{\pi }=0$$