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 ) ) ) )