This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relogdiv

Description: The natural logarithm of the quotient of two positive real numbers is the difference of natural logarithms. Exercise 72(a) and Property 3 of Cohen p. 301, restricted to natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007)

Ref Expression
Assertion relogdiv ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( 𝐴 / 𝐵 ) ) = ( ( log ‘ 𝐴 ) − ( log ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 efsub ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ 𝐵 ) ∈ ℂ ) → ( exp ‘ ( ( log ‘ 𝐴 ) − ( log ‘ 𝐵 ) ) ) = ( ( exp ‘ ( log ‘ 𝐴 ) ) / ( exp ‘ ( log ‘ 𝐵 ) ) ) )
2 resubcl ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ) → ( ( log ‘ 𝐴 ) − ( log ‘ 𝐵 ) ) ∈ ℝ )
3 1 2 relogoprlem ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( log ‘ ( 𝐴 / 𝐵 ) ) = ( ( log ‘ 𝐴 ) − ( log ‘ 𝐵 ) ) )