let n be Nat; :: thesis: (Partial_Sums Reci-seq1) . n = (- 2) + (- (1 / (n + (1 / 2))))
set s = Reci-seq1 ;
set a = rseq (0,1,1,(- (1 / 2)));
set b = - (rseq (0,1,1,(1 / 2)));
ff: for k being Nat holds (- (rseq (0,1,1,(1 / 2)))) . k = - ((rseq (0,1,1,(- (1 / 2)))) . (k + 1))
proof
let k be Nat; :: thesis: (- (rseq (0,1,1,(1 / 2)))) . k = - ((rseq (0,1,1,(- (1 / 2)))) . (k + 1))
(- (rseq (0,1,1,(1 / 2)))) . k = - ((rseq (0,1,1,(1 / 2))) . k) by VALUED_1:8
.= - (1 / ((1 * k) + (1 / 2))) by AlgDef
.= - (1 / ((1 * (k + 1)) + (- (1 / 2))))
.= - ((rseq (0,1,1,(- (1 / 2)))) . (k + 1)) by AlgDef ;
hence (- (rseq (0,1,1,(1 / 2)))) . k = - ((rseq (0,1,1,(- (1 / 2)))) . (k + 1)) ; :: thesis: verum
end;
W2: (rseq (0,1,1,(- (1 / 2)))) . 0 = 1 / ((1 * 0) + (- (1 / 2))) by AlgDef
.= - 2 ;
(- (rseq (0,1,1,(1 / 2)))) . n = - ((rseq (0,1,1,(1 / 2))) . n) by VALUED_1:8
.= - (1 / ((1 * n) + (1 / 2))) by AlgDef
.= - (1 / (n + (1 / 2))) ;
hence (Partial_Sums Reci-seq1) . n = (- 2) + (- (1 / (n + (1 / 2)))) by W2, ff, Telescoping, Tele2; :: thesis: verum