Metamath Proof Explorer

Theorem resinval

Description: The sine of a real number in terms of the exponential function. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion resinval 
|- ( A e. RR -> ( sin ` A ) = ( Im ` ( exp ` ( _i x. A ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 recn 
 |-  ( A e. RR -> A e. CC )
3 cjmul 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( * ` ( _i x. A ) ) = ( ( * ` _i ) x. ( * ` A ) ) )
4 1 2 3 sylancr 
 |-  ( A e. RR -> ( * ` ( _i x. A ) ) = ( ( * ` _i ) x. ( * ` A ) ) )
5 cji 
 |-  ( * ` _i ) = -u _i
6 5 oveq1i 
 |-  ( ( * ` _i ) x. ( * ` A ) ) = ( -u _i x. ( * ` A ) )
7 cjre 
 |-  ( A e. RR -> ( * ` A ) = A )
8 7 oveq2d 
 |-  ( A e. RR -> ( -u _i x. ( * ` A ) ) = ( -u _i x. A ) )
9 6 8 eqtrid 
 |-  ( A e. RR -> ( ( * ` _i ) x. ( * ` A ) ) = ( -u _i x. A ) )
10 4 9 eqtrd 
 |-  ( A e. RR -> ( * ` ( _i x. A ) ) = ( -u _i x. A ) )
11 10 fveq2d 
 |-  ( A e. RR -> ( exp ` ( * ` ( _i x. A ) ) ) = ( exp ` ( -u _i x. A ) ) )
12 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
13 1 2 12 sylancr 
 |-  ( A e. RR -> ( _i x. A ) e. CC )
14 efcj 
 |-  ( ( _i x. A ) e. CC -> ( exp ` ( * ` ( _i x. A ) ) ) = ( * ` ( exp ` ( _i x. A ) ) ) )
15 13 14 syl 
 |-  ( A e. RR -> ( exp ` ( * ` ( _i x. A ) ) ) = ( * ` ( exp ` ( _i x. A ) ) ) )
16 11 15 eqtr3d 
 |-  ( A e. RR -> ( exp ` ( -u _i x. A ) ) = ( * ` ( exp ` ( _i x. A ) ) ) )
17 16 oveq2d 
 |-  ( A e. RR -> ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) - ( * ` ( exp ` ( _i x. A ) ) ) ) )
18 17 oveq1d 
 |-  ( A e. RR -> ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) = ( ( ( exp ` ( _i x. A ) ) - ( * ` ( exp ` ( _i x. A ) ) ) ) / ( 2 x. _i ) ) )
19 sinval 
 |-  ( A e. CC -> ( sin ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
20 2 19 syl 
 |-  ( A e. RR -> ( sin ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
21 efcl 
 |-  ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) e. CC )
22 imval2 
 |-  ( ( exp ` ( _i x. A ) ) e. CC -> ( Im ` ( exp ` ( _i x. A ) ) ) = ( ( ( exp ` ( _i x. A ) ) - ( * ` ( exp ` ( _i x. A ) ) ) ) / ( 2 x. _i ) ) )
23 13 21 22 3syl 
 |-  ( A e. RR -> ( Im ` ( exp ` ( _i x. A ) ) ) = ( ( ( exp ` ( _i x. A ) ) - ( * ` ( exp ` ( _i x. A ) ) ) ) / ( 2 x. _i ) ) )
24 18 20 23 3eqtr4d 
 |-  ( A e. RR -> ( sin ` A ) = ( Im ` ( exp ` ( _i x. A ) ) ) )