Metamath Proof Explorer

Theorem efiarg

Description: The exponential of the "arg" function Im o. log . (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion efiarg ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
2 1 recld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
3 2 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
4 efsub ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( ℜ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) )
5 1 3 4 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) )
6 ax-icn ⊢ i ∈ ℂ
7 1 imcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
8 7 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
9 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ ) → ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ )
10 6 8 9 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℂ )
11 1 replimd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) = ( ( ℜ ‘ ( log ‘ 𝐴 ) ) + ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
12 3 10 11 mvrladdd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( log ‘ 𝐴 ) − ( ℜ ‘ ( log ‘ 𝐴 ) ) ) = ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
13 12 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
14 eflog ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
15 relog ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) = ( log ‘ ( abs ‘ 𝐴 ) ) )
16 15 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) = ( exp ‘ ( log ‘ ( abs ‘ 𝐴 ) ) ) )
17 abscl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )
18 17 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
19 18 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
20 absrpcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
21 20 rpne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ≠ 0 )
22 eflog ⊢ ( ( ( abs ‘ 𝐴 ) ∈ ℂ ∧ ( abs ‘ 𝐴 ) ≠ 0 ) → ( exp ‘ ( log ‘ ( abs ‘ 𝐴 ) ) ) = ( abs ‘ 𝐴 ) )
23 19 21 22 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ ( abs ‘ 𝐴 ) ) ) = ( abs ‘ 𝐴 ) )
24 16 23 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) = ( abs ‘ 𝐴 ) )
25 14 24 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )
26 5 13 25 3eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )