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	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \log \left(\frac{A}{B}\right)=\log A-\log B$$

Proof

Step	Hyp	Ref	Expression
1		efsub	$$⊢\left(\log A\in ℂ\wedge \log B\in ℂ\right)\to {\mathrm{e}}^{\log A-\log B}=\frac{{\mathrm{e}}^{\log A}}{{\mathrm{e}}^{\log B}}$$
2		resubcl	$$⊢\left(\log A\in ℝ\wedge \log B\in ℝ\right)\to \log A-\log B\in ℝ$$
3	1 2	relogoprlem	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \log \left(\frac{A}{B}\right)=\log A-\log B$$