let seq be ExtREAL_sequence; :: thesis: ( seq is non-increasing implies ( seq is convergent & lim seq = inf seq ) )

assume A1: seq is non-increasing ; :: thesis: ( seq is convergent & lim seq = inf seq )

assume A1: seq is non-increasing ; :: thesis: ( seq is convergent & lim seq = inf seq )

per cases
( for n being Element of NAT holds +infty <= seq . n or ex n being Element of NAT st not +infty <= seq . n )
;

end;

suppose A2:
for n being Element of NAT holds +infty <= seq . n
; :: thesis: ( seq is convergent & lim seq = inf seq )

A6: seq is convergent_to_+infty by A2, Th32;

hence A7: seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = inf seq

then rng seq = {+infty} by A5, XBOOLE_0:def 10;

then inf seq = +infty by XXREAL_2:13;

hence lim seq = inf seq by A6, A7, MESFUNC5:def 12; :: thesis: verum

end;

now :: thesis: for y being object st y in {+infty} holds

y in rng seq

then A5:
{+infty} c= rng seq
;y in rng seq

let y be object ; :: thesis: ( y in {+infty} implies y in rng seq )

assume y in {+infty} ; :: thesis: y in rng seq

then A3: y = +infty by TARSKI:def 1;

end;assume y in {+infty} ; :: thesis: y in rng seq

then A3: y = +infty by TARSKI:def 1;

now :: thesis: y in rng seq

hence
y in rng seq
; :: thesis: verumassume A4:
not y in rng seq
; :: thesis: contradiction

end;now :: thesis: for n being Element of NAT holds contradiction

hence
contradiction
; :: thesis: verumlet n be Element of NAT ; :: thesis: contradiction

n in NAT ;

then n in dom seq by FUNCT_2:def 1;

then seq . n <> +infty by A3, A4, FUNCT_1:def 3;

hence contradiction by A2, XXREAL_0:4; :: thesis: verum

end;n in NAT ;

then n in dom seq by FUNCT_2:def 1;

then seq . n <> +infty by A3, A4, FUNCT_1:def 3;

hence contradiction by A2, XXREAL_0:4; :: thesis: verum

A6: seq is convergent_to_+infty by A2, Th32;

hence A7: seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = inf seq

now :: thesis: for y being object st y in rng seq holds

y in {+infty}

then
rng seq c= {+infty}
;y in {+infty}

let y be object ; :: thesis: ( y in rng seq implies y in {+infty} )

assume y in rng seq ; :: thesis: y in {+infty}

then ex x being object st

( x in dom seq & seq . x = y ) by FUNCT_1:def 3;

then y = +infty by A2, XXREAL_0:4;

hence y in {+infty} by TARSKI:def 1; :: thesis: verum

end;assume y in rng seq ; :: thesis: y in {+infty}

then ex x being object st

( x in dom seq & seq . x = y ) by FUNCT_1:def 3;

then y = +infty by A2, XXREAL_0:4;

hence y in {+infty} by TARSKI:def 1; :: thesis: verum

then rng seq = {+infty} by A5, XBOOLE_0:def 10;

then inf seq = +infty by XXREAL_2:13;

hence lim seq = inf seq by A6, A7, MESFUNC5:def 12; :: thesis: verum

suppose
not for n being Element of NAT holds +infty <= seq . n
; :: thesis: ( seq is convergent & lim seq = inf seq )

then consider k being Element of NAT such that

A8: seq . k < +infty ;

end;A8: seq . k < +infty ;

per cases
( -infty <> inf seq or -infty = inf seq )
;

end;

suppose A9:
-infty <> inf seq
; :: thesis: ( seq is convergent & lim seq = inf seq )

set seq0 = seq ^\ k;

A10: inf seq = inf (seq ^\ k) by A1, Th25;

A14: inf (rng (seq ^\ k)) is LowerBound of rng (seq ^\ k) by XXREAL_2:def 4;

inf seq <= seq . k by Th23;

then -infty < seq . k by A9, XXREAL_0:2, XXREAL_0:6;

then A15: seq ^\ k is bounded_above by A1, A8, Th30;

then rng (seq ^\ k) is bounded_above ;

then sup (rng (seq ^\ k)) < +infty by A11, XXREAL_0:9, XXREAL_2:57;

then inf (rng (seq ^\ k)) in REAL by A9, A10, A13, XXREAL_0:14;

then rng (seq ^\ k) is bounded_below by A14, XXREAL_2:def 9;

then seq ^\ k is bounded_below ;

then A16: seq ^\ k is bounded by A15;

A17: seq ^\ k is non-increasing by A1, Th25;

then A18: lim (seq ^\ k) = inf (seq ^\ k) by A16, Lm3;

seq ^\ k is convergent by A17, A16, Lm3;

hence ( seq is convergent & lim seq = inf seq ) by A10, A18, Th17; :: thesis: verum

end;A10: inf seq = inf (seq ^\ k) by A1, Th25;

A11: now :: thesis: not rng (seq ^\ k) = {-infty}

A13:
inf (seq ^\ k) <= sup (seq ^\ k)
by Th24;assume
rng (seq ^\ k) = {-infty}
; :: thesis: contradiction

then A12: -infty in rng (seq ^\ k) by TARSKI:def 1;

-infty is LowerBound of rng (seq ^\ k) by XXREAL_2:42;

hence contradiction by A9, A10, A12, XXREAL_2:56; :: thesis: verum

end;then A12: -infty in rng (seq ^\ k) by TARSKI:def 1;

-infty is LowerBound of rng (seq ^\ k) by XXREAL_2:42;

hence contradiction by A9, A10, A12, XXREAL_2:56; :: thesis: verum

A14: inf (rng (seq ^\ k)) is LowerBound of rng (seq ^\ k) by XXREAL_2:def 4;

inf seq <= seq . k by Th23;

then -infty < seq . k by A9, XXREAL_0:2, XXREAL_0:6;

then A15: seq ^\ k is bounded_above by A1, A8, Th30;

then rng (seq ^\ k) is bounded_above ;

then sup (rng (seq ^\ k)) < +infty by A11, XXREAL_0:9, XXREAL_2:57;

then inf (rng (seq ^\ k)) in REAL by A9, A10, A13, XXREAL_0:14;

then rng (seq ^\ k) is bounded_below by A14, XXREAL_2:def 9;

then seq ^\ k is bounded_below ;

then A16: seq ^\ k is bounded by A15;

A17: seq ^\ k is non-increasing by A1, Th25;

then A18: lim (seq ^\ k) = inf (seq ^\ k) by A16, Lm3;

seq ^\ k is convergent by A17, A16, Lm3;

hence ( seq is convergent & lim seq = inf seq ) by A10, A18, Th17; :: thesis: verum

suppose A19:
-infty = inf seq
; :: thesis: ( seq is convergent & lim seq = inf seq )

then
seq is convergent_to_-infty
by A1, Th34;

hence seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = inf seq

thus lim seq = inf seq by A1, A19, Th34; :: thesis: verum

end;hence seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = inf seq

thus lim seq = inf seq by A1, A19, Th34; :: thesis: verum