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