Solution (source code)

= Solution

For every <integer> $j\geq0$, the $j$th derivative with respect to $t$ of $\cos(t\cos x)$ is $(\cos x)^j$ times a sine or cosine with a sign. Its absolute value is at most $1$ on the finite <interval> $[0,\pi/2]$. This is an integrable dominating function independent of $t$. Repeated <differentiation under the integral sign> is therefore justified for every order, giving \b[$J_0\in C^\infty(\mathbb R)$].