# Equivalence of Definitions of Real Exponential Function

## Theorem

The following definitions of the concept of Real Exponential Function are equivalent:

### As a Power Series Expansion

The exponential function can be defined as a power series:

$\exp x := \ds \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$

### As a Limit of a Sequence

The exponential function can be defined as the following limit of a sequence:

$\exp x := \ds \lim_{n \mathop \to +\infty} \paren {1 + \frac x n}^n$

### As an Extension of the Rational Exponential

Let $e$ denote Euler's number.

Let $f: \Q \to \R$ denote the real-valued function defined as:

$\map f x = e^x$

That is, let $\map f x$ denote $e$ to the power of $x$, for rational $x$.

Then $\exp : \R \to \R$ is defined to be the unique continuous extension of $f$ to $\R$.

$\map \exp x$ is called the exponential of $x$.

### As the Inverse of the Natural Logarithm

Consider the natural logarithm $\ln x$, which is defined on the open interval $\openint 0 {+\infty}$.

$\ln x$ is strictly increasing.
the inverse of $\ln x$ always exists.

The inverse of the natural logarithm function is called the exponential function, which is denoted as $\exp$.

Thus for $x \in \R$, we have:

$y = \exp x \iff x = \ln y$

### As the Solution of a Differential Equation

The exponential function can be defined as the unique solution $y = \map f x$ to the first order ODE:

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

satisfying the initial condition $\map f 0 = 1$.

## Proof

### Inverse of Natural Logarithm implies Limit of Sequence

Let $\exp x$ be the real function defined as the inverse of the natural logarithm:

$y = \exp x \iff x = \ln y$

Let $\left \langle {x_n} \right \rangle$ be the sequence in $\R$ defined as:

$x_n = \paren {1 + \dfrac x n}^n$

First it needs to be noted that $\sequence {x_n}$ does indeed converge to a limit.

$\ds \lim_{n \mathop \to \infty} \paren {1 + \dfrac x n}^n = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$

From Series of Power over Factorial Converges, the right hand side is indeed shown to converge to a limit.

It will next be shown that:

$\ds \map \ln {\lim_{n \mathop \to \infty} \sequence {x_n} } = x$

We have:

 $\ds \map \ln {\paren {1 + \frac x n}^n}$ $=$ $\ds n \, \map \ln {1 + x n^{-1} }$ Logarithms of Powers $\ds$ $=$ $\ds x \frac {\map \ln {1 + x n^{-1} } } {x n^{-1} }$ multiplying by $1 = \dfrac {x n^{-1} } {x n^{-1} }$

From Limit of Sequence is Limit of Real Function, we can consider the differentiable analogue of the sequence.

From Derivative of Logarithm at One we have:

$\ds \lim_{x \mathop \to 0} \frac {\map \ln {1 + x} } x = 1$

But $x n^{-1} \to 0$ as $n \to \infty$ from Sequence of Powers of Reciprocals is Null Sequence.

Thus:

$\ds x \frac {\map \ln {1 + x n^{-1} } } {x n^{-1} } \to x$

as $n \to \infty$.

$\paren {1 + \dfrac x n}^n = \exp \paren {n \map \ln {1 + \dfrac x n} } \to \exp x = e^x$

as $n \to \infty$.

$\blacksquare$

### Limit of Sequence implies Power Series Expansion

Let $\exp x$ be the real function defined as the limit of the sequence:

$\exp x := \ds \lim_{n \mathop \to \infty} \paren {1 + \frac x n}^n$

From the General Binomial Theorem:

 $\ds \paren {1 + \frac x n}^n$ $=$ $\ds 1 + x + \frac {n \paren {n - 1} x^2} {2! \ n^2} + \frac {n \paren {n - 1} \paren {n - 2} x^3} {3! \ n^3} + \cdots$ $\ds$ $=$ $\ds \frac {x^0} {0!} + \frac {x^1} {1!} + \paren {\frac {n - 1} n} \frac {x^2} {2!} + \paren {\frac {\paren {n - 1} \paren {n - 2} } {n^2} } \frac {x^3} {3!} + \cdots$ $\ds \leadsto \ \$ $\ds 0$ $=$ $\ds \paren {1 + \frac x n}^n - \paren {\frac {x^0} {0!} + \frac {x^1} {1!} + \paren {\frac {n - 1} n} \frac {x^2} {2!} + \paren {\frac {\paren {n - 1} \paren {n - 2} } {n^2} } \frac {x^3} {3!} + \cdots}$

From Power over Factorial, this converges to:

$\exp x - \paren {\dfrac {x^0} {0!} + \dfrac {x^1} {1!} + \dfrac {x^2} {2!} + \dfrac {x^3} {3!} + \cdots} = 0$

as $n \to +\infty$.

 $\ds \leadsto \ \$ $\ds \exp x$ $=$ $\ds \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$

$\blacksquare$

### Limit of Sequence implies Extension of Rational Exponential

Let the restriction of the exponential function to the rationals be defined as:

$\ds \exp \restriction_\Q: x \mapsto \lim_{n \mathop \to +\infty}\left ({1 + \frac x n}\right)^n$

Thus, let $e$ be Euler's Number defined as:

$e = \ds \lim_{n \mathop \to +\infty}\left ({1 + \frac 1 n}\right)^n$

For $x = 0$:

 $\ds \exp \restriction_\Q \paren 0$ $=$ $\ds \lim_{n \mathop \to +\infty} \paren {1 + \frac 0 n}^n$ $\ds$ $=$ $\ds 1$ $\ds$ $=$ $\ds e^0$

For $x \ne 0$:

 $\ds \exp \restriction_\Q \paren x$ $=$ $\ds \lim_{n \mathop \to +\infty}\paren {1 + \frac x n}^n$ $\ds$ $=$ $\ds \lim_{\paren {n/x} \mathop \to +\infty}\paren {\paren {1 + \frac 1 {\paren {n/x} } }^{\paren {n/x} } }^x$ Exponent Combination Laws $\ds$ $=$ $\ds e^x$

where the continuity in the last step follows a fortiori from Power Function to Rational Power permits Unique Continuous Extension.

For $x \in \R \setminus \Q$, we invoke Power Function to Rational Power permits Unique Continuous Extension.

$\blacksquare$

### Extension of Rational Exponential implies Solution of Differential Equation

Let $\exp x$ be the real function defined as the extension of rational exponential.

Then we have:

 $\ds \map {D_x} {\exp x}$ $=$ $\ds \lim_{h \mathop \to 0} \frac {\map \exp {x + h} - \exp x} h$ Definition of Derivative $\ds$ $=$ $\ds \lim_{h \mathop \to 0} \frac {\exp x \cdot \exp h - \exp x} h$ Exponential of Sum $\ds$ $=$ $\ds \lim_{h \mathop \to 0} \frac {\exp x \paren {\exp h - 1} } h$ $\ds$ $=$ $\ds \exp x \paren {\lim_{h \mathop \to 0} \frac {\exp h - 1} h}$ Multiple Rule for Limits of Real Functions, as $\exp x$ is constant $\ds$ $=$ $\ds \exp x$ Derivative of Exponential at Zero: Proof 2

The application of Derivative of Exponential at Zero is not circular as the referenced proof does not depend on $D_x \exp x = \exp x$.

$\Box$

 $\ds \exp 0$ $=$ $\ds \lim_{n \mathop \to +\infty} \paren {1 + \frac 0 n}^n$ $\ds$ $=$ $\ds 1$

$\blacksquare$

### Power Series Expansion equivalent to Solution of Differential Equation

#### Power Series Expansion implies Solution of Differential Equation

Let $\exp x$ be the real function defined as the sum of the power series:

$\exp x := \ds \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$

Let $y = \ds \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$.

Then:

 $\ds \dfrac {\d y} {\d x}$ $=$ $\ds \dfrac \d {\d x} \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$ $\ds$ $=$ $\ds \map {\dfrac \d {\d x} } {\frac {x^0} {0!} + \sum_{n \mathop = 1}^\infty \frac {x^n} {n!} }$ extracting the zeroth term $\ds$ $=$ $\ds 0 + \sum_{n \mathop = 1}^\infty \frac {n x^{n - 1} } {n!}$ Power Rule for Derivatives and Derivative of Constant $\ds$ $=$ $\ds \sum_{n \mathop = 1}^\infty \frac {x^{n - 1} } {\paren {n - 1}!}$ simplifying $\ds$ $=$ $\ds \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$ Translation of Index Variable of Summation $\ds$ $=$ $\ds y$

Setting $x = 0$ we find:

 $\ds \map y 0$ $=$ $\ds \sum_{n \mathop = 0}^\infty \frac {0^n} {n!}$ $\ds$ $=$ $\ds \frac {0^0} {0!} + \sum_{n \mathop = 1}^\infty \frac {0^n} {n!}$ $\ds$ $=$ $\ds \frac {0^0} {0!}$ as $0^n = 0$ for all $n > 0$ $\ds$ $=$ $\ds 1$ Definition of $0^0$

$\blacksquare$

That is:

$\exp x$ is the particular solution of the differential equation:

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

satisfying the initial condition $\map f 0 = 1$.

$\Box$

#### Solution of Differential Equation implies Power Series Expansion

Let $\exp x$ be the real function defined as the particular solution of the differential equation:

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

satisfying the initial condition $\map f 0 = 1$.

From Higher Derivatives of Exponential Function, we have:

$\forall n \in \N: \map {f^{\paren n} } {\exp x} = \exp x$

Since $\exp 0 = 1$, the Taylor series expansion for $\exp x$ about $0$ is given by:

$\ds \exp x = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$

From Radius of Convergence of Power Series over Factorial, we know that this power series expansion converges for all $x \in \R$.

From Taylor's Theorem, we know that

$\ds \exp x = 1 + \frac x {1!} + \frac {x^2} {2!} + \cdots + \frac {x^{n - 1} } {\paren {n - 1}!} + \frac {x^n} {n!} \map \exp \eta$

where $0 \le \eta \le x$.

Hence:

 $\ds \size {\exp x - \paren {1 + \frac x {1!} + \frac {x^2} {2!} + \cdots + \frac {x^{n - 1} } {\paren {n - 1}!} } }$ $=$ $\ds \size {\frac {x^n} {n!} \map \exp \eta}$ $\ds$ $\le$ $\ds \frac {\size {x^n} } {n!} \map \exp {\size x}$ Exponential is Strictly Increasing $\ds$ $\to$ $\ds 0$ $\ds \text { as } n \to \infty$ Series of Power over Factorial Converges

So the partial sums of the power series converge to $\exp x$.

The result follows.

$\blacksquare$

### Inverse of Natural Logarithm equivalent to Solution of Differential Equation

#### Inverse of Natural Logarithm implies Solution of Differential Equation

Let $\exp x$ be the real function defined as the inverse of the natural logarithm:

$y = \exp x \iff x = \ln y$

Then:

 $\ds x$ $=$ $\ds \ln y$ $\ds$ $=$ $\ds \int_{t \mathop = 1}^{t \mathop = y} \frac 1 t \rd t$ Definition 1 of Natural Logarithm $\ds \leadsto \ \$ $\ds \map {D_y} x$ $=$ $\ds D_y \int_{t \mathop = 1}^{t \mathop = y} \frac 1 t \rd t$ Differentiation with respect to $y$ $\ds \frac {\d x} {\d y}$ $=$ $\ds \frac 1 y$ Fundamental Theorem of Calculus $\ds \leadstoandfrom \ \$ $\ds \frac {\d y} {\d x}$ $=$ $\ds y$ Derivative of Inverse Function

This proves that $y$ is a solution of the differential equation.

It remains to be proven that $y$ fulfills the initial condition:

 $\ds \map f 0$ $=$ $\ds 1$ $\ds \leadstoandfrom \ \$ $\ds \map {f^{-1} } 1$ $=$ $\ds 0$ Image of Element under Inverse Mapping $\ds \bigintlimits {\ln y} {y \mathop = 1} {}$ $=$ $\ds \int_{t \mathop = 1}^{t \mathop = 1} \frac 1 t \rd t$ $\ds$ $=$ $\ds 0$ Integral on Zero Interval

That is:

$\exp x$ is the particular solution of the differential equation:

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

satisfying the initial condition $\map f 0 = 1$.

$\Box$

#### Solution of Differential Equation implies Inverse of Natural Logarithm

Let $\exp x$ be the real function defined as the particular solution of the differential equation:

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

satisfying the initial condition $\map f = 1$.

Thus:

 $\ds \frac {\d y} {\d x}$ $=$ $\ds y$ $\ds \leadsto \ \$ $\ds \frac {\d x} {\d y}$ $=$ $\ds \frac 1 y$ Derivative of Inverse Function $\ds \leadsto \ \$ $\ds \int \rd x$ $=$ $\ds \int \frac 1 y \rd y$ Separation of Variables $\ds \leadsto \ \$ $\ds x + C$ $=$ $\ds \int_{t \mathop = 1}^{t \mathop = y} \frac 1 t \rd t$ Fundamental Theorem of Calculus $\ds$ $=$ $\ds \ln y$ Definition 1 of Natural Logarithm

To solve for $C$, put $\tuple {x_0, y_0} = \tuple {0, 1}$:

 $\ds 0 + C$ $=$ $\ds \int_{t \mathop = 1}^{t \mathop = 1}\frac 1 t \rd t$ $\ds \leadsto \ \$ $\ds C$ $=$ $\ds 0$ Integral on Zero Interval

That is:

$y = \exp x \iff x = \ln y$

$\blacksquare$