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$
