let n be Nat; :: thesis: ( 3 <= n implies Sum ((TriangleShift2 (n,2)) ") = (2 / 3) - ((n + 1) / (Triangle n)) )
defpred S1[ Nat] means Sum ((TriangleShift2 ($1,2)) ") = (2 / 3) - (($1 + 1) / H2($1));
A1: S1[3] by NUMPOLY1:13;
A2: for j being Nat st 3 <= j & S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( 3 <= j & S1[j] implies S1[j + 1] )
assume that
A3: 3 <= j and
A4: S1[j] ; :: thesis: S1[j + 1]
A5: H2(j + 1) = H2(j) + (j + 1) by NUMPOLY1:10;
A6: H2(j) = (j * (j + 1)) / 2 by NUMPOLY1:19;
then A7: ((j * (j + 1)) + (2 * (j + 1))) / 2 = (H2(j) + j) + 1 ;
A8: ((j + 1) / H2(j)) - (1 / H2(j)) = ((j + 1) - 1) / H2(j)
.= (2 * j) / (j * (j + 1)) by A6, XCMPLX_1:77
.= 2 / (j + 1) by A3, XCMPLX_1:91
.= (2 * (j + 2)) / ((j + 2) * (j + 1)) by XCMPLX_1:91
.= ((j + 1) + 1) / H2(j + 1) by A5, A7, XCMPLX_1:77 ;
A9: <*H2(j)*> " = <*(H2(j) ")*> by NUMBER15:63;
TriangleShift2 ((j + 1),2) = (TriangleShift2 (j,2)) ^ <*H2(j)*> by Lm26, A3, Th131;
then (TriangleShift2 ((j + 1),2)) " = ((TriangleShift2 (j,2)) ") ^ (<*H2(j)*> ") by NUMBER15:60;
hence Sum ((TriangleShift2 ((j + 1),2)) ") = (Sum ((TriangleShift2 (j,2)) ")) + (H2(j) ") by A9, RVSUM_2:31
.= (2 / 3) - (((j + 1) + 1) / H2(j + 1)) by A4, A8 ;
:: thesis: verum
end;
for i being Nat st 3 <= i holds
S1[i] from NAT_1:sch 8(A1, A2);
 hence ( 3 <= n implies Sum ((TriangleShift2 (n,2)) ") = (2 / 3) - ((n + 1) / (Triangle n)) ) ; :: thesis: verum