let a, b be Real; ( (a |^ 3) + (b |^ 3) = (a + b) * (((a ^2) - (a * b)) + (b ^2)) & (a |^ 5) + (b |^ 5) = (a + b) * (((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4)) )
A1: (a + b) * (((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4)) =
(((((((a |^ 4) * a) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b))
.=
(((((((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b))
.=
(((((a |^ (4 + 1)) + (b * (a |^ 4))) - (((a |^ 3) * b) * ((a + b) + 0))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b))
by NEWTON:8
.=
(((((a |^ 5) + (b * (a |^ 4))) - (((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b)))) + ((a * ((a |^ 2) * (b |^ 2))) + (b * ((a |^ 2) * (b |^ 2))))) - ((a * (a * (b |^ 3))) + (b * (a * (b |^ 3))))) + ((a * (b |^ 4)) + (b * (b |^ 4)))
.=
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b * (b |^ 3)) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4)))
by POLYEQ_2:4
.=
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4)))
by POLYEQ_2:4
.=
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ (2 + 1)) * (b |^ 2)) + (((b |^ 2) * b) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4)))
by NEWTON:6
.=
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ (2 + 1)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + ((b |^ 4) * b))
by NEWTON:6
.=
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1)))
by NEWTON:6
.=
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1)))
.=
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1)))
.=
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ 5))
by NEWTON:6
.=
(((a |^ 5) + ((a |^ 2) * (b |^ 3))) - (((a |^ 2) * (b |^ 3)) + (a * (b |^ 4)))) + ((a * (b |^ 4)) + (b |^ 5))
by NEWTON:6
.=
(a |^ 5) + (b |^ 5)
;
(((a ^2) - (a * b)) + (b ^2)) * (a + b) =
((((a ^2) * a) + (b * (a ^2))) - ((a * (a * b)) + (b * (a * b)))) + (((a * (b ^2)) + (b * (b ^2))) + (0 * (b ^2)))
.=
(((a |^ 3) + (b * (a ^2))) - ((a * (a * b)) + (b * (a * b)))) + ((a * (b ^2)) + (b * (b ^2)))
by POLYEQ_2:4
.=
(((a |^ 3) + (b * (a ^2))) - (((a ^2) * b) + ((b * b) * a))) + ((a * (b ^2)) + (b |^ 3))
by POLYEQ_2:4
.=
(a |^ 3) + (b |^ 3)
;
hence
( (a |^ 3) + (b |^ 3) = (a + b) * (((a ^2) - (a * b)) + (b ^2)) & (a |^ 5) + (b |^ 5) = (a + b) * (((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4)) )
by A1; verum