Metamath Proof Explorer


Theorem efeul

Description: Eulerian representation of the complex exponential. (Suggested by Jeff Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006)

Ref Expression
Assertion efeul
|- ( A e. CC -> ( exp ` A ) = ( ( exp ` ( Re ` A ) ) x. ( ( cos ` ( Im ` A ) ) + ( _i x. ( sin ` ( Im ` A ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 replim
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
2 1 fveq2d
 |-  ( A e. CC -> ( exp ` A ) = ( exp ` ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) ) )
3 recl
 |-  ( A e. CC -> ( Re ` A ) e. RR )
4 3 recnd
 |-  ( A e. CC -> ( Re ` A ) e. CC )
5 ax-icn
 |-  _i e. CC
6 imcl
 |-  ( A e. CC -> ( Im ` A ) e. RR )
7 6 recnd
 |-  ( A e. CC -> ( Im ` A ) e. CC )
8 mulcl
 |-  ( ( _i e. CC /\ ( Im ` A ) e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
9 5 7 8 sylancr
 |-  ( A e. CC -> ( _i x. ( Im ` A ) ) e. CC )
10 efadd
 |-  ( ( ( Re ` A ) e. CC /\ ( _i x. ( Im ` A ) ) e. CC ) -> ( exp ` ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) ) = ( ( exp ` ( Re ` A ) ) x. ( exp ` ( _i x. ( Im ` A ) ) ) ) )
11 4 9 10 syl2anc
 |-  ( A e. CC -> ( exp ` ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) ) = ( ( exp ` ( Re ` A ) ) x. ( exp ` ( _i x. ( Im ` A ) ) ) ) )
12 efival
 |-  ( ( Im ` A ) e. CC -> ( exp ` ( _i x. ( Im ` A ) ) ) = ( ( cos ` ( Im ` A ) ) + ( _i x. ( sin ` ( Im ` A ) ) ) ) )
13 7 12 syl
 |-  ( A e. CC -> ( exp ` ( _i x. ( Im ` A ) ) ) = ( ( cos ` ( Im ` A ) ) + ( _i x. ( sin ` ( Im ` A ) ) ) ) )
14 13 oveq2d
 |-  ( A e. CC -> ( ( exp ` ( Re ` A ) ) x. ( exp ` ( _i x. ( Im ` A ) ) ) ) = ( ( exp ` ( Re ` A ) ) x. ( ( cos ` ( Im ` A ) ) + ( _i x. ( sin ` ( Im ` A ) ) ) ) ) )
15 2 11 14 3eqtrd
 |-  ( A e. CC -> ( exp ` A ) = ( ( exp ` ( Re ` A ) ) x. ( ( cos ` ( Im ` A ) ) + ( _i x. ( sin ` ( Im ` A ) ) ) ) ) )