Metamath Proof Explorer

Theorem sinval

Description: Value of the sine function. (Contributed by NM, 14-Mar-2005) (Revised by Mario Carneiro, 10-Nov-2013)

Ref Expression
Assertion sinval 
|- ( A e. CC -> ( sin ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = A -> ( _i x. x ) = ( _i x. A ) )
2 1 fveq2d 
 |-  ( x = A -> ( exp ` ( _i x. x ) ) = ( exp ` ( _i x. A ) ) )
3 oveq2 
 |-  ( x = A -> ( -u _i x. x ) = ( -u _i x. A ) )
4 3 fveq2d 
 |-  ( x = A -> ( exp ` ( -u _i x. x ) ) = ( exp ` ( -u _i x. A ) ) )
5 2 4 oveq12d 
 |-  ( x = A -> ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) = ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) )
6 5 oveq1d 
 |-  ( x = A -> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
7 df-sin 
 |-  sin = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) - ( exp ` ( -u _i x. x ) ) ) / ( 2 x. _i ) ) )
8 ovex 
 |-  ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) e. _V
9 6 7 8 fvmpt 
 |-  ( A e. CC -> ( sin ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )