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, 29May2016)
Ref  Expression  

Hypotheses  relogcld.1   ( ph > A e. RR+ ) 

relogmuld.2   ( ph > B e. RR+ ) 

Assertion  relogdivd   ( ph > ( log ` ( A / B ) ) = ( ( log ` A )  ( log ` B ) ) ) 
Step  Hyp  Ref  Expression 

1  relogcld.1   ( ph > A e. RR+ ) 

2  relogmuld.2   ( ph > B e. RR+ ) 

3  relogdiv   ( ( A e. RR+ /\ B e. RR+ ) > ( log ` ( A / B ) ) = ( ( log ` A )  ( log ` B ) ) ) 

4  1 2 3  syl2anc   ( ph > ( log ` ( A / B ) ) = ( ( log ` A )  ( log ` B ) ) ) 