Metamath Proof Explorer

Theorem absef

Description: The absolute value of the exponential is the exponential of the real part. (Contributed by Paul Chapman, 13-Sep-2007)

Ref Expression
Assertion absef 
|- ( A e. CC -> ( abs ` ( exp ` A ) ) = ( exp ` ( Re ` 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 2 11 eqtrd 
 |-  ( A e. CC -> ( exp ` A ) = ( ( exp ` ( Re ` A ) ) x. ( exp ` ( _i x. ( Im ` A ) ) ) ) )
13 12 fveq2d 
 |-  ( A e. CC -> ( abs ` ( exp ` A ) ) = ( abs ` ( ( exp ` ( Re ` A ) ) x. ( exp ` ( _i x. ( Im ` A ) ) ) ) ) )
14 3 reefcld 
 |-  ( A e. CC -> ( exp ` ( Re ` A ) ) e. RR )
15 14 recnd 
 |-  ( A e. CC -> ( exp ` ( Re ` A ) ) e. CC )
16 efcl 
 |-  ( ( _i x. ( Im ` A ) ) e. CC -> ( exp ` ( _i x. ( Im ` A ) ) ) e. CC )
17 9 16 syl 
 |-  ( A e. CC -> ( exp ` ( _i x. ( Im ` A ) ) ) e. CC )
18 15 17 absmuld 
 |-  ( A e. CC -> ( abs ` ( ( exp ` ( Re ` A ) ) x. ( exp ` ( _i x. ( Im ` A ) ) ) ) ) = ( ( abs ` ( exp ` ( Re ` A ) ) ) x. ( abs ` ( exp ` ( _i x. ( Im ` A ) ) ) ) ) )
19 absefi 
 |-  ( ( Im ` A ) e. RR -> ( abs ` ( exp ` ( _i x. ( Im ` A ) ) ) ) = 1 )
20 6 19 syl 
 |-  ( A e. CC -> ( abs ` ( exp ` ( _i x. ( Im ` A ) ) ) ) = 1 )
21 20 oveq2d 
 |-  ( A e. CC -> ( ( abs ` ( exp ` ( Re ` A ) ) ) x. ( abs ` ( exp ` ( _i x. ( Im ` A ) ) ) ) ) = ( ( abs ` ( exp ` ( Re ` A ) ) ) x. 1 ) )
22 13 18 21 3eqtrd 
 |-  ( A e. CC -> ( abs ` ( exp ` A ) ) = ( ( abs ` ( exp ` ( Re ` A ) ) ) x. 1 ) )
23 15 abscld 
 |-  ( A e. CC -> ( abs ` ( exp ` ( Re ` A ) ) ) e. RR )
24 23 recnd 
 |-  ( A e. CC -> ( abs ` ( exp ` ( Re ` A ) ) ) e. CC )
25 24 mulid1d 
 |-  ( A e. CC -> ( ( abs ` ( exp ` ( Re ` A ) ) ) x. 1 ) = ( abs ` ( exp ` ( Re ` A ) ) ) )
26 efgt0 
 |-  ( ( Re ` A ) e. RR -> 0 < ( exp ` ( Re ` A ) ) )
27 3 26 syl 
 |-  ( A e. CC -> 0 < ( exp ` ( Re ` A ) ) )
28 0re 
 |-  0 e. RR
29 ltle 
 |-  ( ( 0 e. RR /\ ( exp ` ( Re ` A ) ) e. RR ) -> ( 0 < ( exp ` ( Re ` A ) ) -> 0 <_ ( exp ` ( Re ` A ) ) ) )
30 28 14 29 sylancr 
 |-  ( A e. CC -> ( 0 < ( exp ` ( Re ` A ) ) -> 0 <_ ( exp ` ( Re ` A ) ) ) )
31 27 30 mpd 
 |-  ( A e. CC -> 0 <_ ( exp ` ( Re ` A ) ) )
32 14 31 absidd 
 |-  ( A e. CC -> ( abs ` ( exp ` ( Re ` A ) ) ) = ( exp ` ( Re ` A ) ) )
33 22 25 32 3eqtrd 
 |-  ( A e. CC -> ( abs ` ( exp ` A ) ) = ( exp ` ( Re ` A ) ) )