let rseq be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds 0 <= rseq . n ) implies ( ( for n being Element of NAT holds 0 <= (Partial_Sums rseq) . n ) & ( for n being Element of NAT holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Element of NAT holds rseq . n <= Sum rseq ) ) ) ) )
assume A1: for n being Element of NAT holds 0 <= rseq . n ; :: thesis: ( ( for n being Element of NAT holds 0 <= (Partial_Sums rseq) . n ) & ( for n being Element of NAT holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Element of NAT holds rseq . n <= Sum rseq ) ) ) )
A2: Partial_Sums rseq is V45() by A1, SERIES_1:16;
thus A3: for n being Element of NAT holds 0 <= (Partial_Sums rseq) . n :: thesis: ( ( for n being Element of NAT holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Element of NAT holds rseq . n <= Sum rseq ) ) ) )

proof

let n be Element of 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;

thus A5: for n being Element of NAT holds rseq . n <= (Partial_Sums rseq) . n :: thesis: ( rseq is summable implies ( ( for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Element of NAT holds rseq . n <= Sum rseq ) ) )

proof

let n be Element of NAT ; :: thesis: rseq . n <= (Partial_Sums rseq) . n

now

per cases ( n = 0 or n <> 0 ) ;

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

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

end;

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

set nn = n - 1;
0 + 1 <= n by A6, INT_1:7;
then A7: n - 1 in NAT by INT_1:5;
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 A7, SERIES_1:def 1; :: thesis: verum

end;

end;

end;

hence rseq . n <= (Partial_Sums rseq) . n ; :: thesis: verum

end;

assume rseq is summable ; :: thesis: ( ( for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Element of NAT holds rseq . n <= Sum rseq ) )
then A8: Partial_Sums rseq is bounded_above by A1, SERIES_1:17;
thus A9: for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq :: thesis: for n being Element of NAT holds rseq . n <= Sum rseq

proof

let n be Element of NAT ; :: thesis: (Partial_Sums rseq) . n <= Sum rseq
(Partial_Sums rseq) . n <= lim (Partial_Sums rseq) by A1, A8, SEQ_4:37, SERIES_1:16;
hence (Partial_Sums rseq) . n <= Sum rseq by SERIES_1:def 3; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: rseq . n <= Sum rseq
A10: rseq . n <= (Partial_Sums rseq) . n by A5;
(Partial_Sums rseq) . n <= Sum rseq by A9;
hence rseq . n <= Sum rseq by A10, XXREAL_0:2; :: thesis: verum