let n be Nat; ((n * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30) = ((n + 2) * ((2 * (n + 1)) + 1)) * (((3 * ((n + 1) |^ 2)) + (3 * (n + 1))) - 1)
((n + 2) * ((2 * (n + 1)) + 1)) * (((3 * ((n + 1) |^ 2)) + (3 * (n + 1))) - 1) =
((n + 2) * ((2 * n) + 3)) * (((3 * (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) + ((3 * n) + 3)) - 1)
by Lm3
.=
(((n * (2 * n)) + (2 * (2 * n))) + ((n * 3) + (2 * 3))) * ((((3 * (((n |^ 2) + (2 * n)) + (1 |^ 2))) + (3 * n)) + 3) - 1)
.=
(((n * (2 * n)) + (2 * (2 * n))) + ((n * 3) + (2 * 3))) * ((((3 * (((n |^ 2) + (2 * n)) + 1)) + (3 * n)) + 3) - 1)
.=
((((n * n) * 2) + ((2 * 2) * n)) + ((n * 3) + 6)) * (((((((n |^ 2) * 3) + (6 * n)) + 3) + (3 * n)) + 3) - 1)
.=
(((2 * (n |^ 2)) + (4 * n)) + ((n * 3) + 6)) * ((((((3 * (n |^ 2)) + (6 * n)) + 3) + (3 * n)) + 3) - 1)
by WSIERP_1:1
.=
(((((2 * ((n |^ 2) * (n |^ 2))) * 3) + (((2 * (n |^ 2)) * n) * 9)) + (10 * (n |^ 2))) + (((((7 * n) * (n |^ 2)) * 3) + (((7 * n) * n) * 9)) + (35 * n))) + ((((6 * 3) * (n |^ 2)) + ((6 * 9) * n)) + 30)
.=
(((((2 * (n |^ (2 + 2))) * 3) + ((2 * ((n |^ 2) * n)) * 9)) + (10 * (n |^ 2))) + ((((7 * (n * (n |^ 2))) * 3) + ((7 * (n * n)) * 9)) + (35 * n))) + (((18 * (n |^ 2)) + (54 * n)) + 30)
by NEWTON:8
.=
(((((2 * (n |^ 4)) * 3) + ((2 * (n |^ (2 + 1))) * 9)) + (10 * (n |^ 2))) + ((((7 * (n * (n |^ 2))) * 3) + ((7 * (n * n)) * 9)) + (35 * n))) + (((18 * (n |^ 2)) + (54 * n)) + 30)
by NEWTON:6
.=
((((6 * (n |^ 4)) + ((2 * (n |^ 3)) * 9)) + (10 * (n |^ 2))) + ((((7 * (n |^ (2 + 1))) * 3) + ((7 * (n * n)) * 9)) + (35 * n))) + (((18 * (n |^ 2)) + (54 * n)) + 30)
by NEWTON:6
;
then A1: ((n + 2) * ((2 * (n + 1)) + 1)) * (((3 * ((n + 1) |^ 2)) + (3 * (n + 1))) - 1) =
((((6 * (n |^ 4)) + (18 * (n |^ 3))) + (10 * (n |^ 2))) + ((((7 * (n |^ 3)) * 3) + ((7 * (n |^ 2)) * 9)) + (35 * n))) + (((18 * (n |^ 2)) + (54 * n)) + 30)
by WSIERP_1:1
.=
((((6 * (n |^ 4)) + (39 * (n |^ 3))) + ((73 + 18) * (n |^ 2))) + (89 * n)) + 30
;
((n * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30) =
(((2 * (n * n)) + n) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30)
.=
(((2 * ((n |^ 1) * n)) + n) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30)
.=
(((2 * (n |^ (1 + 1))) + n) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30)
by NEWTON:6
.=
(((((2 * ((n |^ 2) * (n |^ 2))) * 3) + ((n * (n |^ 2)) * 3)) + (((2 * ((n |^ 2) * n)) * 3) + ((n * n) * 3))) - ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 3) * 30)
.=
(((((2 * (n |^ (2 + 2))) * 3) + ((n * (n |^ 2)) * 3)) + (((2 * ((n |^ 2) * n)) * 3) + ((n * n) * 3))) - ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 3) * 30)
by NEWTON:8
.=
(((((2 * (n |^ 4)) * 3) + ((n * (n |^ 2)) * 3)) + (((2 * (n |^ (2 + 1))) * 3) + ((n * n) * 3))) - ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 3) * 30)
by NEWTON:6
.=
(((((2 * (n |^ 4)) * 3) + ((n * (n |^ 2)) * 3)) + (((2 * (n |^ 3)) * 3) + ((n |^ 2) * 3))) - ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 3) * 30)
by WSIERP_1:1
.=
((((6 * (n |^ 4)) + ((n |^ (2 + 1)) * 3)) + ((6 * (n |^ 3)) + ((n |^ 2) * 3))) - ((2 * (n |^ 2)) + n)) + (((n + 1) |^ 3) * 30)
by NEWTON:6
.=
((((6 * (n |^ 4)) + (9 * (n |^ 3))) + (1 * (n |^ 2))) - n) + (((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * 30)
by Lm4
.=
((((6 * (n |^ 4)) + (39 * (n |^ 3))) + (91 * (n |^ 2))) + ((90 - 1) * n)) + 30
;
hence
((n * ((2 * n) + 1)) * (((3 * (n |^ 2)) + (3 * n)) - 1)) + (((n + 1) |^ 3) * 30) = ((n + 2) * ((2 * (n + 1)) + 1)) * (((3 * ((n + 1) |^ 2)) + (3 * (n + 1))) - 1)
by A1; verum