let n be Nat; (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;
(- (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))
;
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; verum