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