let a, b be Complex; (a - b) |^ 4 = ((((a |^ 4) - ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) - ((4 * (b |^ 3)) * a)) + (b |^ 4)
(a - b) |^ (3 + 1) =
((a - b) |^ 3) * (a - b)
by NEWTON:6
.=
((((a |^ 3) - ((3 * (a |^ 2)) * b)) + ((3 * (b |^ 2)) * a)) - (b |^ 3)) * (a - b)
by Th5
.=
(((((a |^ 3) * a) - ((a |^ 3) * b)) + ((- (((3 * (a |^ 2)) * b) * a)) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) - (((3 * (b |^ 2)) * a) * b))) + ((- ((b |^ 3) * a)) + ((b |^ 3) * b))
.=
(((((a |^ 3) * a) - ((a |^ 3) * b)) + ((- (((3 * (a |^ 2)) * b) * a)) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) - (((3 * (b |^ 2)) * a) * b))) + ((- ((b |^ 3) * a)) + (b |^ (3 + 1)))
by NEWTON:6
.=
((((a |^ 4) - ((a |^ 3) * b)) + ((- ((3 * ((a |^ 2) * a)) * b)) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) - (((3 * (b |^ 2)) * a) * b))) + ((- ((b |^ 3) * a)) + (b |^ 4))
by NEWTON:6
.=
((((a |^ 4) - ((a |^ 3) * b)) + ((- ((3 * (a |^ (2 + 1))) * b)) + (((3 * (a |^ 2)) * b) * b))) + ((((3 * (b |^ 2)) * a) * a) - (((3 * (b |^ 2)) * a) * b))) + ((- ((b |^ 3) * a)) + (b |^ 4))
by NEWTON:6
.=
((((a |^ 4) - ((a |^ 3) * b)) + ((- ((3 * (a |^ 3)) * b)) + ((3 * (a |^ 2)) * (b * b)))) + ((((3 * (b |^ 2)) * a) * a) - (((3 * (b |^ 2)) * a) * b))) + ((- ((b |^ 3) * a)) + (b |^ 4))
.=
((((a |^ 4) - ((a |^ 3) * b)) + ((- ((3 * (a |^ 3)) * b)) + ((3 * (a |^ 2)) * ((b |^ 1) * b)))) + ((((3 * (b |^ 2)) * a) * a) - (((3 * (b |^ 2)) * a) * b))) + ((- ((b |^ 3) * a)) + (b |^ 4))
.=
((((a |^ 4) - ((a |^ 3) * b)) + ((- ((3 * (a |^ 3)) * b)) + ((3 * (a |^ 2)) * (b |^ (1 + 1))))) + ((((3 * (b |^ 2)) * a) * a) - (((3 * (b |^ 2)) * a) * b))) + ((- ((b |^ 3) * a)) + (b |^ 4))
by NEWTON:6
.=
((((a |^ 4) - ((a |^ 3) * b)) + ((- ((3 * (a |^ 3)) * b)) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * (a * a)) - (((3 * (b |^ 2)) * a) * b))) + ((- ((b |^ 3) * a)) + (b |^ 4))
.=
((((a |^ 4) - ((a |^ 3) * b)) + ((- ((3 * (a |^ 3)) * b)) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * ((a |^ 1) * a)) - (((3 * (b |^ 2)) * b) * a))) + ((- ((b |^ 3) * a)) + (b |^ 4))
.=
((((a |^ 4) - ((a |^ 3) * b)) + ((- ((3 * (a |^ 3)) * b)) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * (a |^ (1 + 1))) - ((3 * ((b |^ 2) * b)) * a))) + ((- ((b |^ 3) * a)) + (b |^ 4))
by NEWTON:6
.=
((((a |^ 4) - ((a |^ 3) * b)) + ((- ((3 * (a |^ 3)) * b)) + ((3 * (a |^ 2)) * (b |^ 2)))) + (((3 * (b |^ 2)) * (a |^ 2)) - ((3 * (b |^ (2 + 1))) * a))) + ((- ((b |^ 3) * a)) + (b |^ 4))
by NEWTON:6
.=
((((a |^ 4) - ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) - ((4 * (b |^ 3)) * a)) + (b |^ 4)
;
hence
(a - b) |^ 4 = ((((a |^ 4) - ((4 * (a |^ 3)) * b)) + ((6 * (a |^ 2)) * (b |^ 2))) - ((4 * (b |^ 3)) * a)) + (b |^ 4)
; verum