theorem :: NEWTON01:23

for a, b, c, m being Nat holds
( (a |^ ((2 * m) + 2)) - (b |^ ((2 * m) + 2)) = (((a |^ 2) - (b |^ 2)) * (((c * ((a |^ 2) + (b |^ 2))) + (a |^ (2 * m))) + (b |^ (2 * m)))) / 2 iff (a |^ (2 * m)) - (b |^ (2 * m)) = ((a |^ 2) - (b |^ 2)) * c )