How do I prove $\tan1 < \frac{\pi}{2}$?

Question

Prove that the equation $$\sin x \sin({\sin x}) = \frac{\pi}{2} \cos({\sin x})$$ has no real solutions.

Let $t=\sin x$, $-1\leq t\leq 1$. Then the expression above is equvalent to $t\sin t = \frac{\pi}{2} \cos t$. As the function $f(t)=t\sin t - \frac{\pi}{2} \cos t$ is even, and $t=0$ is not a solution, I have to prove that $f(t)$ has no positive roots ($t>0$). So, for the left side $0<t\leq 1$ and $0<\sin t\leq \sin1$, then $t\sin t\leq \sin1$. For the right side $\cos t\geq \cos1$, so $\frac{\pi}{2} \cos t\geq \frac{\pi}{2} \cos1$. The objective is to prove that $\sin1<\frac{\pi}{2} \cos1$, or, equivalently, $\tan1 < \frac{\pi}{2}$.

I don't know how to approach this inequality. The arguments and the values are mixed up.

Answer 1

We can use the Taylor series and alternating series theorem to say $$\sin 1 \lt 1-\frac 1{3!}+\frac 1{5!}=\frac {101}{120}\\ \cos 1 \gt 1-\frac 1{2!}+\frac 1{4!}-\frac 1{6!}=1-\frac 12+\frac 1{24}-\frac 1{720}=\frac{389}{720}\\ \tan 1=\frac {\sin 1}{\cos 1} \lt \frac {606}{389} \lt 1.56 \lt \frac {\pi}2$$

Answer 2

This is a Community Wiki repost of one of several deleted answers to a deleted question from last year: Compare $\arcsin (1)$ and $\tan (1)$.

[I have taken this opportunity to incorporate a simplification - but only a slight one - I made later in a comment.]

I would be pleased if we were allowed to revisit the other deleted answers, too.

---

One can write: $$ \frac{1}{\sqrt{1 + \tan^21}} = \cos1 = 1 - 2\sin^2\frac{1}{2} > \frac{17639}{32768} > \frac{17632}{32768} = \frac{551}{1024}, $$ because $$ \sin\frac{1}{2} < \frac{1}{2} - \frac{1}{2^3\cdot3!} + \frac{1}{2^5\cdot5!} = \frac{1920 - 80 + 1}{3840} < \frac{1845}{3840} = \frac{123}{256}. $$ On the other hand, using Archimedes's lower bound, $\pi > 3\tfrac{10}{71}$: $$ \frac{1}{\sqrt{1 + \left(\sin^{-1}1\right)^2}} = \frac{1}{\sqrt{1 + \left(\frac{\pi}{2}\right)^2}} < \frac{1}{\sqrt{1 + \left(\frac{223}{142}\right)^2}} = \frac{142}{\sqrt{69893}} < \frac{142}{\sqrt{69696}} = \frac{142}{264} = \frac{71}{132}. $$ So, one can prove that $\tan1 < \sin^{-1}1$ by proving that: $$ \frac{551}{1024} > \frac{71}{132}, $$ which simplifies to $33 \times 551 > 71 \times 256$, that is, $18183 > 18176$ - which is true.