let n be Nat; ((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - ((n + 1) |^ 2)) - (4 * (n + 1))) + 2) = ((n |^ 2) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) + (((n + 1) |^ 5) * 24)
A1: ((n |^ 2) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) + (((n + 1) |^ 5) * 24) =
(((((3 * ((n |^ 4) * (n |^ 2))) + (6 * ((n |^ 3) * (n |^ 2)))) - ((n |^ 2) * (n |^ 2))) - (4 * (n * (n |^ 2)))) + ((n |^ 2) * 2)) + (((n + 1) |^ 5) * 24)
.=
(((((3 * (n |^ (4 + 2))) + (6 * ((n |^ 3) * (n |^ 2)))) - ((n |^ 2) * (n |^ 2))) - (4 * (n * (n |^ 2)))) + ((n |^ 2) * 2)) + (((n + 1) |^ 5) * 24)
by NEWTON:8
.=
(((((3 * (n |^ (4 + 2))) + (6 * (n |^ (3 + 2)))) - ((n |^ 2) * (n |^ 2))) - (4 * (n * (n |^ 2)))) + ((n |^ 2) * 2)) + (((n + 1) |^ 5) * 24)
by NEWTON:8
.=
(((((3 * (n |^ (4 + 2))) + (6 * (n |^ (3 + 2)))) - (n |^ (2 + 2))) - (4 * (n * (n |^ 2)))) + ((n |^ 2) * 2)) + (((n + 1) |^ 5) * 24)
by NEWTON:8
.=
(((((3 * (n |^ (4 + 2))) + (6 * (n |^ (3 + 2)))) - (n |^ (2 + 2))) - (4 * (n |^ (2 + 1)))) + ((n |^ 2) * 2)) + (((n + 1) |^ 5) * 24)
by NEWTON:6
.=
(((((3 * (n |^ 6)) + (6 * (n |^ 5))) - (n |^ 4)) - (4 * (n |^ 3))) + ((n |^ 2) * 2)) + (((((((n |^ 5) + (5 * (n |^ 4))) + (10 * (n |^ 3))) + (10 * (n |^ 2))) + (5 * n)) + 1) * 24)
by Lm6
.=
((((((3 * (n |^ 6)) + (30 * (n |^ 5))) + (119 * (n |^ 4))) + (236 * (n |^ 3))) + ((n |^ 2) * 242)) + (120 * n)) + 24
;
((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - ((n + 1) |^ 2)) - (4 * (n + 1))) + 2) =
((n + 2) |^ 2) * ((((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - ((n + 1) |^ 2)) - (4 * n)) - 4) + 2)
.=
((n + 2) |^ 2) * ((((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) - (4 * n)) - 4) + 2)
by Lm3
.=
((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) - (4 * n)) - 2)
.=
((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1))) - (((n |^ 2) + (2 * n)) + (1 |^ 2))) - (4 * n)) - 2)
by Lm4
.=
((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((((n |^ 3) + (3 * (n |^ 2))) + (3 * n)) + 1))) - (((n |^ 2) + (2 * n)) + 1)) - (4 * n)) - 2)
.=
((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * (n |^ 3))) + ((18 - 1) * (n |^ 2))) + (((18 - 2) - 4) * n)) + 3)
.=
((n + 2) |^ 2) * (((((3 * (((((n |^ 4) + (4 * (n |^ 3))) + (6 * (n |^ 2))) + (4 * n)) + 1)) + (6 * (n |^ 3))) + (17 * (n |^ 2))) + (12 * n)) + 3)
by Lm6
.=
(((n |^ 2) + ((2 * n) * 2)) + (2 * 2)) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (35 * (n |^ 2))) + (24 * n)) + 6)
by Lm3
.=
((((((3 * ((n |^ 4) * (n |^ 2))) + (18 * ((n |^ 3) * (n |^ 2)))) + (35 * ((n |^ 2) * (n |^ 2)))) + (24 * (n * (n |^ 2)))) + ((n |^ 2) * 6)) + ((4 * n) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (35 * (n |^ 2))) + (24 * n)) + 6))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24)
.=
((((((3 * (n |^ (4 + 2))) + (18 * ((n |^ 3) * (n |^ 2)))) + (35 * ((n |^ 2) * (n |^ 2)))) + (24 * (n * (n |^ 2)))) + ((n |^ 2) * 6)) + ((4 * n) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (35 * (n |^ 2))) + (24 * n)) + 6))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24)
by NEWTON:8
.=
((((((3 * (n |^ (4 + 2))) + (18 * (n |^ (3 + 2)))) + (35 * ((n |^ 2) * (n |^ 2)))) + (24 * (n * (n |^ 2)))) + ((n |^ 2) * 6)) + ((4 * n) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (35 * (n |^ 2))) + (24 * n)) + 6))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24)
by NEWTON:8
.=
((((((3 * (n |^ (4 + 2))) + (18 * (n |^ (3 + 2)))) + (35 * (n |^ (2 + 2)))) + (24 * (n * (n |^ 2)))) + ((n |^ 2) * 6)) + ((4 * n) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (35 * (n |^ 2))) + (24 * n)) + 6))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24)
by NEWTON:8
.=
((((((3 * (n |^ (4 + 2))) + (18 * (n |^ (3 + 2)))) + (35 * (n |^ (2 + 2)))) + (24 * (n |^ (2 + 1)))) + ((n |^ 2) * 6)) + ((4 * n) * (((((3 * (n |^ 4)) + (18 * (n |^ 3))) + (35 * (n |^ 2))) + (24 * n)) + 6))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24)
by NEWTON:6
.=
((((((3 * (n |^ 6)) + (18 * (n |^ 5))) + (35 * (n |^ 4))) + (24 * (n |^ 3))) + ((n |^ 2) * 6)) + (((((12 * ((n |^ 4) * n)) + (72 * ((n |^ 3) * n))) + (140 * ((n |^ 2) * n))) + (96 * (n * n))) + (24 * n))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24)
.=
((((((3 * (n |^ 6)) + (18 * (n |^ 5))) + (35 * (n |^ 4))) + (24 * (n |^ 3))) + ((n |^ 2) * 6)) + (((((12 * (n |^ (4 + 1))) + (72 * ((n |^ 3) * n))) + (140 * ((n |^ 2) * n))) + (96 * (n * n))) + (24 * n))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24)
by NEWTON:6
.=
((((((3 * (n |^ 6)) + (18 * (n |^ 5))) + (35 * (n |^ 4))) + (24 * (n |^ 3))) + ((n |^ 2) * 6)) + (((((12 * (n |^ (4 + 1))) + (72 * (n |^ (3 + 1)))) + (140 * ((n |^ 2) * n))) + (96 * (n * n))) + (24 * n))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24)
by NEWTON:6
.=
((((((3 * (n |^ 6)) + (18 * (n |^ 5))) + (35 * (n |^ 4))) + (24 * (n |^ 3))) + ((n |^ 2) * 6)) + (((((12 * (n |^ (4 + 1))) + (72 * (n |^ (3 + 1)))) + (140 * (n |^ (2 + 1)))) + (96 * (n * n))) + (24 * n))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24)
by NEWTON:6
.=
((((((3 * (n |^ 6)) + (18 * (n |^ 5))) + (35 * (n |^ 4))) + (24 * (n |^ 3))) + ((n |^ 2) * 6)) + (((((12 * (n |^ 5)) + (72 * (n |^ 4))) + (140 * (n |^ 3))) + (96 * (n |^ 2))) + (24 * n))) + (((((12 * (n |^ 4)) + (72 * (n |^ 3))) + (140 * (n |^ 2))) + (96 * n)) + 24)
by WSIERP_1:1
.=
((((((3 * (n |^ 6)) + (30 * (n |^ 5))) + (119 * (n |^ 4))) + (236 * (n |^ 3))) + (242 * (n |^ 2))) + (120 * n)) + 24
;
hence
((n + 2) |^ 2) * (((((3 * ((n + 1) |^ 4)) + (6 * ((n + 1) |^ 3))) - ((n + 1) |^ 2)) - (4 * (n + 1))) + 2) = ((n |^ 2) * (((((3 * (n |^ 4)) + (6 * (n |^ 3))) - (n |^ 2)) - (4 * n)) + 2)) + (((n + 1) |^ 5) * 24)
by A1; verum