# Equivalence of Definitions of Real Exponential Function/Inverse of Natural Logarithm equivalent to Differential Equation

## Contents

## Theorem

The following definitions of the concept of **real exponential function** are equivalent:

### As the Inverse of the Natural Logarithm

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

From Logarithm is Strictly Increasing:

- $\ln x$ is strictly increasing.

From Inverse of Strictly Monotone Function:

- 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 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:

\(\displaystyle x\) | \(=\) | \(\displaystyle \ln y\) | |||||||||||

\(\displaystyle \) | \(=\) | \(\displaystyle \int_{t \mathop = 1}^{t \mathop = y} \frac 1 t \rd t\) | Definition 1 of Natural Logarithm | ||||||||||

\(\displaystyle \leadsto \ \ \) | \(\displaystyle \map {D_y} x\) | \(=\) | \(\displaystyle D_y \int_{t \mathop = 1}^{t \mathop = y} \frac 1 t \rd t\) | Differentiation with respect to $y$ | |||||||||

\(\displaystyle \frac {\d x} {\d y}\) | \(=\) | \(\displaystyle \frac 1 y\) | Fundamental Theorem of Calculus | ||||||||||

\(\displaystyle \iff \ \ \) | \(\displaystyle \frac {\d y} {\d x}\) | \(=\) | \(\displaystyle y\) | Derivative of Inverse Function |

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

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

\(\displaystyle \map f 0\) | \(=\) | \(\displaystyle 1\) | |||||||||||

\(\displaystyle \iff \ \ \) | \(\displaystyle \map {f^{-1} } 1\) | \(=\) | \(\displaystyle 0\) | Image of Element under Inverse Mapping | |||||||||

\(\displaystyle \bigintlimits {\ln y} {y \mathop = 1} {}\) | \(=\) | \(\displaystyle \int_{t \mathop = 1}^{t \mathop = 1} \frac 1 t \rd t\) | |||||||||||

\(\displaystyle \) | \(=\) | \(\displaystyle 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:

\(\displaystyle \frac {\d y} {\d x}\) | \(=\) | \(\displaystyle y\) | |||||||||||

\(\displaystyle \leadsto \ \ \) | \(\displaystyle \frac {\d x} {\d y}\) | \(=\) | \(\displaystyle \frac 1 y\) | Derivative of Inverse Function | |||||||||

\(\displaystyle \leadsto \ \ \) | \(\displaystyle \int \rd x\) | \(=\) | \(\displaystyle \int \frac 1 y \rd y\) | Separation of Variables | |||||||||

\(\displaystyle \leadsto \ \ \) | \(\displaystyle x + C\) | \(=\) | \(\displaystyle \int_{t \mathop = 1}^{t \mathop = y} \frac 1 t \rd t\) | Fundamental Theorem of Calculus | |||||||||

\(\displaystyle \) | \(=\) | \(\displaystyle \ln y\) | Definition 1 of Natural Logarithm |

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

\(\displaystyle 0 + C\) | \(=\) | \(\displaystyle \int_{t \mathop = 1}^{t \mathop = 1}\frac 1 t \rd t\) | |||||||||||

\(\displaystyle \leadsto \ \ \) | \(\displaystyle C\) | \(=\) | \(\displaystyle 0\) | Integral on Zero Interval |

That is:

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

$\blacksquare$