let n be Real; ( (n + 1) |^ 4 = ((((n |^ 4) + (4 * (n |^ 3))) + (6 * (n |^ 2))) + (4 * n)) + 1 & (n + 1) |^ 5 = (((((n |^ 5) + (5 * (n |^ 4))) + (10 * (n |^ 3))) + (10 * (n |^ 2))) + (5 * n)) + 1 )
A1: (n + 1) |^ (3 + 1) =
((n + 1) |^ 3) * (n + 1)
by NEWTON:6
.=
((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * (n + 1)
by Lm4
.=
(((((n |^ 3) * n) + (n |^ 3)) + ((3 * ((n |^ 2) * n)) + (3 * (n |^ 2)))) + ((3 * (n * n)) + (3 * n))) + (n + 1)
.=
((((n |^ (3 + 1)) + (n |^ 3)) + ((3 * ((n |^ 2) * n)) + (3 * (n |^ 2)))) + ((3 * (n * n)) + (3 * n))) + (n + 1)
by NEWTON:6
.=
((((n |^ (3 + 1)) + (n |^ 3)) + ((3 * (n |^ (2 + 1))) + (3 * (n |^ 2)))) + ((3 * (n * n)) + (3 * n))) + (n + 1)
by NEWTON:6
.=
((((n |^ 4) + (n |^ 3)) + ((3 * (n |^ 3)) + (3 * (n |^ 2)))) + ((3 * (n |^ 2)) + (3 * n))) + (n + 1)
by WSIERP_1:1
;
(n + 1) |^ (3 + 2) =
((n + 1) |^ 3) * ((n + 1) |^ 2)
by NEWTON:8
.=
((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * ((n + 1) |^ 2)
by Lm4
.=
((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))
by Lm3
.=
((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * (((n |^ 2) + (2 * n)) + 1)
.=
((((((n |^ 3) * (n |^ 2)) + ((2 * n) * (n |^ 3))) + ((n |^ 3) * 1)) + ((((3 * (n |^ 2)) * (n |^ 2)) + ((2 * n) * (3 * (n |^ 2)))) + ((3 * (n |^ 2)) * 1))) + ((((3 * n) * (n |^ 2)) + ((3 * n) * (2 * n))) + ((3 * n) * 1))) + (((n |^ 2) + (2 * n)) + 1)
.=
(((((n |^ (3 + 2)) + (2 * (n * (n |^ 3)))) + (n |^ 3)) + (((3 * ((n |^ 2) * (n |^ 2))) + ((2 * (n * (n |^ 2))) * 3)) + (3 * (n |^ 2)))) + (((3 * (n * (n |^ 2))) + ((3 * (n * n)) * 2)) + (3 * n))) + (((n |^ 2) + (2 * n)) + 1)
by NEWTON:8
.=
(((((n |^ (3 + 2)) + (2 * (n * (n |^ 3)))) + (n |^ 3)) + (((3 * (n |^ (2 + 2))) + ((2 * (n * (n |^ 2))) * 3)) + (3 * (n |^ 2)))) + (((3 * (n * (n |^ 2))) + ((3 * (n * n)) * 2)) + (3 * n))) + (((n |^ 2) + (2 * n)) + 1)
by NEWTON:8
.=
(((((n |^ (3 + 2)) + (2 * (n |^ (3 + 1)))) + (n |^ 3)) + (((3 * (n |^ (2 + 2))) + ((2 * (n * (n |^ 2))) * 3)) + (3 * (n |^ 2)))) + (((3 * (n * (n |^ 2))) + ((3 * (n * n)) * 2)) + (3 * n))) + (((n |^ 2) + (2 * n)) + 1)
by NEWTON:6
.=
(((((n |^ (3 + 2)) + (2 * (n |^ (3 + 1)))) + (n |^ 3)) + (((3 * (n |^ (2 + 2))) + ((2 * (n |^ (2 + 1))) * 3)) + (3 * (n |^ 2)))) + (((3 * (n * (n |^ 2))) + ((3 * (n * n)) * 2)) + (3 * n))) + (((n |^ 2) + (2 * n)) + 1)
by NEWTON:6
.=
(((((n |^ 5) + (2 * (n |^ 4))) + (n |^ 3)) + (((3 * (n |^ 4)) + ((2 * (n |^ 3)) * 3)) + (3 * (n |^ 2)))) + (((3 * (n |^ 3)) + ((3 * (n * n)) * 2)) + (3 * n))) + (((n |^ 2) + (2 * n)) + 1)
by NEWTON:6
.=
(((((n |^ 5) + (2 * (n |^ 4))) + (n |^ 3)) + (((3 * (n |^ 4)) + (6 * (n |^ 3))) + (3 * (n |^ 2)))) + (((3 * (n |^ 3)) + ((3 * (n |^ 2)) * 2)) + (3 * n))) + (((n |^ 2) + (2 * n)) + 1)
by WSIERP_1:1
;
hence
( (n + 1) |^ 4 = ((((n |^ 4) + (4 * (n |^ 3))) + (6 * (n |^ 2))) + (4 * n)) + 1 & (n + 1) |^ 5 = (((((n |^ 5) + (5 * (n |^ 4))) + (10 * (n |^ 3))) + (10 * (n |^ 2))) + (5 * n)) + 1 )
by A1; verum