Metamath Proof Explorer

Theorem relogdivd

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 Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses relogcld.1 φ A +
relogmuld.2 φ B +
Assertion relogdivd φ log A B = log A log B


Step Hyp Ref Expression
1 relogcld.1 φ A +
2 relogmuld.2 φ B +
3 relogdiv A + B + log A B = log A log B
4 1 2 3 syl2anc φ log A B = log A log B