Metamath Proof Explorer


Theorem sin2pi

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

Ref Expression
Assertion sin2pi sin2π=0

Proof

Step Hyp Ref Expression
1 picn π
2 sin2t πsin2π=2sinπcosπ
3 1 2 ax-mp sin2π=2sinπ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 2sinπcosπ=20
11 2t0e0 20=0
12 10 11 eqtri 2sinπcosπ=0
13 3 12 eqtri sin2π=0