let s1, s2 be Real_Sequence; :: thesis: ( ( 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 ; :: thesis: ( 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; :: thesis: 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

for n being Nat holds (s1 ^\ (N + 1)) . n <= (s2 ^\ (N + 1)) . n

((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; :: thesis: verum

( 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 ; :: thesis: ( 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; :: thesis: 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

proof

A12:
s2 ^\ (N + 1) is summable
by A3, SERIES_1:12;
let n be Nat; :: thesis: 0 <= (s1 ^\ (N + 1)) . n

(s1 ^\ (N + 1)) . n = s1 . (n + (N + 1)) by NAT_1:def 3;

hence 0 <= (s1 ^\ (N + 1)) . n by A1; :: thesis: verum

end;(s1 ^\ (N + 1)) . n = s1 . (n + (N + 1)) by NAT_1:def 3;

hence 0 <= (s1 ^\ (N + 1)) . n by A1; :: thesis: verum

for n being Nat holds (s1 ^\ (N + 1)) . n <= (s2 ^\ (N + 1)) . n

proof

then A14:
Sum (s1 ^\ (N + 1)) <= Sum (s2 ^\ (N + 1))
by A11, A12, SERIES_1:20;
let n be Nat; :: thesis: (s1 ^\ (N + 1)) . n <= (s2 ^\ (N + 1)) . n

A13: (s1 ^\ (N + 1)) . n = s1 . (n + (N + 1)) by NAT_1:def 3;

(s2 ^\ (N + 1)) . n = s2 . (n + (N + 1)) by NAT_1:def 3;

hence (s1 ^\ (N + 1)) . n <= (s2 ^\ (N + 1)) . n by A1, A13; :: thesis: verum

end;A13: (s1 ^\ (N + 1)) . n = s1 . (n + (N + 1)) by NAT_1:def 3;

(s2 ^\ (N + 1)) . n = s2 . (n + (N + 1)) by NAT_1:def 3;

hence (s1 ^\ (N + 1)) . n <= (s2 ^\ (N + 1)) . n by A1, A13; :: thesis: verum

((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; :: thesis: verum