let seq be ExtREAL_sequence; :: thesis: ( seq is convergent iff lim_inf seq = lim_sup seq )
thus ( seq is convergent implies lim_inf seq = lim_sup seq ) :: thesis: ( lim_inf seq = lim_sup seq implies seq is convergent )

proof

assume A1: seq is convergent ; :: thesis: lim_inf seq = lim_sup seq

per cases ( seq is convergent_to_finite_number or seq is convergent_to_-infty or seq is convergent_to_+infty ) by A1, MESFUNC5:def 11;

suppose A2: seq is convergent_to_finite_number ; :: thesis: lim_inf seq = lim_sup seq

then consider k being Element of NAT such that
A3: seq ^\ k is bounded by Th19;
reconsider rseq0 = seq ^\ k as Real_Sequence by A3, Th11;
seq ^\ k is convergent_to_finite_number by A2, Th20;
then A4: rseq0 is convergent by Th15;
then rseq0 is bounded by RINFSUP1:90;
then ( lim_inf rseq0 = lim_inf (seq ^\ k) & lim_sup rseq0 = lim_sup (seq ^\ k) ) by Th9, Th10;
then ( lim_inf rseq0 = lim_inf seq & lim_sup rseq0 = lim_sup seq ) by Th28, Th29;
hence lim_inf seq = lim_sup seq by A4, RINFSUP1:90; :: thesis: verum

end;

suppose A5: seq is convergent_to_-infty ; :: thesis: lim_inf seq = lim_sup seq

now

let g be real number ; :: thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
(inferior_realsequence seq) . m <= g )
assume g < 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
(inferior_realsequence seq) . m <= g
then consider n being Nat such that
A6: for m being Nat st n <= m holds
seq . m <= g by A5, MESFUNC5:def 10;

now

let m be Nat; :: thesis: ( n <= m implies (inferior_realsequence seq) . m <= g )
assume n <= m ; :: thesis: (inferior_realsequence seq) . m <= g
then A7: seq . m <= g by A6;
m is Element of NAT by ORDINAL1:def 13;
then (inferior_realsequence seq) . m <= seq . m by Th8;
hence (inferior_realsequence seq) . m <= g by A7, XXREAL_0:2; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
(inferior_realsequence seq) . m <= g ; :: thesis: verum

end;

then A8: inferior_realsequence seq is convergent_to_-infty by MESFUNC5:def 10;
then inferior_realsequence seq is convergent by MESFUNC5:def 11;
then lim (inferior_realsequence seq) = -infty by A8, MESFUNC5:def 12;
then A9: lim_inf seq = -infty by Th37;
A10: superior_realsequence seq is convergent_to_-infty

proof

set iseq = superior_realsequence seq;
assume not superior_realsequence seq is convergent_to_-infty ; :: thesis: contradiction
then consider g being real number such that
A11: ( g < 0 & ( for n being Nat ex m being Nat st
( n <= m & g < (superior_realsequence seq) . m ) ) ) by MESFUNC5:def 10;
consider N being Nat such that
A12: for m being Nat st N <= m holds
seq . m <= g by A5, A11, MESFUNC5:def 10;

now

let m be Nat; :: thesis: ( N <= m implies (superior_realsequence seq) . m <= g )
m is Element of NAT by ORDINAL1:def 13;
then consider Y being non empty Subset of ExtREAL such that
A13: ( Y = { (seq . k) where k is Element of NAT : m <= k } & (superior_realsequence seq) . m = sup Y ) by Def7;
assume A14: N <= m ; :: thesis: (superior_realsequence seq) . m <= g

now

let x be ext-real number ; :: thesis: ( x in Y implies x <= g )
assume x in Y ; :: thesis: x <= g
then consider k being Element of NAT such that
A15: ( x = seq . k & m <= k ) by A13;
N <= k by A14, A15, XXREAL_0:2;
hence x <= g by A12, A15; :: thesis: verum

end;

then g is UpperBound of Y by XXREAL_2:def 1;
hence (superior_realsequence seq) . m <= g by A13, XXREAL_2:def 3; :: thesis: verum

end;

hence contradiction by A11; :: thesis: verum

end;

then superior_realsequence seq is convergent by MESFUNC5:def 11;
then lim (superior_realsequence seq) = -infty by A10, MESFUNC5:def 12;
hence lim_inf seq = lim_sup seq by A9, Th36; :: thesis: verum

end;

suppose A16: seq is convergent_to_+infty ; :: thesis: lim_inf seq = lim_sup seq

now

let g be real number ; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= (superior_realsequence seq) . m )
assume 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= (superior_realsequence seq) . m
then consider n being Nat such that
A17: for m being Nat st n <= m holds
g <= seq . m by A16, MESFUNC5:def 9;

now

let m be Nat; :: thesis: ( n <= m implies g <= (superior_realsequence seq) . m )
assume n <= m ; :: thesis: g <= (superior_realsequence seq) . m
then A18: g <= seq . m by A17;
m is Element of NAT by ORDINAL1:def 13;
then seq . m <= (superior_realsequence seq) . m by Th8;
hence g <= (superior_realsequence seq) . m by A18, XXREAL_0:2; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
g <= (superior_realsequence seq) . m ; :: thesis: verum

end;

then A19: superior_realsequence seq is convergent_to_+infty by MESFUNC5:def 9;
then superior_realsequence seq is convergent by MESFUNC5:def 11;
then lim (superior_realsequence seq) = +infty by A19, MESFUNC5:def 12;
then A20: lim_sup seq = +infty by Th36;
A21: inferior_realsequence seq is convergent_to_+infty

proof

set iseq = inferior_realsequence seq;
assume not inferior_realsequence seq is convergent_to_+infty ; :: thesis: contradiction
then consider g being real number such that
A22: ( 0 < g & ( for n being Nat ex m being Nat st
( n <= m & (inferior_realsequence seq) . m < g ) ) ) by MESFUNC5:def 9;
consider N being Nat such that
A23: for m being Nat st N <= m holds
g <= seq . m by A16, A22, MESFUNC5:def 9;

now

let m be Nat; :: thesis: ( N <= m implies g <= (inferior_realsequence seq) . m )
assume A24: N <= m ; :: thesis: g <= (inferior_realsequence seq) . m
m is Element of NAT by ORDINAL1:def 13;
then consider Y being non empty Subset of ExtREAL such that
A25: ( Y = { (seq . k) where k is Element of NAT : m <= k } & (inferior_realsequence seq) . m = inf Y ) by Def6;

now

let x be ext-real number ; :: thesis: ( x in Y implies g <= x )
assume x in Y ; :: thesis: g <= x
then consider k being Element of NAT such that
A26: ( x = seq . k & m <= k ) by A25;
N <= k by A24, A26, XXREAL_0:2;
hence g <= x by A23, A26; :: thesis: verum

end;

then g is LowerBound of Y by XXREAL_2:def 2;
hence g <= (inferior_realsequence seq) . m by A25, XXREAL_2:def 4; :: thesis: verum

end;

hence contradiction by A22; :: thesis: verum

end;

then inferior_realsequence seq is convergent by MESFUNC5:def 11;
then lim (inferior_realsequence seq) = +infty by A21, MESFUNC5:def 12;
hence lim_inf seq = lim_sup seq by A20, Th37; :: thesis: verum

end;

end;

end;

assume A27: lim_inf seq = lim_sup seq ; :: thesis: seq is convergent
set a = lim_inf seq;

per cases ( lim_inf seq in REAL or lim_inf seq = +infty or lim_inf seq = -infty ) by XXREAL_0:14;

suppose lim_inf seq in REAL ; :: thesis: seq is convergent

hence seq is convergent by A27, Lm8; :: thesis: verum

end;

suppose lim_inf seq = +infty ; :: thesis: seq is convergent

hence seq is convergent by A27, Lm6; :: thesis: verum

end;

suppose lim_inf seq = -infty ; :: thesis: seq is convergent

hence seq is convergent by A27, Lm7; :: thesis: verum

end;

end;