I have the initial value problem
$$\ddot x (t) + k \sin(x(t)) = 0$$
with initial conditions $x(0) =: x_0 $ and $\dot x (0) =: v_0$. Using Maxima I should check that
$$\frac{1}{2}(\dot x (t))^2 + k (1-\cos(x(t))) = \text{const}$$
So I though I will simply find solution and substitute. But the solution I got is ugly
$$\pm \frac{\displaystyle\int{\frac{dx}{\sqrt{k\cos(x)-\%k1k}}}}{\sqrt{2}}=t+\%k2$$
I haven't used my initial condition about $x$ and $\dot x$ because I am not sure how?
I will be more than glad for help.
$$\frac{d^2x}{dt^2}+k\sin(x)=0$$
$2\frac{d^2x}{dt^2}\frac{dx}{dt}+2k\sin(x)\frac{dx}{dt}=0 \quad\to\quad \left(\frac{dx}{dt}\right)^2-2k\cos(x)=c_1$
$x(0)=x_0$ and $x'(0)=v_0$ $\to$ $(v_0)^2-2k\cos(x_0)=c_1$ $$\left(\frac{dx}{dt}\right)^2-2k\cos(x)=(v_0)^2-2k\cos(x_0)$$
$$dt=\pm \frac{dx}{\sqrt{2k\cos(x)-2k\cos(x_0)+(v_0)^2}}$$
$$t=\int_{x_0}^x \frac{d\chi}{\sqrt{2k\cos(\chi)-2k\cos(x_0)+(v_0)^2}}$$
$$ t= \sqrt{\frac{m}{k}}\left( F\left(\frac{x}{2}\:\Bigg|\:m\right) - F\left(\frac{x_0}{2}\:\Bigg|\:m\right)\right)$$ $m=\frac{4k}{v_0^2+2k-2k\cos(x_0)}$ and $F\:$ is the elliptic integral of the first kind.
The inverse function $x(t)$ can be expressed in terms of Jacobi amplitude function : http://mathworld.wolfram.com/JacobiAmplitude.html
In ADDITION to my first answer :
Reading again the question, especially this point :
If that's all the problem, the analytic answer is easy :
Multiply the ODE by $\dot x(t)$ and integrate :
$$\ddot x (t)\dot x(t) + k \sin(x(t))\dot x(t) = 0$$ $$\frac{1}{2}\left(\dot x(t)\right)^2 -k \cos\left(x(t)\right) = c$$ $$\frac{1}{2}\left(\dot x(t)\right)^2 +k\left(1- \cos\left(x(t)\right) \right)=k+c $$ $$\frac{1}{2}\left(\dot x(t)\right)^2 +k\left(1- \cos\left(x(t)\right) \right) = \text{const} $$ That is what it was asked to show.
So, you just have to make the symbolic computer doing the same than what was handly done above.