let n be Nat; :: thesis: Sum (Reci-seq1,n,1) < 2 / 3
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 ;
V1: (rseq (0,1,1,(- (1 / 2)))) . 1 = 1 / ((1 * 1) + (- (1 / 2))) by AlgDef
.= 2 ;
V2: (- (rseq (0,1,1,(1 / 2)))) . 0 = - ((rseq (0,1,1,(1 / 2))) . 0) by VALUED_1:8
.= - (1 / ((1 * 0) + (1 / 2))) by AlgDef
.= - 2 ;
V3: (- (rseq (0,1,1,(1 / 2)))) . 1 = - ((rseq (0,1,1,(1 / 2))) . 1) by VALUED_1:8
.= - (1 / ((1 * 1) + (1 / 2))) by AlgDef
.= - (2 / 3) ;
Reci-seq1 . 0 = ((rseq (0,1,1,(- (1 / 2)))) . 0) + ((- (rseq (0,1,1,(1 / 2)))) . 0) by Tele2;
then V4: (Reci-seq1 . 0) + (Reci-seq1 . 1) = (((rseq (0,1,1,(- (1 / 2)))) . 0) + ((- (rseq (0,1,1,(1 / 2)))) . 0)) + (((rseq (0,1,1,(- (1 / 2)))) . 1) + ((- (rseq (0,1,1,(1 / 2)))) . 1)) by Tele2
.= (- 2) + (- (2 / 3)) by V1, V3, W2, V2 ;
V5: (Partial_Sums Reci-seq1) . 1 = ((Partial_Sums Reci-seq1) . 0) + (Reci-seq1 . (0 + 1)) by SERIES_1:def 1
.= (- 2) + (- (2 / 3)) by V4, SERIES_1:def 1 ;
W1: (- (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))) ;
W3: (Partial_Sums Reci-seq1) . n = (- 2) + ((- (rseq (0,1,1,(1 / 2)))) . n) by W2, ff, Telescoping, Tele2;
((- (rseq (0,1,1,(1 / 2)))) . n) + (2 / 3) < 0 + (2 / 3) by XREAL_1:8, W1;
hence Sum (Reci-seq1,n,1) < 2 / 3 by W3, V5; :: thesis: verum