An inequality in Lemma 4.3 of "PRIMES is in P" by AKS I'm having trouble verifying the following inequality in Lemma 4.3 in the paper PRIMES is in P.

\begin{align}
&amp;n^{\lfloor\log{\lceil\log^5n\rceil}\rfloor+\frac{1}{2}(\log^4(n)+\log^2(n))} &lt; n^{\log^4(n)}\\ 
&amp;\text{where }n&gt;2\text{ and }n \in\mathbb{N}
\end{align} 

The same inequality is dealt with differently in the older Annals of Mathematics version, but it contains a mistake as pointed out here, which is corrected in the newer version that is cited above.

I have used a graphing software to verify the inequality but am unsure as to how to proceed.

Thanking you in advance!

Edit: the base of the logarithm is $2$.
Since $f(x) = n^x$ is a strictly increasing function for positive $x$, or you can see this by taking logarithms of both sides, the equality you want to prove is equivalent to

$$\lfloor\log{\lceil\log^5n\rceil}\rfloor+\frac{1}{2}(\log^4(n)+\log^2(n)) \lt \log^4(n) \tag{1}\label{eq1A}$$

Note that, as stated in the linked paper in section $3$, "Notation and Preliminaries",


  We use log for base $2$ logarithm, and ln for natural logarithm.


One way to show \eqref{eq1A} holds is to break the inequality into $2$ parts. First, consider

$$\frac{1}{2}\left(\log^2(n)\right) \lt \frac{1}{6}\left(\log^4(n)\right) \iff 3 \lt \log^2(n) \tag{2}\label{eq2A}$$

This is satisfied for $n = 4$, and all larger values since $\log(n)$ is a strictly increasing function for positive $n$.

Next, have

$$y = \log^4(n) \tag{3}\label{eq3A}$$

so $y = 16$ for $n = 4$, and

$$\begin{equation}\begin{aligned}
\lfloor\log{\lceil\log^5n\rceil}\rfloor &amp; \lt \frac{1}{3}\left(\log^4(n)\right) \\
\lfloor\log{\lceil y^{\frac{5}{4}}\rceil}\rfloor &amp; \lt \frac{y}{3}
\end{aligned}\end{equation}\tag{4}\label{eq4A}$$

Consider

$$y^{\frac{5}{4}} + 1 \lt y^{\frac{4}{3}} \tag{5}\label{eq5A}$$

This is true for $y = 16$ and, since $f_1(y) = y^{\frac{4}{3}}$ is a faster growing function than $f_2(y) = y^{\frac{5}{4}}$, \eqref{eq5A} is true for all $y \ge 16$. Next, consider

$$\begin{equation}\begin{aligned}
\lfloor\log{\lceil y^{\frac{5}{4}}\rceil}\rfloor &amp; \lt \lfloor\log(y^{\frac{5}{4}} + 1)\rfloor \\
&amp; \lt \lfloor\log(y^{\frac{4}{3}})\rfloor \\
&amp; \le \frac{4}{3}(\log(y))
\end{aligned}\end{equation}\tag{6}\label{eq6A}$$

As such, you can prove that \eqref{eq5A} is to have the RHS of \eqref{eq6A} be less than or equal to the RHS of \eqref{eq5A}, i.e.,

$$\frac{4}{3}(\log(y)) \leq \frac{y}{3} \iff 4\log(y) \leq y \tag{7}\label{eq7A}$$

For $y = 16$, the $2$ sides of \eqref{eq7A} are equal. Since, for $y \ge 16$, $f_3(y) = y - 4\log(y) \implies f'_3(y) = 1 - \frac{1}{\ln(2)y} \gt 0$, this shows \eqref{eq4A} is true for all $y \ge 16$.

Finally, using \eqref{eq2A} and \eqref{eq4A} in the LHS of \eqref{eq1A} shows it's less than the RHS, so \eqref{eq1A} will be true for all $n \ge 4$. Since you're considering $n \gt 2$ and $n \in \mathbb{N}$, this just leaves $n = 3$ to check, either through your graph or just doing it manually.
Since $f(x) = n^x$ is a strictly increasing function for positive $x$, or you can see this by taking logarithms of both sides, the equality you want to prove is equivalent to

$$\lfloor\log{\lceil\log^5n\rceil}\rfloor+\frac{1}{2}(\log^4(n)+\log^2(n)) \lt \log^4(n) \tag{1}\label{eq1A}$$

Note that, as stated in the linked paper in section $3$, "Notation and Preliminaries",


  We use log for base $2$ logarithm, and ln for natural logarithm.


One way to show \eqref{eq1A} holds is to break the inequality into $2$ parts. First, consider

$$\frac{1}{2}\left(\log^2(n)\right) \lt \frac{1}{6}\left(\log^4(n)\right) \iff 3 \lt \log^2(n) \tag{2}\label{eq2A}$$

This is satisfied for $n = 4$, and all larger values since $\log(n)$ is a strictly increasing function for positive $n$.

Next, have

$$y = \log^4(n) \tag{3}\label{eq3A}$$

so $y = 16$ for $n = 4$, and

$$\begin{equation}\begin{aligned}
\lfloor\log{\lceil\log^5n\rceil}\rfloor &amp; \lt \frac{1}{3}\left(\log^4(n)\right) \\
\lfloor\log{\lceil y^{\frac{5}{4}}\rceil}\rfloor &amp; \lt \frac{y}{3}
\end{aligned}\end{equation}\tag{4}\label{eq4A}$$

Consider

$$y^{\frac{5}{4}} + 1 \lt y^{\frac{4}{3}} \tag{5}\label{eq5A}$$

This is true for $y = 16$ and, since $f_1(y) = y^{\frac{4}{3}}$ is a faster growing function than $f_2(y) = y^{\frac{5}{4}}$, \eqref{eq5A} is true for all $y \ge 16$. Next, consider

$$\begin{equation}\begin{aligned}
\lfloor\log{\lceil y^{\frac{5}{4}}\rceil}\rfloor &amp; \lt \lfloor\log(y^{\frac{5}{4}} + 1)\rfloor \\
&amp; \lt \lfloor\log(y^{\frac{4}{3}})\rfloor \\
&amp; \le \frac{4}{3}(\log(y))
\end{aligned}\end{equation}\tag{6}\label{eq6A}$$

As such, you can prove that \eqref{eq5A} is to have the RHS of \eqref{eq6A} be less than or equal to the RHS of \eqref{eq5A}, i.e.,

$$\frac{4}{3}(\log(y)) \leq \frac{y}{3} \iff 4\log(y) \leq y \tag{7}\label{eq7A}$$

For $y = 16$, the $2$ sides of \eqref{eq7A} are equal. Since, for $y \ge 16$, $f_3(y) = y - 4\log(y) \implies f'_3(y) = 1 - \frac{1}{\ln(2)y} \gt 0$, this shows \eqref{eq4A} is true for all $y \ge 16$.

Finally, using \eqref{eq2A} and \eqref{eq4A} in the LHS of \eqref{eq1A} shows it's less than the RHS, so \eqref{eq1A} will be true for all $n \ge 4$. Since you're considering $n \gt 2$ and $n \in \mathbb{N}$, this just leaves $n = 3$ to check, either through your graph or just doing it manually.