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 relogmuld
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 Mario Carneiro , 29-May-2016)
Ref
Expression
Hypotheses
relogcld.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
relogmuld.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
Assertion
relogmuld ⊢ ( 𝜑 → ( log ‘ ( 𝐴 · 𝐵 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) )
Proof
Step
Hyp
Ref
Expression
1
relogcld.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2
relogmuld.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
3
relogmul ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( 𝐴 · 𝐵 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) )
4
1 2 3
syl2anc ⊢ ( 𝜑 → ( log ‘ ( 𝐴 · 𝐵 ) ) = ( ( log ‘ 𝐴 ) + ( log ‘ 𝐵 ) ) )