By claim 5 of \ref{thm:exponential-properties-2026a}, the \reftext{def:exponential-function-real-2026a}{exponential function} is a \reftext{def:bijection-sets-2026a}{bijection} from $\mathbb{R}$ onto the \reftext{def:interval-real-line-c54-2026c}{interval} $(0,\infty)$. The \textbf{natural logarithm} is its inverse function

By claim 3 of \ref{thm:exponential-properties-2026a} and the \reftext{thm:smooth-local-inverse-euclidean-2026b}{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$.