let rseq be Real_Sequence; :: thesis: ( ( for n being Nat holds 0 <= rseq . n ) implies ( ( for n being Nat holds 0 <= (Partial_Sums rseq) . n ) & ( for n being Nat holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Nat holds rseq . n <= Sum rseq ) ) ) ) )

assume A1: for n being Nat holds 0 <= rseq . n ; :: thesis: ( ( for n being Nat holds 0 <= (Partial_Sums rseq) . n ) & ( for n being Nat holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Nat holds rseq . n <= Sum rseq ) ) ) )

A2: Partial_Sums rseq is V50() by A1, SERIES_1:16;

thus A3: for n being Nat holds 0 <= (Partial_Sums rseq) . n :: thesis: ( ( for n being Nat holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Nat holds rseq . n <= Sum rseq ) ) ) )

then A9: Partial_Sums rseq is bounded_above by A1, SERIES_1:17;

thus A10: for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq :: thesis: for n being Nat holds rseq . n <= Sum rseq

A11: rseq . n <= (Partial_Sums rseq) . n by A5;

(Partial_Sums rseq) . n <= Sum rseq by A10;

hence rseq . n <= Sum rseq by A11, XXREAL_0:2; :: thesis: verum

assume A1: for n being Nat holds 0 <= rseq . n ; :: thesis: ( ( for n being Nat holds 0 <= (Partial_Sums rseq) . n ) & ( for n being Nat holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Nat holds rseq . n <= Sum rseq ) ) ) )

A2: Partial_Sums rseq is V50() by A1, SERIES_1:16;

thus A3: for n being Nat holds 0 <= (Partial_Sums rseq) . n :: thesis: ( ( for n being Nat holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Nat holds rseq . n <= Sum rseq ) ) ) )

proof

thus A5:
for n being Nat holds rseq . n <= (Partial_Sums rseq) . n
:: thesis: ( rseq is summable implies ( ( for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Nat holds rseq . n <= Sum rseq ) ) )
let n be Nat; :: thesis: 0 <= (Partial_Sums rseq) . n

A4: ( n = n + 0 & (Partial_Sums rseq) . 0 = rseq . 0 ) by SERIES_1:def 1;

0 <= rseq . 0 by A1;

hence 0 <= (Partial_Sums rseq) . n by A2, A4, SEQM_3:5; :: thesis: verum

end;A4: ( n = n + 0 & (Partial_Sums rseq) . 0 = rseq . 0 ) by SERIES_1:def 1;

0 <= rseq . 0 by A1;

hence 0 <= (Partial_Sums rseq) . n by A2, A4, SEQM_3:5; :: thesis: verum

proof

assume
rseq is summable
; :: thesis: ( ( for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Nat holds rseq . n <= Sum rseq ) )
let n be Nat; :: thesis: rseq . n <= (Partial_Sums rseq) . n

end;now :: thesis: ( ( n = 0 & rseq . n <= (Partial_Sums rseq) . n ) or ( n <> 0 & rseq . n <= (Partial_Sums rseq) . n ) )end;

hence
rseq . n <= (Partial_Sums rseq) . n
; :: thesis: verumper cases
( n = 0 or n <> 0 )
;

end;

case A6:
n <> 0
; :: thesis: rseq . n <= (Partial_Sums rseq) . n

A7:
n in NAT
by ORDINAL1:def 12;

set nn = n - 1;

0 + 1 <= n by A6, INT_1:7, A7;

then A8: n - 1 in NAT by INT_1:5, A7;

then 0 <= (Partial_Sums rseq) . (n - 1) by A3;

then ( (n - 1) + 1 = n & (rseq . n) + 0 <= (rseq . n) + ((Partial_Sums rseq) . (n - 1)) ) by XREAL_1:7;

hence rseq . n <= (Partial_Sums rseq) . n by A8, SERIES_1:def 1; :: thesis: verum

end;set nn = n - 1;

0 + 1 <= n by A6, INT_1:7, A7;

then A8: n - 1 in NAT by INT_1:5, A7;

then 0 <= (Partial_Sums rseq) . (n - 1) by A3;

then ( (n - 1) + 1 = n & (rseq . n) + 0 <= (rseq . n) + ((Partial_Sums rseq) . (n - 1)) ) by XREAL_1:7;

hence rseq . n <= (Partial_Sums rseq) . n by A8, SERIES_1:def 1; :: thesis: verum

then A9: Partial_Sums rseq is bounded_above by A1, SERIES_1:17;

thus A10: for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq :: thesis: for n being Nat holds rseq . n <= Sum rseq

proof

let n be Nat; :: thesis: rseq . n <= Sum rseq
let n be Nat; :: thesis: (Partial_Sums rseq) . n <= Sum rseq

(Partial_Sums rseq) . n <= lim (Partial_Sums rseq) by A1, A9, SEQ_4:37, SERIES_1:16;

hence (Partial_Sums rseq) . n <= Sum rseq by SERIES_1:def 3; :: thesis: verum

end;(Partial_Sums rseq) . n <= lim (Partial_Sums rseq) by A1, A9, SEQ_4:37, SERIES_1:16;

hence (Partial_Sums rseq) . n <= Sum rseq by SERIES_1:def 3; :: thesis: verum

A11: rseq . n <= (Partial_Sums rseq) . n by A5;

(Partial_Sums rseq) . n <= Sum rseq by A10;

hence rseq . n <= Sum rseq by A11, XXREAL_0:2; :: thesis: verum