Insane trig identities

Trig identities are the bread and butter of high-school precalculus instructors. However, after a certain point, the ones that usually show up in textbooks just get tedious and follow from the same old tired trig identities. This is a shame, because trig functions also satisfy some really crazy identities that require more creative proofs. Here are some gems (some of which admittedly push the boundary of what can be called a "trig identity").

Most of these are from Math Stack Exchange, and their proofs have varying levels of difficulty. Bask in their glory!

$$\cos\big(\frac{\pi}{5}\big) = \frac{\phi}{2}$$ $$\cos\big(\frac{2\pi}{5}\big) = \frac{1}{2\phi}$$

$$\arctan(1) + \arctan(2) + \arctan(3) = \pi$$

$$\sin\frac{\pi}{7}\cdot \sin\frac{2\pi}{7}\cdot \sin\frac{3\pi}{7} = \frac{\sqrt{7}}{8}$$ $$\cos\frac{\pi}{7}\cdot \cos\frac{2\pi}{7}\cdot \cos\frac{3\pi}{7} = \frac{1}{8}$$ $$\frac{1}{\sin\frac{2\pi}{7}} + \frac{1}{\sin\frac{3\pi}{7}} = \frac{1}{\sin\frac{\pi}{7}}$$ $$-\sin\frac{\pi}{7} + \sin\frac{2\pi}{7} + \sin\frac{4\pi}{7} = \frac{\sqrt{7}}{2}$$

$$\sqrt[3]{\cos\frac{2\pi}{7}} + \sqrt[3]{\cos\frac{4\pi}{7}} + \sqrt[3]{\cos\frac{8\pi}{7}} = \sqrt[3]{\frac{5-3\sqrt[3]{7}}{2}}$$ $$\sqrt[3]{\cos\frac{2\pi}{9}} + \sqrt[3]{\cos\frac{4\pi}{9}} + \sqrt[3]{\cos\frac{8\pi}{9}} = \sqrt[3]{\frac{3\sqrt[3]{9}-6}{2}}$$

$$\tan\frac{2\pi}{13}\cdot\tan\frac{5\pi}{13}\cdot\tan\frac{6\pi}{13} = \sqrt{65 + 18\sqrt{13}}$$

$$\sqrt[3]{\cos\frac{2\pi}{13}+\cos\frac{10\pi}{13}}+ \sqrt[3]{\cos\frac{4\pi}{13}+\cos\frac{6\pi}{13}}+ \sqrt[3]{\cos\frac{8\pi}{13}+\cos\frac{12\pi}{13}}= \sqrt[3]{\frac{3\sqrt[3]{13}-7}2}$$

$$\sum_{k=1}^{n-1} \frac{1}{\sin^2\frac{\pi k}{n}} = \frac{n^2-1}{3}$$

$$\lim_{N\to\infty} \frac{1}{n}\cdot \big|\big\{x\in \mathbb R ~ : ~ |x| < n, ~ \sin(x) + \sin(x\sqrt{2}) = 1\big\}\big| = \frac{(1+\sqrt{2})\pi -2\arcsin(\sqrt{3}-1) - 2\sqrt{2}\arcsin(2-\sqrt{3}))}{\pi^2}$$

$$\sum_{n\in\mathbb Z} \frac{\sin n}{n} = \sum_{n\in\mathbb Z} \Big(\frac{\sin n}{n}\Big)^2 = \int_\mathbb{R} \frac{\sin x}{x} ~ dx = \int_\mathbb{R} \Big(\frac{\sin x}{x}\Big)^2 ~ dx = \pi$$

$$\sum_{n=1}^\infty \frac{1}{n}\sin\big(\frac{x}{n}\big) = \Omega(\sqrt{\log\log n})$$

$$\sum_{n=1}^\infty \frac{\cot(\pi n \phi)}{n^3} = -\frac{\pi^3}{45\sqrt{5}}$$ $$\sum_{n=1}^\infty \frac{\cot(\pi n \sqrt{61})}{n^3} = -\frac{16793\pi^3}{45660\sqrt{61}}$$

$$\sum_{n=1}^\infty \frac{1}{n^3 \sin\pi n\sqrt{2}} = -\frac{13\pi^3}{360\sqrt{2}}$$

$$\lim_{m\to\infty} \frac{1}{\log m}\sum_{n=1}^m \frac{1}{n^2 \sin^2(\pi n \phi)} = \frac{2\pi^2}{15\sqrt{5}\log\phi}$$