theorem :: NEWTON01:24

for m being Nat
for a1, b1 being Complex holds (a1 |^ ((2 * m) + 3)) + (b1 |^ ((2 * m) + 3)) = (((a1 |^ ((2 * m) + 2)) + (b1 |^ ((2 * m) + 2))) * (a1 + b1)) - ((a1 * b1) * ((a1 |^ ((2 * m) + 1)) + (b1 |^ ((2 * m) + 1))))