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
proof
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;
A12: s2 ^\ (N + 1) is summable by A3, SERIES_1:12;
for n being Nat holds (s1 ^\ (N + 1)) . n <= (s2 ^\ (N + 1)) . n
proof
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;
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; :: thesis: verum