ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation 0
Let $!$ be the D6: Natural number factorial function.
Let $n \in 1, 2, 3, \ldots$ be a D5094: Positive integer.
Then \begin{equation} n \log n - n < \log (n !) \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.
From result R4900: , we have \begin{equation} \exp(n) > \frac{n^n}{n!} \end{equation} Taking logarithms of each side leads to \begin{equation} n > n \log n - \log n! \end{equation} Rearranging, this gives \begin{equation} \log n! > n \log n - n \end{equation} which is what was desired. $\square$