let n be Nat; ((n |^ 2) * (((2 * (n |^ 2)) + (2 * n)) - 1)) + (((n + 1) |^ 3) * 12) = ((n + 2) |^ 2) * (((2 * ((n + 1) |^ 2)) + (2 * (n + 1))) - 1)
A1: ((n |^ 2) * (((2 * (n |^ 2)) + (2 * n)) - 1)) + (((n + 1) |^ 3) * 12) =
(((2 * ((n |^ 2) * (n |^ 2))) + (2 * (n * (n |^ 2)))) - (n |^ 2)) + (((n + 1) |^ 3) * 12)
.=
(((2 * (n |^ (2 + 2))) + (2 * (n * (n |^ 2)))) - (n |^ 2)) + (((n + 1) |^ 3) * 12)
by NEWTON:8
.=
(((2 * (n |^ (2 + 2))) + (2 * (n |^ (2 + 1)))) - (n |^ 2)) + (((n + 1) |^ 3) * 12)
by NEWTON:6
.=
(((2 * (n |^ 4)) + (2 * (n |^ 3))) - (n |^ 2)) + (((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1) * 12)
by Lm4
.=
((((((2 * (n |^ 4)) + (2 * (n |^ 3))) - (n |^ 2)) + ((n |^ 3) * 12)) + (36 * (n |^ 2))) + (36 * n)) + 12
;
((n + 2) |^ 2) * (((2 * ((n + 1) |^ 2)) + (2 * (n + 1))) - 1) =
((n + 2) |^ 2) * (((2 * (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) + (2 * (n + 1))) - 1)
by Lm3
.=
(((n |^ 2) + ((2 * n) * 2)) + (2 |^ 2)) * (((((2 * (n |^ 2)) + ((2 * n) * 2)) + (2 * (1 |^ 2))) + ((2 * n) + (2 * 1))) - 1)
by Lm3
.=
(((n |^ 2) + ((2 * n) * 2)) + (2 |^ 2)) * (((((2 * (n |^ 2)) + (4 * n)) + (2 * 1)) + ((2 * n) + 2)) - 1)
.=
(((n |^ 2) + (4 * n)) + (2 * 2)) * ((((((2 * (n |^ 2)) + (4 * n)) + 2) + (2 * n)) + 2) - 1)
by WSIERP_1:1
.=
((((2 * ((n |^ 2) * (n |^ 2))) + (6 * (n * (n |^ 2)))) + ((n |^ 2) * 3)) + ((4 * n) * (((2 * (n |^ 2)) + (6 * n)) + 3))) + ((((2 * (n |^ 2)) * 4) + (24 * n)) + 12)
.=
((((2 * (n |^ (2 + 2))) + (6 * (n * (n |^ 2)))) + ((n |^ 2) * 3)) + ((4 * n) * (((2 * (n |^ 2)) + (6 * n)) + 3))) + ((((2 * (n |^ 2)) * 4) + (24 * n)) + 12)
by NEWTON:8
.=
((((2 * (n |^ (2 + 2))) + (6 * (n |^ (2 + 1)))) + ((n |^ 2) * 3)) + ((4 * n) * (((2 * (n |^ 2)) + (6 * n)) + 3))) + ((((2 * (n |^ 2)) * 4) + (24 * n)) + 12)
by NEWTON:6
.=
((((2 * (n |^ 4)) + (6 * (n |^ 3))) + ((n |^ 2) * 3)) + ((((4 * (n * (n |^ 2))) * 2) + ((4 * (n * n)) * 6)) + ((4 * n) * 3))) + (((8 * (n |^ 2)) + (24 * n)) + 12)
.=
((((2 * (n |^ 4)) + (6 * (n |^ 3))) + ((n |^ 2) * 3)) + ((((4 * (n |^ (2 + 1))) * 2) + (24 * (n * n))) + ((4 * n) * 3))) + (((8 * (n |^ 2)) + (24 * n)) + 12)
by NEWTON:6
.=
((((2 * (n |^ 4)) + (6 * (n |^ 3))) + ((n |^ 2) * 3)) + ((((4 * (n |^ 3)) * 2) + (24 * (n |^ 2))) + (12 * n))) + (((8 * (n |^ 2)) + (24 * n)) + 12)
by WSIERP_1:1
.=
((((((2 * (n |^ 4)) + (14 * (n |^ 3))) + (27 * (n |^ 2))) + (12 * n)) + (8 * (n |^ 2))) + (24 * n)) + 12
;
hence
((n |^ 2) * (((2 * (n |^ 2)) + (2 * n)) - 1)) + (((n + 1) |^ 3) * 12) = ((n + 2) |^ 2) * (((2 * ((n + 1) |^ 2)) + (2 * (n + 1))) - 1)
by A1; verum