let seq be ExtREAL_sequence; :: thesis: ( seq is convergent iff lim_inf seq = lim_sup seq )
set a = lim_inf 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 A5: rseq0 is bounded ;
then lim_sup rseq0 = lim_sup (seq ^\ k) by Th9;
then A6: lim_sup rseq0 = lim_sup seq by Th28;
lim_inf rseq0 = lim_inf (seq ^\ k) by A5, Th10;
then lim_inf rseq0 = lim_inf seq by Th29;
hence lim_inf seq = lim_sup seq by A4, A6, RINFSUP1:88; :: thesis: verum

end;

suppose A7: 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
A8: for m being Nat st n <= m holds
seq . m <= g by A7, MESFUNC5:def 10;

now

let m be Nat; :: thesis: ( n <= m implies (inferior_realsequence seq) . m <= g )
m is Element of NAT by ORDINAL1:def 12;
then A9: (inferior_realsequence seq) . m <= seq . m by Th8;
assume n <= m ; :: thesis: (inferior_realsequence seq) . m <= g
then seq . m <= g by A8;
hence (inferior_realsequence seq) . m <= g by A9, 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 A10: 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 A10, MESFUNC5:def 12;
then A11: lim_inf seq = -infty by Th37;
A12: 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
A13: g < 0 and
A14: 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
A15: for m being Nat st N <= m holds
seq . m <= g by A7, A13, 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 12;
then consider Y being non empty Subset of ExtREAL such that
A16: Y = { (seq . k) where k is Element of NAT : m <= k } and
A17: (superior_realsequence seq) . m = sup Y by Def7;
assume A18: 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
A19: x = seq . k and
A20: m <= k by A16;
N <= k by A18, A20, XXREAL_0:2;
hence x <= g by A15, A19; :: thesis: verum

end;

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

end;

hence contradiction by A14; :: thesis: verum

end;

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

end;

suppose A21: 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
A22: for m being Nat st n <= m holds
g <= seq . m by A21, MESFUNC5:def 9;

now

let m be Nat; :: thesis: ( n <= m implies g <= (superior_realsequence seq) . m )
m is Element of NAT by ORDINAL1:def 12;
then A23: seq . m <= (superior_realsequence seq) . m by Th8;
assume n <= m ; :: thesis: g <= (superior_realsequence seq) . m
then g <= seq . m by A22;
hence g <= (superior_realsequence seq) . m by A23, 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 A24: 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 A24, MESFUNC5:def 12;
then A25: lim_sup seq = +infty by Th36;
A26: 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
A27: 0 < g and
A28: 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
A29: for m being Nat st N <= m holds
g <= seq . m by A21, A27, MESFUNC5:def 9;

now

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

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
A33: x = seq . k and
A34: m <= k by A30;
N <= k by A32, A34, XXREAL_0:2;
hence g <= x by A29, A33; :: thesis: verum

end;

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

end;

hence contradiction by A28; :: thesis: verum

end;

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

end;

end;

end;

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

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 A35, Lm7; :: thesis: verum

end;

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

hence seq is convergent by A35, Lm5; :: thesis: verum

end;

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

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

end;

end;