Prove that $12(a\sin a+\cos a-1)^2\le 2a^4+a^3\sin(2a)$,$\forall a\in (0,\infty)$

Question

Prove that $$12(a\sin a+\cos a-1)^2\le 2a^4+a^3\sin2a,\forall a\in (0,\infty).$$
The solution in the book where I found this goes like this : from CS for integrals we have that $$\left(\int_0^a x\cos x dx\right)^2\le \left(\int_0^a x^2 dx \right)\left(\int_0^a \cos^2 x dx \right)\iff \left(x\sin x \bigg |_0^a -\int_0^a \sin x dx\right)^2 \le$$ $$\le \frac{a^3}{3}\int_0^a\frac{1+\cos 2x}{2}dx \iff (a\sin a+\cos a-1)^2\le \frac{a^3}{6} \cdot \left(x \bigg|_0^a + \frac{1}{2}\sin 2x\bigg|_0^a\right) \iff $$ $$\iff 6(a\sin a+ \cos a -1)^2\le a^3\left(a+\frac{\sin 2a}{2}\right)$$$$\iff 12(a\sin a+\cos a-1)^2\le 2a^4+a^3\sin2a,\forall a\in (0,\infty).$$
I can understand why this works, but I can't understand how you are supposed to come up with such an idea. I have never seen a proof like this before (i.e. using an integral inequality to prove an inequality that appears not to be related with integrals) and I haven't been able to prove this inequality in any other way. What I tried was to consider the function $f:(0,\infty)\to \mathbb{R}$,$f(a)=12(a\sin a+\cos a-1)^2-2a^4-a^3\sin2a$, and then I attempted to study its extrema, but this didn't work out due to the fact that $f'(a)$ has an ugly form and I couldn't solve $f'(a)=0$.
To sum up, I would like to know how someone can think of this proof and I am also curious if there is some other way to prove this inequality.

Answer 1

Problem: Prove that $f(a) = 2a^4+a^3\sin 2a - 12(a\sin a + \cos a-1)^2\ge 0$ for $a \ge 0$.

Proof: Note that $f(0) = 0$. It suffices to prove that $$f'(a) = a\left[(2\cos 2a + 8)a^2-18a \sin a\cos a - 24\cos^2 a+24\cos a\right] \ge 0, \ a \ge 0.$$ It suffices to prove that $$g(a)=(2\cos 2a + 8)a^2-18a \sin a\cos a - 24\cos^2 a+24\cos a \ge 0, \ a\ge 0.$$

Denote $c = \cos a$ and $s = \sin a$. We rewrite $g(a)$ as $$g(a) = (4c^2+6)\Big(a-\frac{9sc}{4c^2+6}\Big)^2 - \frac{81s^2c^2}{4c^2+6} - 24c^2+24c.$$

(1) If $0\le a \le \frac{19}{10}$, since $a \ge \sin a$, $4c^2+6 \ge 2\sqrt{4\cdot 6}\, c \ge 9c$ and $a-\frac{9sc}{4c^2+6} \ge \sin a - \frac{9sc}{4c^2+6} \ge 0$, it suffices to prove that $$(4c^2+6)\Big(s -\frac{9sc}{4c^2+6}\Big)^2- \frac{81s^2c^2}{4c^2+6} - 24c^2+24c\ge 0$$ or $$2(1-c)(2c^3-7c^2+6c+3) \ge 0.$$ Since $0\le c\le 1$, we have $2c^3-7c^2+6c+3 = c(2c^2-7c+7)+(3-c)\ge 0$. The inequality is true.

(2) If $a > \frac{19}{10}$, since $a-\frac{9sc}{4c^2+6} \ge \frac{23}{10}$ (see Remark at the end), it suffices to prove that $$(4c^2+6)\Big(\frac{23}{10}\Big)^2- \frac{81s^2c^2}{4c^2+6} - 24c^2+24c\ge 0$$ or $$\frac{c^2(1741c^2+2400c+1723)+(3600c+4761 - 1000c^2)}{25(4c^2+6)}\ge 0.$$ Since $-1\le c\le 1$, clearly the inequality is true. This completes the proof.

Remark (proof of $a-\frac{9sc}{4c^2+6} \ge \frac{23}{10}$ for $a > \frac{19}{10}$): Let $h(a) = a-\frac{9sc}{4c^2+6} - \frac{23}{10}$. Since $h(\frac{19}{10})>0$, it suffices to prove that $h'(a) \ge 0$ for $a > \frac{19}{10}$. It suffices to prove that $8c^4-48c^2+45 = 8(3-c^2)^2-27\ge 0$ for $-1\le c\le 1$. Clearly, This inequality is true.