let seq be ExtREAL_sequence; :: thesis: ( seq is non-decreasing & +infty = sup seq implies ( seq is convergent_to_+infty & lim seq = +infty ) )
assume that
A1: seq is non-decreasing and
A2: +infty = sup seq ; :: thesis: ( seq is convergent_to_+infty & lim seq = +infty )
A3: seq is convergent_to_+infty
proof
assume not seq is convergent_to_+infty ; :: thesis: contradiction
then consider g being Real such that
0 < g and
A4: for n being Nat ex m being Nat st
( n <= m & seq . m < g ) by MESFUNC5:def 9;
for y being ExtReal st y in rng seq holds
y <= g
proof
let y be ExtReal; :: thesis: ( y in rng seq implies y <= g )
assume y in rng seq ; :: thesis: y <= g
then consider n being object such that
A5: n in NAT and
A6: y = seq . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A5;
consider m being Nat such that
A7: n <= m and
A8: seq . m < g by A4;
seq . n <= seq . m by A1, A7, Th7;
hence y <= g by A6, A8, XXREAL_0:2; :: thesis: verum
end;
then g is UpperBound of rng seq by XXREAL_2:def 1;
then A9: sup (rng seq) <= g by XXREAL_2:def 3;
g in REAL by XREAL_0:def 1;
hence contradiction by A2, A9, XXREAL_0:9; :: thesis: verum
end;
then seq is convergent by MESFUNC5:def 11;
hence ( seq is convergent_to_+infty & lim seq = +infty ) by A3, MESFUNC5:def 12; :: thesis: verum