theorem Th20: :: NUMBER04:20

for k being Nat
for r being Real holds Sum (OddEvenPowers (r,((2 * k) + 3))) = ((r |^ ((2 * k) + 2)) - (r |^ ((2 * k) + 1))) + (Sum (OddEvenPowers (r,((2 * k) + 1))))