Btukfyl

I'm trying to prove the following:
$$ int_0^{2 pi} e^{cos(2 t)} cos(sin(2 t)) =2pi $$

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?

Write

$$ I(alpha) = int_{0}^{2pi} e^{alpha cos(2t)}cos(alpha sin(2t)) , dt. $$

Then $I(0) = 2pi$, and for $alpha > 0$,

begin{align*}
I'(alpha)
&= int_{0}^{2pi} 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}{2alpha} e^{alphacos(2t)}sin(alphasin(2t)) right]_{0}^{2pi} \
&= 0.
end{align*}

So $I(alpha) = 2pi$ 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}^{2pi} f(re^{itheta}) , dtheta. $$

Then

$$ I'(r)
= int_{0}^{2pi} f'(re^{itheta})e^{itheta} , dtheta
= left[ frac{1}{ir} f(re^{itheta}) right]_{0}^{2pi}
= 0 $$

and thus $I$ is constant with the value $I(0) = 2pi f(0)$. The above answer corresponds to the real part of this computation with $f(z) = e^z$.