This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC REAL AND COMPLEX FUNCTIONS Basic trigonometry The natural logarithm on complex numbers relogmul
Description: The natural logarithm of the product of two positive real numbers is the
sum of natural logarithms. Property 2 of Cohen p. 301, restricted to
natural logarithms. (Contributed by Steve Rodriguez , 25-Nov-2007)
Ref
Expression
Assertion
relogmul ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( 𝐴 · 𝐵 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) )
Proof
Step
Hyp
Ref
Expression
1
efadd ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) · ( exp ‘ ( log ‘ 𝐵 ) ) ) )
2
readdcl ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ) → ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) ∈ ℝ )
3
1 2
relogoprlem ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( 𝐴 · 𝐵 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) )