let n be Nat; :: thesis: (n + 2) block n = (3 * ((n + 2) choose 4)) + ((n + 2) choose 3)
defpred S1[ Nat] means (\$1 + 2) block \$1 = (3 * ((\$1 + 2) choose 4)) + ((\$1 + 2) choose 3);
A1: 2 choose 3 = 0 by NEWTON:def 3;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
set k1 = k + 1;
set k2 = k + 2;
set k3 = (k + 2) + 1;
A4: (k + 1) * (((k + 1) + 1) block (k + 1)) = (k + 1) * ((k + 2) choose 2) by Th52
.= (k + 1) * (((k + 2) * ((k + 2) - 1)) / 2) by Th51
.= ((k + 2) * ((k + 2) - 1)) * (((k + 1) * 12) / 24) ;
(k + 2) block k = (3 * (((((k + 2) * ((k + 2) - 1)) * ((k + 2) - 2)) * ((k + 2) - 3)) / 24)) + ((k + 2) choose 3) by
.= (3 * (((((k + 2) * ((k + 2) - 1)) * ((k + 2) - 2)) * ((k + 2) - 3)) / 24)) + ((((k + 2) * ((k + 2) - 1)) * ((k + 2) - 2)) / 6) by Th51
.= ((k + 2) * ((k + 2) - 1)) * ((((3 * ((k + 2) - 2)) * ((k + 2) - 3)) / 24) + ((4 * ((k + 2) - 2)) / 24)) ;
then ((k + 2) + 1) block (k + 1) = (((k + 2) * (k + 1)) * (((k + 1) * 12) / 24)) + (((k + 2) * (k + 1)) * ((((3 * k) * ((k + 2) - 3)) / 24) + ((4 * k) / 24))) by
.= (3 * ((((((k + 2) + 1) * (((k + 2) + 1) - 1)) * (((k + 2) + 1) - 2)) * (((k + 2) + 1) - 3)) / 24)) + (((((k + 2) + 1) * (k + 2)) * (k + 1)) / 6)
.= (3 * (((k + 2) + 1) choose 4)) + (((((k + 2) + 1) * (((k + 2) + 1) - 1)) * (((k + 2) + 1) - 2)) / 6) by Th51
.= (3 * (((k + 2) + 1) choose 4)) + (((k + 2) + 1) choose 3) by Th51 ;
hence S1[k + 1] ; :: thesis: verum
end;
2 choose 4 = 0 by NEWTON:def 3;
then A5: S1[ 0 ] by ;
for k being Nat holds S1[k] from NAT_1:sch 2(A5, A2);
hence (n + 2) block n = (3 * ((n + 2) choose 4)) + ((n + 2) choose 3) ; :: thesis: verum