Proof of Properties of the Natural Logarithm: Values at 1 and e, Products, Quotients, Monotonicity, Continuity, Derivative and the Bound log t at most t - 1

Values. By The Natural Logarithm (ii),

$$(\mathrm{V})\qquad \exp(\log t)=t\quad\text{for every }t\in(0,\infty),\qquad \log(\exp u)=u\quad\text{for every }u\in\mathbb{R}.$$

For $s,t\in(0,\infty)$ we have $st\in(0,\infty)$, as $0=0\cdot t<s\cdot t$ by Rules of Arithmetic and Order in an Ordered Field (i) and Rules of Arithmetic and Order in an Ordered Field (vi); $1/t\in(0,\infty)$ by Rules of Arithmetic and Order in an Ordered Field (viii); and $s/t=s\cdot(1/t)\in(0,\infty)$ in the same way, by Rules of Arithmetic and Order in an Ordered Field (vi).

Proof of (i). By Basic Properties of the Exponential Function (i), $\exp(0)=1$, so $\log(1)=\log(\exp(0))=0$ by $(\mathrm{V})$. By The Real Exponential Function (iii), $e=\exp(1)$, so $\log(e)=\log(\exp(1))=1$ by $(\mathrm{V})$.

Proof of (ii). Let $s,t\in(0,\infty)$. By Basic Properties of the Exponential Function (ii) and $(\mathrm{V})$,

$$\exp\bigl(\log(s)+\log(t)\bigr)=\exp(\log(s))\,\exp(\log(t))=st .$$

Applying $\log$ and $(\mathrm{V})$ gives $\log(st)=\log\bigl(\exp(\log(s)+\log(t))\bigr)=\log(s)+\log(t)$.

Proof of (iii). Let $s,t\in(0,\infty)$. By Basic Properties of the Exponential Function (iv) and $(\mathrm{V})$, $\exp(-\log(t))=1/\exp(\log(t))=1/t$, so $\log(1/t)=\log(\exp(-\log(t)))=-\log(t)$ by $(\mathrm{V})$. Then (ii), applied to $s$ and $1/t$, gives $\log(s/t)=\log(s\cdot(1/t))=\log(s)+\log(1/t)=\log(s)-\log(t)$.

The logarithm as an inverse function. Let $f=\exp:\mathbb{R}\to\mathbb{R}$. The set $\mathbb{R}$ is an interval containing two distinct points, by Basic Facts about Intervals of the Real Line (i); $f$ is continuous on $\mathbb{R}$, by Basic Properties of the Exponential Function (viii); and $f$ is strictly increasing in the sense of Inverse of a Continuous Strictly Increasing Function on an Interval: Continuity and Derivative ($f(s)<f(t)$ for all $s,t\in\mathbb{R}$ with $s<t$), by Basic Properties of the Exponential Function (ix). So Inverse of a Continuous Strictly Increasing Function on an Interval: Continuity and Derivative applies to $f$ on $\mathbb{R}$. Its image $J=f(\mathbb{R})$ is $(0,\infty)$: every $\exp(u)$ lies in $(0,\infty)$ by Basic Properties of the Exponential Function (iii), and every $t\in(0,\infty)$ is $\exp(u)$ for some $u\in\mathbb{R}$, because the map $\mathbb{R}\to(0,\infty)$, $u\mapsto\exp(u)$, is surjective by Basic Properties of the Exponential Function (xi). Let $g=f^{-1}:(0,\infty)\to\mathbb{R}$ be the inverse of the bijection $f:\mathbb{R}\to(0,\infty)$ of Inverse of a Continuous Strictly Increasing Function on an Interval: Continuity and Derivative (ii).

We show $g=\log$. The maps $\log\circ f:\mathbb{R}\to\mathbb{R}$ and $\mathrm{id}_{\mathbb{R}}$ have the values $\log(\exp(u))=u$ and $u$ at every $u\in\mathbb{R}$, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii), Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (iii) and $(\mathrm{V})$, so $\log\circ f=\mathrm{id}_{\mathbb{R}}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i). Likewise $f\circ\log:(0,\infty)\to(0,\infty)$ and $\mathrm{id}_{(0,\infty)}$ have the values $\exp(\log(t))=t$ and $t$ at every $t\in(0,\infty)$, so $f\circ\log=\mathrm{id}_{(0,\infty)}$. Hence $\log=f^{-1}=g$, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (vii).

Proof of (iv). Let $0<s<t$. Then $s,t\in(0,\infty)$, and $\log(s)=g(s)<g(t)=\log(t)$ by Inverse of a Continuous Strictly Increasing Function on an Interval: Continuity and Derivative (iii).

Proof of (v). By Inverse of a Continuous Strictly Increasing Function on an Interval: Continuity and Derivative (iv), $g=\log$, read as a map $(0,\infty)\to\mathbb{R}$, is continuous on $J=(0,\infty)$.

Proof of (vi). First, $\log$ is differentiable at every $t\in(0,\infty)$, relative to the interval $(0,\infty)$, with $\log'(t)=1/t$. Indeed, $(0,\infty)=J$ is an interval containing two distinct points, by Inverse of a Continuous Strictly Increasing Function on an Interval: Continuity and Derivative (i). Let $t\in(0,\infty)$ and $x=\log(t)\in\mathbb{R}$, so $f(x)=\exp(\log(t))=t$ by $(\mathrm{V})$. By Basic Properties of the Exponential Function (vii), applied to the interval $\mathbb{R}$, the restriction $\exp|_{\mathbb{R}}$, which is $\exp$ itself (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iii)), is differentiable at $x$ with $f'(x)=\exp(x)$, and $\exp(x)>0$ by Basic Properties of the Exponential Function (iii), so $f'(x)\neq0$. By Inverse of a Continuous Strictly Increasing Function on an Interval: Continuity and Derivative (v), $g=\log$ is differentiable at $f(x)=t$ and

$$\log'(t)=\frac{1}{f'(x)}=\frac{1}{\exp(\log(t))}=\frac{1}{t},$$

the last step by $(\mathrm{V})$.

Now let $I\subseteq(0,\infty)$ be an interval containing two distinct points, and let $t\in I$. By Restriction Stability of Continuity and of the Derivative (ii), applied to the intervals $I\subseteq(0,\infty)$, the map $\log:(0,\infty)\to\mathbb{R}$ and the point $t$, the restriction $\log|_{I}$ is differentiable at $t$ and $(\log|_{I})'(t)=\log'(t)=1/t$. As $t\in I$ was arbitrary, $\log|_{I}$ is differentiable on $I$, that is, differentiable, by Derivative of a Real Function on an Interval (iii).

Proof of (vii). Let $t\in(0,\infty)$. By Basic Properties of the Exponential Function (v) with $u=\log(t)$ and by $(\mathrm{V})$, $t=\exp(\log(t))\ge1+\log(t)$, hence $\log(t)\le t-1$.