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

## 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}$.

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