Metamath Proof Explorer

Theorem sin0

Description: Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005)

Ref Expression
Assertion sin0 
|- ( sin ` 0 ) = 0

Proof

Step Hyp Ref Expression
1 neg0 
 |-  -u 0 = 0
2 1 fveq2i 
 |-  ( sin ` -u 0 ) = ( sin ` 0 )
3 0cn 
 |-  0 e. CC
4 sinneg 
 |-  ( 0 e. CC -> ( sin ` -u 0 ) = -u ( sin ` 0 ) )
5 3 4 ax-mp 
 |-  ( sin ` -u 0 ) = -u ( sin ` 0 )
6 2 5 eqtr3i 
 |-  ( sin ` 0 ) = -u ( sin ` 0 )
7 sincl 
 |-  ( 0 e. CC -> ( sin ` 0 ) e. CC )
8 3 7 ax-mp 
 |-  ( sin ` 0 ) e. CC
9 8 eqnegi 
 |-  ( ( sin ` 0 ) = -u ( sin ` 0 ) <-> ( sin ` 0 ) = 0 )
10 6 9 mpbi 
 |-  ( sin ` 0 ) = 0