let n be Nat; ((Triangle (n + 1)) |^ 2) - ((Triangle n) |^ 2) = (n + 1) |^ 3
A1: Triangle (n + 1) =
((n + 1) * ((n + 1) + 1)) / 2
by Th19
.=
((n + 1) * (n + 2)) / 2
;
A2: (n + 1) |^ 3 =
((n + 1) * (n + 1)) * (n + 1)
by POLYEQ_3:27
.=
((((n * n) * n) + ((3 * n) * n)) + (3 * n)) + 1
;
A3:
(n + 1) * (n + 1) = (n + 1) |^ 2
by NEWTON:81;
((Triangle (n + 1)) |^ 2) - ((Triangle n) |^ 2) =
((((n + 1) * (n + 2)) / 2) |^ 2) - (((n * (n + 1)) / 2) |^ 2)
by Th19, A1
.=
((((n + 1) * (n + 2)) / 2) * (((n + 1) * (n + 2)) / 2)) - (((n * (n + 1)) / 2) |^ 2)
by NEWTON:81
.=
(((((n + 1) * (n + 1)) * (n + 2)) * (n + 2)) / 4) - (((n * (n + 1)) / 2) |^ 2)
.=
(((((n + 1) |^ 2) * (n + 2)) * (n + 2)) / 4) - (((n * (n + 1)) / 2) |^ 2)
by NEWTON:81
.=
(((((n + 1) |^ 2) * (n + 2)) * (n + 2)) / 4) - (((n * (n + 1)) / 2) * ((n * (n + 1)) / 2))
by NEWTON:81
.=
(((((n + 1) |^ 2) * (n + 2)) * (n + 2)) / 4) - ((((n * n) * (n + 1)) * (n + 1)) / 4)
.=
(((((n + 1) |^ 2) * (n + 2)) * (n + 2)) / 4) - ((((n |^ 2) * (n + 1)) * (n + 1)) / 4)
by NEWTON:81
.=
(((n + 1) |^ 2) * (((((n * n) + (2 * n)) + (2 * n)) + 4) - (n |^ 2))) / 4
by A3
.=
(((n + 1) |^ 2) * (((((n |^ 2) + (2 * n)) + (2 * n)) + 4) - (n |^ 2))) / 4
by NEWTON:81
.=
((n + 1) |^ 2) * (n + 1)
.=
((n + 1) * (n + 1)) * (n + 1)
by NEWTON:81
.=
(n + 1) |^ 3
by A2
;
hence
((Triangle (n + 1)) |^ 2) - ((Triangle n) |^ 2) = (n + 1) |^ 3
; verum