Solution (source code)

= Solution

By <De Moivre's theorem>, $(e^{i\alpha})^j=e^{ij\alpha}$. The complex sum whose real part is wanted is therefore a <finite geometric series>:
$$
Z=\sum_{j=0}^ne^{i(\theta+j\alpha)}
=e^{i\theta}\frac{1-e^{i(n+1)\alpha}}{1-e^{i\alpha}},
\qquad \alpha\notin2\pi\mathbb Z.
$$
Use $1-e^{i\beta}=-2ie^{i\beta/2}\sin(\beta/2)$ in the numerator and denominator. This yields
$$
Z=\frac{\sin((n+1)\alpha/2)}{\sin(\alpha/2)}
e^{i(\theta+n\alpha/2)}.
$$
Taking its real part proves the <finite trigonometric sum>
$$
\boxed{\sum_{j=0}^n\cos(\theta+j\alpha)
=\frac{\sin((n+1)\alpha/2)}{\sin(\alpha/2)}
\cos\left(\theta+\frac{n\alpha}{2}\right).}
$$
When $\alpha\in2\pi\mathbb Z$, the printed quotient is undefined; the original sum is directly \b[$(n+1)\cos\theta$], also the limiting value of the displayed identity. The denominator restriction cannot be omitted from a literal use of the quotient.