ELF.APP.4 : $ \ln(y) = \log_{base}( y ) \cdot ln(base) $ or $\log_{base}(y) = \frac{\ln(y)} {\ln(base)}$
  Proof : Apply $\ln(b^p)=p\ln(b)$ with $b = base ; p = \log_{base}(y)$.
So $y = b^p = base^{ \log_{base}(y)}$ and thus $\ln(y) = \log_{base}(y) \cdot \ln(base).$

This can also be proven directly by using the inverse relation of  $\ln  $ and  $ \exp_{e}$ for the $base$.
Let $\ln(base)=a$  so $e^a=base$.
Here's what that looks like on a mapping diagram:MD exp log inverse
Next we consider  $x= \log_{base} (y)$ so  $base^x = y$.
Then  $(e^a)^x =e^{ax} = y $.


Here's what that looks like on a mapping diagram:Md for (e^a)^x ... =y


and thus we have the corresponding logarithmic equation:
$\ln(y)=ax= \ln(base) \cdot  \log_{base}(y)$.


Here's what that looks like on a mapping diagram:MD for ln(y)= ...

And here's a mapping diagram showing the product of the logarithms visualized as well:
MD for the entire proof
Finally here is a dynamic visualization of the proof using mapping diagrams:
Proof of $ \ ln(y) = \log_{base}( y ) \cdot ln(base) $

Martin Flashman, 26 Oct 2014, revised 24 Aug 2016, Created with GeoGebra