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:

$\ds \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:

$\ds \ln x := \lim_{n \mathop \to \infty} n \paren {\sqrt [n] x - 1}$

Proof

Definition 1 implies Definition 2

Let $\map F x$ be $\ds \int_1^x \frac {\d t} t$.

Let $\map f t$ be $\ds \int \frac {\d t} t$.

Then:

$\dfrac {\d t} t = \dfrac 1 t$

Or:

$\dfrac {\d x} x = \dfrac 1 x$

Also:

$\map F x = \map f x - \map f 1$

Therefore:

 $\ds \frac {\d \map F x} {\d x}$ $=$ $\ds \frac {\d \map f x} {\d x} - \frac {\d \map F 1} {\d x}$ $\ds$ $=$ $\ds \frac {\d \map f x} {\d x}$ Derivative of Constant $\ds$ $=$ $\ds \frac 1 x$ $\ds \leadsto \ \$ $\ds \frac {\d x} {\d \map F x}$ $=$ $\ds x$ Derivative of Inverse Function

Furthermore:

$\map F 1 = \map f 1 - \map f 1 = 0$

The result follows from the fifth definition of the exponential function:

$\map F x \equiv e^x$

$\Box$

Definition 2 implies Definition 1

 $\ds e^{\map F x}$ $=$ $\ds x$ $\ds \leadsto \ \$ $\ds \frac {\d x} {\d \map F x}$ $=$ $\ds x$ $\ds \leadsto \ \$ $\ds \frac {\d \map F x} {\d x}$ $=$ $\ds \frac 1 x$ Derivative of Inverse Function

Let $\map f t$ be $\ds \int \frac 1 t \rd t$.

Then:

$\map F x = \map f x + C$

When $\map F x = 0$:

$x = e^{\map F x} = 1$
$\map F 1 = \map f 1 + C = 0 \implies \map f 1 = - C$

Therefore:

$\map F x = \map f x - \map f 1$

Therefore:

$\ds \map F x = \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$