ThmDex – An index of mathematical definitions, results, and conjectures.

Result R4900 on D1932: Standard natural real exponential function

Formulation 0

Let $\exp$ be the D1932: Standard natural real exponential function.
Let $!$ be the D6: Natural number factorial function.
Let $n \in \mathbb{N}$ be a D996: Natural number.

Then

(1)	\begin{equation} \exp (n) \geq \frac{n^n}{n!} \end{equation}
(2)	\begin{equation} \exp (n) = \frac{n^n}{n!} \quad \iff \quad n = 0 \end{equation}

Proofs

Proof 0

Let $\exp$ be the D1932: Standard natural real exponential function.
Let $!$ be the D6: Natural number factorial function.
Let $n \in \mathbb{N}$ be a D996: Natural number.

Proceeding directly from the definitions, we have \begin{equation} \exp(n) = \sum_{m = 0}^{\infty} \frac{n^m}{m!} \geq \frac{n^n}{n!} \end{equation} The second claim is immediate. $\square$