<s>[INST] A real analysis proof question (related to sin(1/x)) The problem statement is 

Let 
  $$f(x) = \left\{\begin{array}{cc} 
x^4 \left(2 + \sin \frac 1 x\right) & x \ne 0 \\
0 & x = 0
\end{array}\right.
$$
(a)Prove that $f$ is differentiable on $\mathbb{R}$
(b)Prove that $f$ has an absolute minimum at $x=0$
(c) Prove that $f'$ takes both positive and negative values in every neighborhood of $0$.

This first two parts of the problem are pretty straightforward. The only problem I encountered was in the last part. I was not sure how to prove it. I know both $\sin(1/x)$ and $\cos(1/x)$oscillate near zero. For any interval around zero they are gonna take positive and negative values since they oscillates. But this was not consider as a "proof". Is there a way to do that more rigorously? Can I use intermediate value property?
BTW, $$f'(x) = 4x^3\left(2+\sin \frac 1 x\right)+x^2\cos \left(\frac 1 x\right)$$ when $x\neq 0$.
 [/INST] Since away from $0$ we have
$$f(x) = x^4\left(2 + \sin \frac 1 x\right)$$
we have
\begin{align*}
f'(x) &= 4x^3 \left(2 + \sin \frac 1 x\right) + x^4 \left(\cos \frac 1 x\right) \left(-\frac 1 {x^2}\right) \\
&= 8x^3 + 4x^3 \sin \frac 1 x - x^2 \cos \frac 1 x \\
&= x^2 \left(8x + 4x \sin \frac 1 x - \cos \frac 1 x\right)
\end{align*}
(Note there's a sign error in the original post, but it doesn't actually matter). Now notice that the terms with $x$ tend to zero at the origin while the cosine term does not: The cosine term is dominant here. To be explicit, choose $x = 1 / (n \pi)$ with $n > 8$. The first two terms can be controlled as
$$\left|8x + 4x \sin \frac 1 x\right| \le 12 |x| < \frac 1 2$$
On the other hand, $\cos 1/x = \cos (n\pi) = \pm 1$ according to the parity of $n$. Hence, the derivative can be estimated either as
$$f'(x) > \frac 1 {(n\pi)^2} \cdot \left(1 - \frac 1 2\right) = \frac 1 {2 (n \pi)^2}$$
if $n$ is odd or
$$f'(x) < \frac 1 {(n \pi)^2} \cdot \left(-1 + \frac 1 2\right) = - \frac 1 {2(n\pi)^2}$$
if $n$ is even.
</s>