Metamath Proof Explorer

Theorem cosval

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

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

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 ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )
7 df-cos 
 |-  cos = ( x e. CC |-> ( ( ( exp ` ( _i x. x ) ) + ( exp ` ( -u _i x. x ) ) ) / 2 ) )
8 ovex 
 |-  ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) e. _V
9 6 7 8 fvmpt 
 |-  ( A e. CC -> ( cos ` A ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )