let s1, s2 be Real_Sequence; ( ( for n being Nat holds
( 0 <= s1 . n & s1 . n <= s2 . n ) ) & ex n being Nat st
( 1 <= n & s1 . n < s2 . n ) & s2 is summable implies ( s1 is summable & Sum s1 < Sum s2 ) )
assume that
A1:
for n being Nat holds
( 0 <= s1 . n & s1 . n <= s2 . n )
and
A2:
ex n being Nat st
( 1 <= n & s1 . n < s2 . n )
and
A3:
s2 is summable
; ( s1 is summable & Sum s1 < Sum s2 )
consider N being Nat such that
A4:
( 1 <= N & s1 . N < s2 . N )
by A2;
A5:
for n being Nat st 0 <= n holds
s1 . n <= s2 . n
by A1;
hence
s1 is summable
by A1, A3, SERIES_1:19; Sum s1 < Sum s2
N - 1 in NAT
by A4, INT_1:5;
then reconsider N1 = N - 1 as Nat ;
A6:
N1 + 1 = N
;
then A7:
(Partial_Sums s1) . N = ((Partial_Sums s1) . N1) + (s1 . N)
by SERIES_1:def 1;
A8:
Sum s1 = ((Partial_Sums s1) . N) + (Sum (s1 ^\ (N + 1)))
by A1, A3, A5, SERIES_1:15, SERIES_1:19;
A9:
(Partial_Sums s2) . N = ((Partial_Sums s2) . N1) + (s2 . N)
by A6, SERIES_1:def 1;
A10:
Sum s2 = ((Partial_Sums s2) . N) + (Sum (s2 ^\ (N + 1)))
by SERIES_1:15, A3;
A11:
for n being Nat holds 0 <= (s1 ^\ (N + 1)) . n
A12:
s2 ^\ (N + 1) is summable
by A3, SERIES_1:12;
for n being Nat holds (s1 ^\ (N + 1)) . n <= (s2 ^\ (N + 1)) . n
then A14:
Sum (s1 ^\ (N + 1)) <= Sum (s2 ^\ (N + 1))
by A11, A12, SERIES_1:20;
((Partial_Sums s1) . N1) + (s1 . N) < ((Partial_Sums s2) . N1) + (s2 . N)
by XREAL_1:8, A4, A1, SERIES_1:14;
hence
Sum s1 < Sum s2
by A7, A8, A9, A10, A14, XREAL_1:8; verum