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