Theorem sin2pi

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

	Ref	Expression
Assertion	sin2pi	⊢ ( sin ‘ ( 2 · π ) ) = 0

Proof

Step	Hyp	Ref	Expression
1		picn	⊢ π ∈ ℂ
2		sin2t	⊢ ( π ∈ ℂ → ( sin ‘ ( 2 · π ) ) = ( 2 · ( ( sin ‘ π ) · ( cos ‘ π ) ) ) )
3	1 2	ax-mp	⊢ ( sin ‘ ( 2 · π ) ) = ( 2 · ( ( sin ‘ π ) · ( cos ‘ π ) ) )
4		sinpi	⊢ ( sin ‘ π ) = 0
5		cospi	⊢ ( cos ‘ π ) = - 1
6	4 5	oveq12i	⊢ ( ( sin ‘ π ) · ( cos ‘ π ) ) = ( 0 · - 1 )
7		neg1cn	⊢ - 1 ∈ ℂ
8	7	mul02i	⊢ ( 0 · - 1 ) = 0
9	6 8	eqtri	⊢ ( ( sin ‘ π ) · ( cos ‘ π ) ) = 0
10	9	oveq2i	⊢ ( 2 · ( ( sin ‘ π ) · ( cos ‘ π ) ) ) = ( 2 · 0 )
11		2t0e0	⊢ ( 2 · 0 ) = 0
12	10 11	eqtri	⊢ ( 2 · ( ( sin ‘ π ) · ( cos ‘ π ) ) ) = 0
13	3 12	eqtri	⊢ ( sin ‘ ( 2 · π ) ) = 0