let f, g be Real_Sequence; :: thesis: ( f is convergent & g is convergent & g majorizes f implies lim f <= lim g )
assume that
A1: ( f is convergent & g is convergent ) and
A2: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
f . n <= g . n ; :: according to ASYMPT_0:def 8 :: thesis: lim f <= lim g
consider N being Element of NAT such that
A3: for n being Element of NAT st n >= N holds
f . n <= g . n by A2;
now :: thesis: for n being Nat st n >= N holds
0 <= (g - f) . n
let n be Nat; :: thesis: ( n >= N implies 0 <= (g - f) . n )
A4: n in NAT by ORDINAL1:def 12;
assume n >= N ; :: thesis: 0 <= (g - f) . n
then f . n <= g . n by A3, A4;
then A5: (f . n) - (f . n) <= (g . n) - (f . n) by XREAL_1:9;
(g - f) . n = (g . n) + ((- f) . n) by SEQ_1:7
.= (g . n) + (- (f . n)) by SEQ_1:10
.= (g . n) - (f . n) ;
hence 0 <= (g - f) . n by A5; :: thesis: verum
end;
then A6: g - f is eventually-nonnegative ;
A7: lim (g - f) = (lim g) - (lim f) by A1, SEQ_2:12;
g - f is convergent by A1, SEQ_2:11;
then 0 <= lim (g - f) by A6, Th3;
then 0 + (lim f) <= ((lim g) - (lim f)) + (lim f) by A7, XREAL_1:6;
hence lim f <= lim g ; :: thesis: verum