let a, b be Real_Sequence; :: thesis: ( ( for i being Nat holds a . i <= b . i ) & a is non-decreasing & b is non-increasing implies ( a is convergent & b is convergent ) )
assume that
A1: for i being Nat holds a . i <= b . i and
A2: a is non-decreasing and
A3: b is non-increasing ; :: thesis: ( a is convergent & b is convergent )
now :: thesis: ex r being set st
for n being Nat holds a . n < r
take r = (b . 0) + 1; :: thesis: for n being Nat holds a . n < r
hereby :: thesis: verum
let n be Nat; :: thesis: a . n < r
reconsider n0 = n as ExtReal ;
0 in NAT ;
then A4: 0 in dom b by SEQ_1:1;
n in NAT by ORDINAL1:def 12;
then n0 in dom b by SEQ_1:1;
then A5: b . n0 <= b . 0 by A4, A3;
a . n <= b . n by A1;
then a . n <= b . 0 by A5, XXREAL_0:2;
then (a . n) + 0 < (b . 0) + 1 by XREAL_1:8;
hence a . n < r ; :: thesis: verum
end;
end;
then A6: a is bounded_above by SEQ_2:def 3;
now :: thesis: ex r being set st
for n being Nat holds r < b . n
take r = (a . 0) - 1; :: thesis: for n being Nat holds r < b . n
hereby :: thesis: verum
let n be Nat; :: thesis: r < b . n
reconsider n0 = n as ExtReal ;
0 in NAT ;
then A7: 0 in dom a by SEQ_1:1;
n in NAT by ORDINAL1:def 12;
then n0 in dom a by SEQ_1:1;
then A8: a . 0 <= a . n0 by A7, A2;
a . n <= b . n by A1;
then a . 0 <= b . n by A8, XXREAL_0:2;
then (a . 0) - 1 < (b . n) - 0 by XREAL_1:15;
hence r < b . n ; :: thesis: verum
end;
end;
then b is bounded_below by SEQ_2:def 4;
hence ( a is convergent & b is convergent ) by A2, A3, A6; :: thesis: verum