Equivalence of Definitions of Real Natural Logarithm
Theorem
The following definitions of the concept of Real Natural Logarithm are equivalent:
Definition 1
Let $x \in \R$ be a real number such that $x > 0$.
The (natural) logarithm of $x$ is defined as:
- $\displaystyle \ln x := \int_1^x \frac {\d t} t$
Definition 2
Let $x \in \R$ be a real number such that $x > 0$.
The (natural) logarithm of $x$ is defined as:
- $\ln x := y \in \R: e^y = x$
where $e$ is Euler's number.
Definition 3
Let $x \in \R$ be a real number such that $x > 0$.
The (natural) logarithm of $x$ is defined as:
- $ \displaystyle \ln x := \lim_{n \mathop \to \infty} n \paren {\sqrt [n] x - 1}$
Proof
Definition 1 implies Definition 2
Let $F \left({x}\right)$ be $\displaystyle \int_1^x \frac {\d t} t$.
Let $f \left({t}\right)$ be $\displaystyle \int \frac {\d t} t$.
Then:
- $\dfrac {\d t} t = \dfrac 1 t$
Or:
- $\dfrac {\d x} x = \dfrac 1 x$
Also:
- $F \left({x}\right) = f \left({x}\right) - f \left({1}\right)$
Therefore:
\(\ds \frac {\d F \left({x}\right)} {\d x}\) | \(=\) | \(\ds \frac {\d f \left({x}\right)} {\d x} - \frac {\d F \left({1}\right)} {\d x}\) | ||||||||||||
\(\ds \) | \(=\) | \(\ds \frac {\d f \left({x}\right)} {\d x}\) | Derivative of Constant | |||||||||||
\(\ds \) | \(=\) | \(\ds \frac 1 x\) | ||||||||||||
\(\ds \leadsto \ \ \) | \(\ds \frac {\d x} {\d F \left({x}\right)}\) | \(=\) | \(\ds x\) | Derivative of Inverse Function |
Furthermore:
- $F \left({1}\right) = f \left({1}\right) - f \left({1}\right) = 0$
The result follows from the fifth definition of the exponential function:
- $F \left({x}\right) \equiv e^x$
$\Box$
Definition 2 implies Definition 1
\(\ds e^{F \left({x}\right)}\) | \(=\) | \(\ds x\) | ||||||||||||
\(\ds \leadsto \ \ \) | \(\ds \frac {\d x} {\d F \left({x}\right)}\) | \(=\) | \(\ds x\) | |||||||||||
\(\ds \leadsto \ \ \) | \(\ds \frac {\d F \left({x}\right)} {\d x}\) | \(=\) | \(\ds \frac 1 x\) | Derivative of Inverse Function |
Let $f \left({t}\right)$ be $\displaystyle \int \frac 1 t \rd t$.
Then:
- $F \left({x}\right) = f \left({x}\right) + C$
When $F \left({x}\right) = 0$:
- $x = e^{F \left({x}\right)} = 1$
- $F \left({1}\right) = f \left({1}\right) + C = 0 \implies f \left({1}\right) = - C$
Therefore:
- $F \left({x}\right) = f \left({x}\right) - f \left({1}\right)$
Therefore:
- $\displaystyle F \left({x}\right) = \int_1^x \frac {\d t} t$
$\Box$
Therefore:
\(\ds y = \int_1^x \frac {\d t} t\) | \(\leadsto\) | \(\ds e^y = x\) | Definition 1 implies Definition 2 | |||||||||||
\(\ds e^y = x\) | \(\leadsto\) | \(\ds y = \int_1^x \frac {\d t} t\) | Definition 2 implies Definition 1 | |||||||||||
\(\ds \leadsto \ \ \) | \(\ds y = \int_1^x \frac {\d t} t\) | \(\iff\) | \(\ds e^y = x\) |
$\blacksquare$