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 )

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 A36:
lim_inf seq = lim_sup seq
; :: thesis: seq is convergent
assume A1:
seq is convergent
; :: thesis: lim_inf seq = lim_sup seq

end;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;

end;

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

then consider k being Nat such that

A3: seq ^\ k is bounded by Th19;

reconsider rseq0 = seq ^\ k as Real_Sequence by A3, Th11;

A4: k in NAT by ORDINAL1:def 12;

seq ^\ k is convergent_to_finite_number by A2, Th20;

then A5: rseq0 is convergent by Th15;

then A6: rseq0 is bounded ;

then lim_sup rseq0 = lim_sup (seq ^\ k) by Th9;

then A7: lim_sup rseq0 = lim_sup seq by Th28, A4;

lim_inf rseq0 = lim_inf (seq ^\ k) by A6, Th10;

then lim_inf rseq0 = lim_inf seq by Th29, A4;

hence lim_inf seq = lim_sup seq by A5, A7, RINFSUP1:88; :: thesis: verum

end;A3: seq ^\ k is bounded by Th19;

reconsider rseq0 = seq ^\ k as Real_Sequence by A3, Th11;

A4: k in NAT by ORDINAL1:def 12;

seq ^\ k is convergent_to_finite_number by A2, Th20;

then A5: rseq0 is convergent by Th15;

then A6: rseq0 is bounded ;

then lim_sup rseq0 = lim_sup (seq ^\ k) by Th9;

then A7: lim_sup rseq0 = lim_sup seq by Th28, A4;

lim_inf rseq0 = lim_inf (seq ^\ k) by A6, Th10;

then lim_inf rseq0 = lim_inf seq by Th29, A4;

hence lim_inf seq = lim_sup seq by A5, A7, RINFSUP1:88; :: thesis: verum

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

then inferior_realsequence seq is convergent by MESFUNC5:def 11;

then lim (inferior_realsequence seq) = -infty by A11, MESFUNC5:def 12;

then A12: lim_inf seq = -infty by Th37;

A13: superior_realsequence seq is convergent_to_-infty

then lim (superior_realsequence seq) = -infty by A13, MESFUNC5:def 12;

hence lim_inf seq = lim_sup seq by A12, Th36; :: thesis: verum

end;

now :: thesis: for g being Real st g < 0 holds

ex n being Nat st

for m being Nat st n <= m holds

(inferior_realsequence seq) . m <= g

then A11:
inferior_realsequence seq is convergent_to_-infty
by MESFUNC5:def 10;ex n being Nat st

for m being Nat st n <= m holds

(inferior_realsequence seq) . m <= g

let g be Real; :: 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

A9: for m being Nat st n <= m holds

seq . m <= g by A8, MESFUNC5:def 10;

for m being Nat st n <= m holds

(inferior_realsequence seq) . m <= g ; :: thesis: verum

end;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

A9: for m being Nat st n <= m holds

seq . m <= g by A8, MESFUNC5:def 10;

now :: thesis: for m being Nat st n <= m holds

(inferior_realsequence seq) . m <= g

hence
ex n being Nat st (inferior_realsequence seq) . m <= g

let m be Nat; :: thesis: ( n <= m implies (inferior_realsequence seq) . m <= g )

A10: (inferior_realsequence seq) . m <= seq . m by Th8;

assume n <= m ; :: thesis: (inferior_realsequence seq) . m <= g

then seq . m <= g by A9;

hence (inferior_realsequence seq) . m <= g by A10, XXREAL_0:2; :: thesis: verum

end;A10: (inferior_realsequence seq) . m <= seq . m by Th8;

assume n <= m ; :: thesis: (inferior_realsequence seq) . m <= g

then seq . m <= g by A9;

hence (inferior_realsequence seq) . m <= g by A10, XXREAL_0:2; :: thesis: verum

for m being Nat st n <= m holds

(inferior_realsequence seq) . m <= g ; :: thesis: verum

then inferior_realsequence seq is convergent by MESFUNC5:def 11;

then lim (inferior_realsequence seq) = -infty by A11, MESFUNC5:def 12;

then A12: lim_inf seq = -infty by Th37;

A13: superior_realsequence seq is convergent_to_-infty

proof

then
superior_realsequence seq is convergent
by MESFUNC5:def 11;
set iseq = superior_realsequence seq;

assume not superior_realsequence seq is convergent_to_-infty ; :: thesis: contradiction

then consider g being Real such that

A14: g < 0 and

A15: 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

A16: for m being Nat st N <= m holds

seq . m <= g by A8, A14, MESFUNC5:def 10;

end;assume not superior_realsequence seq is convergent_to_-infty ; :: thesis: contradiction

then consider g being Real such that

A14: g < 0 and

A15: 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

A16: for m being Nat st N <= m holds

seq . m <= g by A8, A14, MESFUNC5:def 10;

now :: thesis: for m being Nat st N <= m holds

(superior_realsequence seq) . m <= g

hence
contradiction
by A15; :: thesis: verum(superior_realsequence seq) . m <= g

let m be Nat; :: thesis: ( N <= m implies (superior_realsequence seq) . m <= g )

consider Y being non empty Subset of ExtREAL such that

A17: Y = { (seq . k) where k is Nat : m <= k } and

A18: (superior_realsequence seq) . m = sup Y by Def7;

assume A19: N <= m ; :: thesis: (superior_realsequence seq) . m <= g

hence (superior_realsequence seq) . m <= g by A18, XXREAL_2:def 3; :: thesis: verum

end;consider Y being non empty Subset of ExtREAL such that

A17: Y = { (seq . k) where k is Nat : m <= k } and

A18: (superior_realsequence seq) . m = sup Y by Def7;

assume A19: N <= m ; :: thesis: (superior_realsequence seq) . m <= g

now :: thesis: for x being ExtReal st x in Y holds

x <= g

then
g is UpperBound of Y
by XXREAL_2:def 1;x <= g

let x be ExtReal; :: thesis: ( x in Y implies x <= g )

assume x in Y ; :: thesis: x <= g

then consider k being Nat such that

A20: x = seq . k and

A21: m <= k by A17;

N <= k by A19, A21, XXREAL_0:2;

hence x <= g by A16, A20; :: thesis: verum

end;assume x in Y ; :: thesis: x <= g

then consider k being Nat such that

A20: x = seq . k and

A21: m <= k by A17;

N <= k by A19, A21, XXREAL_0:2;

hence x <= g by A16, A20; :: thesis: verum

hence (superior_realsequence seq) . m <= g by A18, XXREAL_2:def 3; :: thesis: verum

then lim (superior_realsequence seq) = -infty by A13, MESFUNC5:def 12;

hence lim_inf seq = lim_sup seq by A12, Th36; :: thesis: verum

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

then superior_realsequence seq is convergent by MESFUNC5:def 11;

then lim (superior_realsequence seq) = +infty by A25, MESFUNC5:def 12;

then A26: lim_sup seq = +infty by Th36;

A27: inferior_realsequence seq is convergent_to_+infty

then lim (inferior_realsequence seq) = +infty by A27, MESFUNC5:def 12;

hence lim_inf seq = lim_sup seq by A26, Th37; :: thesis: verum

end;

now :: thesis: for g being Real st 0 < g holds

ex n being Nat st

for m being Nat st n <= m holds

g <= (superior_realsequence seq) . m

then A25:
superior_realsequence seq is convergent_to_+infty
by MESFUNC5:def 9;ex n being Nat st

for m being Nat st n <= m holds

g <= (superior_realsequence seq) . m

let g be Real; :: 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

A23: for m being Nat st n <= m holds

g <= seq . m by A22, MESFUNC5:def 9;

for m being Nat st n <= m holds

g <= (superior_realsequence seq) . m ; :: thesis: verum

end;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

A23: for m being Nat st n <= m holds

g <= seq . m by A22, MESFUNC5:def 9;

now :: thesis: for m being Nat st n <= m holds

g <= (superior_realsequence seq) . m

hence
ex n being Nat st g <= (superior_realsequence seq) . m

let m be Nat; :: thesis: ( n <= m implies g <= (superior_realsequence seq) . m )

A24: seq . m <= (superior_realsequence seq) . m by Th8;

assume n <= m ; :: thesis: g <= (superior_realsequence seq) . m

then g <= seq . m by A23;

hence g <= (superior_realsequence seq) . m by A24, XXREAL_0:2; :: thesis: verum

end;A24: seq . m <= (superior_realsequence seq) . m by Th8;

assume n <= m ; :: thesis: g <= (superior_realsequence seq) . m

then g <= seq . m by A23;

hence g <= (superior_realsequence seq) . m by A24, XXREAL_0:2; :: thesis: verum

for m being Nat st n <= m holds

g <= (superior_realsequence seq) . m ; :: thesis: verum

then superior_realsequence seq is convergent by MESFUNC5:def 11;

then lim (superior_realsequence seq) = +infty by A25, MESFUNC5:def 12;

then A26: lim_sup seq = +infty by Th36;

A27: inferior_realsequence seq is convergent_to_+infty

proof

then
inferior_realsequence seq is convergent
by MESFUNC5:def 11;
set iseq = inferior_realsequence seq;

assume not inferior_realsequence seq is convergent_to_+infty ; :: thesis: contradiction

then consider g being Real such that

A28: 0 < g and

A29: 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

A30: for m being Nat st N <= m holds

g <= seq . m by A22, A28, MESFUNC5:def 9;

end;assume not inferior_realsequence seq is convergent_to_+infty ; :: thesis: contradiction

then consider g being Real such that

A28: 0 < g and

A29: 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

A30: for m being Nat st N <= m holds

g <= seq . m by A22, A28, MESFUNC5:def 9;

now :: thesis: for m being Nat st N <= m holds

g <= (inferior_realsequence seq) . m

hence
contradiction
by A29; :: thesis: verumg <= (inferior_realsequence seq) . m

let m be Nat; :: thesis: ( N <= m implies g <= (inferior_realsequence seq) . m )

consider Y being non empty Subset of ExtREAL such that

A31: Y = { (seq . k) where k is Nat : m <= k } and

A32: (inferior_realsequence seq) . m = inf Y by Def6;

assume A33: N <= m ; :: thesis: g <= (inferior_realsequence seq) . m

hence g <= (inferior_realsequence seq) . m by A32, XXREAL_2:def 4; :: thesis: verum

end;consider Y being non empty Subset of ExtREAL such that

A31: Y = { (seq . k) where k is Nat : m <= k } and

A32: (inferior_realsequence seq) . m = inf Y by Def6;

assume A33: N <= m ; :: thesis: g <= (inferior_realsequence seq) . m

now :: thesis: for x being ExtReal st x in Y holds

g <= x

then
g is LowerBound of Y
by XXREAL_2:def 2;g <= x

let x be ExtReal; :: thesis: ( x in Y implies g <= x )

assume x in Y ; :: thesis: g <= x

then consider k being Nat such that

A34: x = seq . k and

A35: m <= k by A31;

N <= k by A33, A35, XXREAL_0:2;

hence g <= x by A30, A34; :: thesis: verum

end;assume x in Y ; :: thesis: g <= x

then consider k being Nat such that

A34: x = seq . k and

A35: m <= k by A31;

N <= k by A33, A35, XXREAL_0:2;

hence g <= x by A30, A34; :: thesis: verum

hence g <= (inferior_realsequence seq) . m by A32, XXREAL_2:def 4; :: thesis: verum

then lim (inferior_realsequence seq) = +infty by A27, MESFUNC5:def 12;

hence lim_inf seq = lim_sup seq by A26, Th37; :: thesis: verum

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

end;