This result is a consequence of the results

(i)	R2589: Trivial factorial upper bound
(ii)	R3612: Standard natural basic real logarithm function is strictly isotone

$\square$