Theorem relogmul

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 Steve Rodriguez, 25-Nov-2007)

	Ref	Expression
Assertion	relogmul	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \log AB=\log A+\log B$$

Proof

Step	Hyp	Ref	Expression
1		efadd	$$⊢\left(\log A\in ℂ\wedge \log B\in ℂ\right)\to {\mathrm{e}}^{\log A+\log B}={\mathrm{e}}^{\log A}{\mathrm{e}}^{\log B}$$
2		readdcl	$$⊢\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 AB=\log A+\log B$$