let a, b be Real; (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 Th2
.=
(((((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