In title, factor $x^{17}+1$ into a product of irreducibles over $\mathbb{R}$. I know it factors as $$(x+1)(x^{16}-x^{15}+\dots+1)$$
but I have no real justification for why the second factor is irreducible besides "mathematica says it's true and I don't want to try to factor it". I know it has no real zeros, since -1 is the only real zero of the original function and $x^{17}+1$ is coprime with its derivative, but that doesn't rule out that its the product of other irreducible polynomials of degrees higher than 1. I could also show the ideal generated by $x^{16}-x^{15}+\dots+1$ is maximal but that sounds horrific and I don't want to do it. Eisenstein's criterion also fails since the constant term is 1.
Consider $\omega_k=\cos(\frac{2k\pi}{17})+i\sin(\frac{2k\pi}{17})$, with $k\in\{0,...,16\}$. Now since $f(x)=x^{17}+1$ splits in $\mathbb{C}$ and $f(-\omega_k)=0, \forall k\in\{0,...,16\}$, we can write $f$ as, $$f(x)=\prod_{k=0}^{16}(x+\omega_k)=(x+1)\prod_{k=1}^{16}(x+\omega_k).$$ Using the fact that $f(-\omega_k)=0\implies f(-\overline{\omega_k})=0$ we have that, $$(x+1)\prod_{k=1}^{16}(x+\omega_k)=(x+1)\prod_{k=1}^8(x+\omega_k)(x+\overline{\omega_k})=(x+1)\prod_{k=1}^8(x^2+2\operatorname{Re}(\omega_k)+\lvert\omega_k\rvert^2)=$$
$$=(x+1)\prod_{k=1}^8(x^2+2\cos(\frac{2k\pi}{17})+1).$$ At this point notice that the polynomials $f_k(x)=(x^2+2\cos(\frac{2k\pi}{17})+1)\in\mathbb{R}[x]$ are degree 2 and have negative discriminant, for any $k\in\{1,...,16\}$, and therefore they are irreducible.