>>12998501Here's a proof technique then.
Consider f(x) = SUM[n*cos(nx)] up to N.
Differentiate it 2k times then evaluate at 0 to get the sum of (2k+1) powers (with a factor (-1)^k).
f(x) has a nasty closed form so this looks like it will not work.
The trick will be to use strong induction on k.
f(x) = [1 - (N+1)cos(Nx) + Ncos((N+1)x)]/[2i*sin(x/2)]^2
Multiply both sides by -2sin(x/2)^2 = cos(x)-1
[cos(x)-1]*f(x) = [1 - (N+1)cos(Nx) + Ncos((N+1)x)]/2
Differentiate this 2k+2 times and evaluate at 0.
Clearly N(N+1)/2 divides the right hand side.
For the left side use
https://en.wikipedia.org/wiki/General_Leibniz_ruleThe odd derivatives of f (the sums of even powers) won't contribute because they will have sin terms.
The 2k+2 derivative of f won't contribute because the cos(x)-1 is 0 at x=0.
If we assume N(N+1)/2 divides all even derivatives below 2k of f at zero so we must conclude it also divides f^(2k)(0)*(2k+2)(2k+1)/2.
