ThmDex – An index of mathematical definitions, results, and conjectures.
Result R2589 on D6: Natural number factorial function
Trivial factorial upper bound
Formulation 0
Let $!$ be the D6: Natural number factorial function.
Let $n \in \mathbb{N}$ be a D996: Natural number.
Then
(1) \begin{equation} n ! \leq n^n \end{equation}
(2) \begin{equation} n! = n^n \quad \iff \quad n \in \{ 0, 1 \} \end{equation}
Subresults
▶ R4898
Proofs
Proof 0
Let $!$ be the D6: Natural number factorial function.
Let $n \in \mathbb{N}$ be a D996: Natural number.