Proving solution is defined and $C^{\infty}$

Question

Consider the harmonic pendulum problem with $l=1$, $\ddot{x}=-g \sin(x)$ with $x(t_0) = x_0$; $x'(t_0)=v_0$. Show that the solution $\varphi(t,t_0,x_0,v_0,g)$ is defined on all $\mathbb{R}^5$ and is of class $C^{\infty}$.

I am not sure how to proceed on this, I know that $-g \sin(x)$ is $C^{\infty}$ but I don't see how to use this so that the solution is well defined and also $C^{\infty}$. In my book I have the following theorem that might be related to this:

Theorem - Let $f$ be a continuous function on the open $\Omega$ of $\mathbb{R}\times \mathbb{E}\times\Lambda$ where $\Lambda$ and $\mathbb{E}$ are Euclidean spaces. Suppose that $D_2 f$ is continuous on $\Omega$. Then for a fixed $\lambda$, the solution $\varphi = \varphi(t,t_0,x_0,\lambda)$ of $x'=f(t,x,\lambda)$ with $x(t_0) = x_0$ is unique and admits partial derivative $D_3\varphi$ with respect to $x_0$. Even more, the map $(t,t_0,x_0,\lambda)\rightarrow D_3\varphi(t,t_0,x_0,\lambda)$ is continuous on its domain $D = [(t,t_0,x_0,\lambda);((t,x_0,\lambda)\in \Omega,\omega_-(t_0,x_0,\lambda)<t<\omega_+(t_0,x_0,\lambda)]$ and $$x(t) = D_3\varphi(t,t_0,x_0,\lambda)\cdot e_k = \frac{\partial \varphi}{\partial x_0^k},$$ for all $1\leq k\leq \text{dim} \mathbb{E}$ is solution of $x'=J(t)x$, $x(t_0) = e_k$, where $J(t) = J(t,t_0,x_0,\lambda)=D_2f(t,\varphi(t,t_0,x_0,\lambda),\lambda)$.

Answer 1

Sketch. The standard method of reducing to a first order ODE works here, set $$ X = \binom x{x'},\quad X'=f(X), \quad f\left(\binom{a}{b}\right) := \binom{b}{-g \sin a}$$ Since $f$ is globally Lipschitz, a global solution exists $\phi$ for any initial data $t_0,x_0,v_0$. In fact $F$ is smooth with bounded derivatives, so $\phi$ is also. $F$ is smooth in the parameter $g$. By dependence on initial data/parameters results, this transfers to smoothness of the solution in the initial data and parameter as well.

"Gerald Teschl - Ordinary Differential Equations and Dynamical Systems" has these theorems, for instance