ThmDex – An index of mathematical definitions, results, and conjectures.
Characterisation of natural real exponential function by a differential equation
Formulation 0
Let $f : \mathbb{R} \to (0, \infty)$ be a D5614: Differentiable real function.
Let $\exp : \mathbb{R} \to (0, \infty)$ be the D1932: Standard natural real exponential function.
Let $a \in \mathbb{R}$ be a D993: Real number.
Then $f = a \exp$ if and only if
(1) $\forall \, x \in \mathbb{R}: f'(x) = f(x)$
(2) $f(0) = a$
Proofs
Proof 0
Let $f : \mathbb{R} \to (0, \infty)$ be a D5614: Differentiable real function.
Let $\exp : \mathbb{R} \to (0, \infty)$ be the D1932: Standard natural real exponential function.
Let $a \in \mathbb{R}$ be a D993: Real number.
If $f = a \exp$, then from the results
(i) R5254: Slope function for standard natural real exponential function
(ii) R4285: Standard natural real exponential function maps zero to one

we know that conditions (1) and (2) hold.

Conversely, assume that the conditions (1) and (2) hold. Using the results
(i) R5255: Slope function for pointwise product of two differentiable real functions
(ii) R5256: Slope function for composition of two differentiable real functions

and the assumption $f' = f$, we have \begin{equation} \frac{d}{d x} f(x) \exp(- x) = f'(x) \exp(- x) - f(x) \exp(- x) = f'(x) \exp(- x) - f'(x) \exp(- x) = 0 \end{equation} for every $x \in \mathbb{R}$. That is, the function \begin{equation} x \mapsto f(x) \exp(- x) = \frac{f(x)}{\exp(x)} \end{equation} is constant everywhere on $\mathbb{R}$. Since $f(0) = a$, then $f(0) \exp(-0) = a \exp(0) = a$. That is, $f(x) \exp(-x) = a$ and equivalently $f(x) = a \exp(x)$ for every $x \in \mathbb{R}$. $\square$