This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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