let a, b be Real_Sequence; :: thesis: ( ( for n being Nat holds a . n <= b . n ) & b is convergent & a is V48() implies ( a is convergent & lim a <= lim b ) )

assume that

A1: for n being Nat holds a . n <= b . n and

A2: b is convergent and

A3: a is V48() ; :: thesis: ( a is convergent & lim a <= lim b )

A4: b is bounded by A2;

A5: a is bounded_above

thus lim a <= lim b by A1, A2, A3, A5, SEQ_2:18; :: thesis: verum

assume that

A1: for n being Nat holds a . n <= b . n and

A2: b is convergent and

A3: a is V48() ; :: thesis: ( a is convergent & lim a <= lim b )

A4: b is bounded by A2;

A5: a is bounded_above

proof

hence
a is convergent
by A3; :: thesis: lim a <= lim b
consider r being Real such that

A6: for n being Nat holds b . n < r by A4, SEQ_2:def 3;

end;A6: for n being Nat holds b . n < r by A4, SEQ_2:def 3;

now :: thesis: for n being Nat holds a . n < r + 1

hence
a is bounded_above
by SEQ_2:def 3; :: thesis: verumlet n be Nat; :: thesis: a . n < r + 1

a . n <= b . n by A1;

then a . n <= r by A6, XXREAL_0:2;

then (a . n) + 0 < r + 1 by XREAL_1:8;

hence a . n < r + 1 ; :: thesis: verum

end;a . n <= b . n by A1;

then a . n <= r by A6, XXREAL_0:2;

then (a . n) + 0 < r + 1 by XREAL_1:8;

hence a . n < r + 1 ; :: thesis: verum

thus lim a <= lim b by A1, A2, A3, A5, SEQ_2:18; :: thesis: verum