Let $m$ and $n$ be positive integers. I am trying to prove that if $m \log m >0.53n$, then
$$m>\frac{0.53n}{\log 0.53n},$$
where $m$ is not necessarily bigger than $n$.
My attempt: First recall the Lambert function denoted by $W(x)$ which is the inverse fonction of $xe^x$, i.e., $W(xe^x)=x$, $W$ is increasing because $xe^x$ is increasing.
As $ m \log m =\log m e^{\log m} $, by applying $W$ we get $ m>W(0.53n)$.
How to prove such inequality?
Edit question. After seeing the comments It seems that the second inequality is not true for any value of $n$ and $m$. So we have to put some condition on $n$ and $m$.
Here is my second attempt: Assume $n$ is large enough s.t. $\log 0.53 n >1$. Then if $m<0.53n$ then $\log m <\log 0.53n$, hence
$$m \log 0.53n >m \log m>0.53n $$ So we get
$$ m>\frac{0.53n}{\log 0.53n}, $$
If $0.53n<m$ then $m>0.53n>\frac{0.53n}{\log 0.53n} $
The last inequality is true By our assumption on $n$ so we get
$$ m>\frac{0.53n}{\log 0.53n},$$
if $0.53n=m$.
By replacing it in the first inequality we get $n>6$.
So the inequality is true assuming $n>6$ .
Is my second attempt right?
Fact 1. Let $m, n\in \mathbb{Z}_{> 0}$ with $n \ge 4$. If $m\ln m > c n$, then $m > \frac{cn}{\ln(cn)}$ where $c = 0.53$.
Proof.
If $n = 4, 5$, it is easy.
In the following, assume that $n \ge 6$.
We have $\ln(cn) > 1$. Thus, we have $\ln \frac{cn}{\ln(cn)} < \ln (cn)$ and $$\frac{cn}{\ln(cn)}\ln \frac{cn}{\ln(cn)} < cn.$$
Thus, we have $$m\ln m > c n > \frac{cn}{\ln(cn)}\ln \frac{cn}{\ln(cn)}.$$
Since $x \mapsto x\ln x$ is strictly increasing on $x \ge 1$, using $\frac{cn}{\ln(cn)} > 1$, we have $$m > \frac{cn}{\ln(cn)}.$$
We are done.