Metamath Proof Explorer

Theorem relog

Description: Real part of a logarithm. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion relog ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) = ( log ‘ ( abs ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 logcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
2 1 recld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
3 relogef ⊢ ( ( ℜ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ → ( log ‘ ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( ℜ ‘ ( log ‘ 𝐴 ) ) )
4 2 3 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( ℜ ‘ ( log ‘ 𝐴 ) ) )
5 absef ⊢ ( ( log ‘ 𝐴 ) ∈ ℂ → ( abs ‘ ( exp ‘ ( log ‘ 𝐴 ) ) ) = ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) )
6 1 5 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( exp ‘ ( log ‘ 𝐴 ) ) ) = ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) )
7 eflog ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
8 7 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( exp ‘ ( log ‘ 𝐴 ) ) ) = ( abs ‘ 𝐴 ) )
9 6 8 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) = ( abs ‘ 𝐴 ) )
10 9 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ ( exp ‘ ( ℜ ‘ ( log ‘ 𝐴 ) ) ) ) = ( log ‘ ( abs ‘ 𝐴 ) ) )
11 4 10 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℜ ‘ ( log ‘ 𝐴 ) ) = ( log ‘ ( abs ‘ 𝐴 ) ) )