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 x. _pi ) ) = 0

Proof

Step Hyp Ref Expression
1 picn 
 |-  _pi e. CC
2 sin2t 
 |-  ( _pi e. CC -> ( sin ` ( 2 x. _pi ) ) = ( 2 x. ( ( sin ` _pi ) x. ( cos ` _pi ) ) ) )
3 1 2 ax-mp 
 |-  ( sin ` ( 2 x. _pi ) ) = ( 2 x. ( ( sin ` _pi ) x. ( cos ` _pi ) ) )
4 sinpi 
 |-  ( sin ` _pi ) = 0
5 cospi 
 |-  ( cos ` _pi ) = -u 1
6 4 5 oveq12i 
 |-  ( ( sin ` _pi ) x. ( cos ` _pi ) ) = ( 0 x. -u 1 )
7 neg1cn 
 |-  -u 1 e. CC
8 7 mul02i 
 |-  ( 0 x. -u 1 ) = 0
9 6 8 eqtri 
 |-  ( ( sin ` _pi ) x. ( cos ` _pi ) ) = 0
10 9 oveq2i 
 |-  ( 2 x. ( ( sin ` _pi ) x. ( cos ` _pi ) ) ) = ( 2 x. 0 )
11 2t0e0 
 |-  ( 2 x. 0 ) = 0
12 10 11 eqtri 
 |-  ( 2 x. ( ( sin ` _pi ) x. ( cos ` _pi ) ) ) = 0
13 3 12 eqtri 
 |-  ( sin ` ( 2 x. _pi ) ) = 0