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 ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ 𝐴 ) ) = ( exp ‘ ( ℜ ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 replim ⊢ ( 𝐴 ∈ ℂ → 𝐴 = ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) )
2 1 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = ( exp ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
3 recl ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
4 3 recnd ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℂ )
5 ax-icn ⊢ i ∈ ℂ
6 imcl ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
7 6 recnd ⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℂ )
8 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
9 5 7 8 sylancr ⊢ ( 𝐴 ∈ ℂ → ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ )
10 efadd ⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℂ ∧ ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ ) → ( exp ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( ℜ ‘ 𝐴 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
11 4 9 10 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ( ℜ ‘ 𝐴 ) + ( i · ( ℑ ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( ℜ ‘ 𝐴 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
12 2 11 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = ( ( exp ‘ ( ℜ ‘ 𝐴 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) )
13 12 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ 𝐴 ) ) = ( abs ‘ ( ( exp ‘ ( ℜ ‘ 𝐴 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
14 3 reefcld ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ℜ ‘ 𝐴 ) ) ∈ ℝ )
15 14 recnd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ℜ ‘ 𝐴 ) ) ∈ ℂ )
16 efcl ⊢ ( ( i · ( ℑ ‘ 𝐴 ) ) ∈ ℂ → ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ∈ ℂ )
17 9 16 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ∈ ℂ )
18 15 17 absmuld ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( ( exp ‘ ( ℜ ‘ 𝐴 ) ) · ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( ( abs ‘ ( exp ‘ ( ℜ ‘ 𝐴 ) ) ) · ( abs ‘ ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) )
19 absefi ⊢ ( ( ℑ ‘ 𝐴 ) ∈ ℝ → ( abs ‘ ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) = 1 )
20 6 19 syl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) = 1 )
21 20 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ ( exp ‘ ( ℜ ‘ 𝐴 ) ) ) · ( abs ‘ ( exp ‘ ( i · ( ℑ ‘ 𝐴 ) ) ) ) ) = ( ( abs ‘ ( exp ‘ ( ℜ ‘ 𝐴 ) ) ) · 1 ) )
22 13 18 21 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ 𝐴 ) ) = ( ( abs ‘ ( exp ‘ ( ℜ ‘ 𝐴 ) ) ) · 1 ) )
23 15 abscld ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ ( ℜ ‘ 𝐴 ) ) ) ∈ ℝ )
24 23 recnd ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ ( ℜ ‘ 𝐴 ) ) ) ∈ ℂ )
25 24 mulid1d ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ ( exp ‘ ( ℜ ‘ 𝐴 ) ) ) · 1 ) = ( abs ‘ ( exp ‘ ( ℜ ‘ 𝐴 ) ) ) )
26 efgt0 ⊢ ( ( ℜ ‘ 𝐴 ) ∈ ℝ → 0 < ( exp ‘ ( ℜ ‘ 𝐴 ) ) )
27 3 26 syl ⊢ ( 𝐴 ∈ ℂ → 0 < ( exp ‘ ( ℜ ‘ 𝐴 ) ) )
28 0re ⊢ 0 ∈ ℝ
29 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( exp ‘ ( ℜ ‘ 𝐴 ) ) ∈ ℝ ) → ( 0 < ( exp ‘ ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( exp ‘ ( ℜ ‘ 𝐴 ) ) ) )
30 28 14 29 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 0 < ( exp ‘ ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( exp ‘ ( ℜ ‘ 𝐴 ) ) ) )
31 27 30 mpd ⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( exp ‘ ( ℜ ‘ 𝐴 ) ) )
32 14 31 absidd ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ ( ℜ ‘ 𝐴 ) ) ) = ( exp ‘ ( ℜ ‘ 𝐴 ) ) )
33 22 25 32 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ ( exp ‘ 𝐴 ) ) = ( exp ‘ ( ℜ ‘ 𝐴 ) ) )