This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efmival

Description: The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006)

Ref Expression
Assertion efmival 
|- ( A e. CC -> ( exp ` ( -u _i x. A ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 mulneg12 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( -u _i x. A ) = ( _i x. -u A ) )
3 1 2 mpan 
 |-  ( A e. CC -> ( -u _i x. A ) = ( _i x. -u A ) )
4 3 fveq2d 
 |-  ( A e. CC -> ( exp ` ( -u _i x. A ) ) = ( exp ` ( _i x. -u A ) ) )
5 negcl 
 |-  ( A e. CC -> -u A e. CC )
6 efival 
 |-  ( -u A e. CC -> ( exp ` ( _i x. -u A ) ) = ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) )
7 5 6 syl 
 |-  ( A e. CC -> ( exp ` ( _i x. -u A ) ) = ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) )
8 cosneg 
 |-  ( A e. CC -> ( cos ` -u A ) = ( cos ` A ) )
9 sinneg 
 |-  ( A e. CC -> ( sin ` -u A ) = -u ( sin ` A ) )
10 9 oveq2d 
 |-  ( A e. CC -> ( _i x. ( sin ` -u A ) ) = ( _i x. -u ( sin ` A ) ) )
11 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
12 mulneg2 
 |-  ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. -u ( sin ` A ) ) = -u ( _i x. ( sin ` A ) ) )
13 1 11 12 sylancr 
 |-  ( A e. CC -> ( _i x. -u ( sin ` A ) ) = -u ( _i x. ( sin ` A ) ) )
14 10 13 eqtrd 
 |-  ( A e. CC -> ( _i x. ( sin ` -u A ) ) = -u ( _i x. ( sin ` A ) ) )
15 8 14 oveq12d 
 |-  ( A e. CC -> ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) = ( ( cos ` A ) + -u ( _i x. ( sin ` A ) ) ) )
16 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
17 mulcl 
 |-  ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. ( sin ` A ) ) e. CC )
18 1 11 17 sylancr 
 |-  ( A e. CC -> ( _i x. ( sin ` A ) ) e. CC )
19 16 18 negsubd 
 |-  ( A e. CC -> ( ( cos ` A ) + -u ( _i x. ( sin ` A ) ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )
20 15 19 eqtrd 
 |-  ( A e. CC -> ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )
21 7 20 eqtrd 
 |-  ( A e. CC -> ( exp ` ( _i x. -u A ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )
22 4 21 eqtrd 
 |-  ( A e. CC -> ( exp ` ( -u _i x. A ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )