Tricky real integral: $\int_0^{2 \pi} e^{\cos(2 t)} \cos(\sin(2 t)) =2\pi$ I'm trying to prove the following:
$$ \int_0^{2 \pi} e^{\cos(2 t)} \cos(\sin(2 t))  =2\pi $$
Numerical analysis agrees with this to very high accuracy, so I'm almost sure it's true. Mathematica gives this answer after thinking for a long, but gives an insane antiderivative in terms of exponential integrals. I'd like to evaluate the integral with purely real methods (I've never done complex analysis), as elegantly as possible.
How can I tackle this integral?
 A: Assuming that you could enjoy special functions.
Consider
$$I=\int e^{\cos(a t)} \cos(\sin(a t))\,dt\qquad \text{and}\qquad J=\int e^{\cos(a t)} \sin(\sin(a t))\,dt$$
$$I+iJ=\int e^{e^{ i at}}\,dt=-\frac{i}{a}\, \text{Ei}\left(e^{i a t}\right)$$
$$I-iJ=\int e^{e^{- ia t}}\,dt=\frac{i}{a} \, \text{Ei}\left(e^{- i a t}\right)$$ (where appear the exponential integral function) since, using $e^{kt}=u$,
$$\int e^{e^{kt}}\,dt=\frac{1}{k }\int\frac{e^u}{u}\,du=\frac{1}{k }\,\text{Ei}(u)$$ This makes
$$I=\frac{i }{2 a}\,\left(\text{Ei}\left(e^{-i a t}\right)-\text{Ei}\left(e^{i a
   t}\right)\right)$$
$$J=-\frac{1}{2 a}\,\left(\text{Ei}\left(e^{-i a t}\right)+\text{Ei}\left(e^{i a t}\right)\right)$$ For integer values of $a$, the definite integration from $0$ to $2\pi$ requires breaking it in $2a$ intervals and, as @user170231 commented, the result is $2\pi$ for any $a$.
A: Write
$$ I(\alpha) = \int_{0}^{2\pi} e^{\alpha \cos(2t)}\cos(\alpha \sin(2t)) \, dt. $$
Then $I(0) = 2\pi$, and for $\alpha > 0$,
\begin{align*}
I'(\alpha)
&= \int_{0}^{2\pi} \left[ e^{\alpha \cos(2t)}\cos(\alpha \sin(2t))\cos(2t) - e^{\alpha \cos(2t)}\sin(\alpha \sin(2t))\sin(2t) \right] \, dt \\
&= \left[ \frac{1}{2\alpha} e^{\alpha\cos(2t)}\sin(\alpha\sin(2t)) \right]_{0}^{2\pi} \\
&= 0.
\end{align*}
So $I(\alpha) = 2\pi$ for all $\alpha \in \mathbb{R}$.

A general computation. Let $f$ be analytic on $B(0,R)$. Define $I : [0, R) \to \mathbb{C}$ by
$$ I(r) = \int_{0}^{2\pi} f\left(re^{i\theta}\right) \, d\theta. $$
Then
$$ I'(r)
= \int_{0}^{2\pi} f'\left(re^{i\theta}\right)e^{i\theta} \, d\theta
= \left[ \frac{1}{ir} f\left(re^{i\theta}\right) \right]_{0}^{2\pi}
= 0 $$
and thus $I$ is constant with the value $I(0) = 2\pi f(0)$. The above answer corresponds to the real part of this computation with $f(z) = e^z$.
A: Put $z=e^{it}$ and using the formulas:
$$\cos{2t}=\frac{z^2+\frac{1}{z^2}}{2}$$
$$\sin{2t}=\frac{z^2-\frac{1}{z^2}}{2i}$$
apply the $\text{Residue theorem}$ integrating along the circle $C(0,1)=\{z:|z|=1\}$
