> [!Definition] Theorem (Logarithm) > There exists a [[Continuous Real Function|continuous]] strictly increasing function $x \mapsto \log x$ defined on $(0, \infty)$ that is the is inverse of the [[Real Exponential Function|exponential function]] i.e. $\exp(\log x)=x$for all $x\in(0,\infty)$ and $\log(\exp(y))=y$ for all $y\in \mathbb{R}$. **Proof**: Follows directly from [[Inverse of Strictly Monotonic Continuous Real Function Exists, is Strictly Monotonic in the Same Sense, and is Continuous]] since the [[Real Exponential Function is Strictly Increasing|exponential function is strictly increasing]] and [[Continuity of Real Power Series About Zero on Interval of Convergence|continuous]].