The Natural Logarithm

By claim 5 of Basic Properties of the Exponential Function, the exponential function is a bijection from $\mathbb{R}$ onto the interval $(0,\infty)$. The natural logarithm is its inverse function

By claim 3 of Basic Properties of the Exponential Function and the smooth inverse function theorem (with $n=1$; the Jacobian determinant of $\exp$ at $u$ is $\exp(u)\ne 0$), $\log$ is smooth on $(0,\infty)$ with derivative $\log'(t)=1/t$, and by claim 1 it satisfies $\log(st)=\log(s)+\log(t)$ for all $s,t>0$.