Let $a,b,c$ be positive real numbers. Let $x(t)$ denote the solution of the following differential equation $$ \dot{x} = a - b\sin(x), \quad x(0)\in\mathbb{R}. $$
I'm interested in the computation of the following integral $$ \int_0^t \cos(x(\tau))e^{c\tau}\,\mathrm{d}\tau. $$
In particular, is it possible to derive a closed-form expression of the above integral?
So far, I've tried a brute-force approach via Wolfram Alpha. I can find (a quite nasty) an explicit expression for $x(t)$, but, using this expression, the computation of the integral seems not feasible with this symbolic tool. So I'm wondering if there exists some elegant tricks, that can avoid the use of symbolic math softwares. Thanks for your help!
HINT, we have:
$$\text{y}\space'\left(t\right)=\text{a}-\text{b}\cdot\sin\left(\text{y}\left(t\right)\right)\tag1$$
Divide both sides by the RHS:
$$\frac{\text{y}\space'\left(t\right)}{\text{a}-\text{b}\cdot\sin\left(\text{y}\left(t\right)\right)}=1\tag2$$
Integrate both sides with respect to $t$:
$$\int\frac{\text{y}\space'\left(t\right)}{\text{a}-\text{b}\cdot\sin\left(\text{y}\left(t\right)\right)}\space\text{d}t=\int1\space\text{d}t\tag3$$
The RHS of equation $\left(3\right)$, equals:
$$\int1\space\text{d}t=t+\text{C}_1\tag4$$
For the LHS of equation $\left(3\right)$, we substitute $\text{u}:=\text{y}\left(t\right)$:
$$\int\frac{\text{y}\space'\left(t\right)}{\text{a}-\text{b}\cdot\sin\left(\text{y}\left(t\right)\right)}\space\text{d}t=\int\frac{1}{\text{a}-\text{b}\cdot\sin\left(\text{u}\right)}\space\text{d}\text{u}\tag5$$
Now, substitute $\text{s}:=\tan\left(\frac{\text{u}}{2}\right)$.
Then you end up with:
$$\int\frac{1}{\text{a}-\text{b}\cdot\sin\left(\text{u}\right)}\space\text{d}\text{u}=2\cdot\int\frac{1}{\left(\text{s}\cdot\sqrt{\text{a}}-\frac{\text{b}}{\sqrt{\text{a}}}\right)^2+\frac{\text{a}^2-\text{b}^2}{\text{a}}}\space\text{d}\text{s}\tag6$$