let a, b, c, m be Nat; ( (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 )
set k = a |^ 2;
set l = b |^ 2;
A1:
( a |^ (2 * m) = (a |^ 2) |^ m & b |^ (2 * m) = (b |^ 2) |^ m )
by NEWTON:9;
A2: a |^ ((2 * m) + 2) =
a |^ (2 * (m + 1))
.=
(a |^ 2) |^ (m + 1)
by NEWTON:9
;
b |^ ((2 * m) + 2) =
b |^ (2 * (m + 1))
.=
(b |^ 2) |^ (m + 1)
by NEWTON:9
;
hence
( (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 )
by A1, A2, Th14; verum