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

proof

reconsider r = lower_bound (superior_realsequence seq) as Real ;
assume that
A1: seq is bounded and
A2: lim_sup seq = lim_inf seq ; :: thesis: seq is convergent
A3: inferior_realsequence seq is bounded by A1, Th56;
A4: inferior_realsequence seq is non-decreasing by A1, Th50;
A5: superior_realsequence seq is non-increasing by A1, Th51;
A6: superior_realsequence seq is bounded by A1, Th56;
for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r).| < s

proof

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r).| < s )
assume A7: 0 < s ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r).| < s
consider k2 being Nat such that
A8: (superior_realsequence seq) . k2 < r + s by A6, A7, Th8;
consider k1 being Nat such that
A9: r - s < (inferior_realsequence seq) . k1 by A2, A3, A7, Th7;
reconsider k = max (k1,k2) as Nat by TARSKI:1;
k2 <= k by XXREAL_0:25;
then A10: (superior_realsequence seq) . k <= (superior_realsequence seq) . k2 by A5, SEQM_3:8;
k1 <= k by XXREAL_0:25;
then A11: (inferior_realsequence seq) . k1 <= (inferior_realsequence seq) . k by A4, SEQM_3:6;
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r).| < s

proof

take k ; :: thesis: for m being Nat st k <= m holds
|.((seq . m) - r).| < s
let m be Nat; :: thesis: ( k <= m implies |.((seq . m) - r).| < s )
assume k <= m ; :: thesis: |.((seq . m) - r).| < s
then consider k3 being Nat such that
A12: m = k + k3 by NAT_1:10;
seq . m <= (superior_realsequence seq) . k by A1, A12, Th41;
then seq . m <= (superior_realsequence seq) . k2 by A10, XXREAL_0:2;
then A13: seq . m < r + s by A8, XXREAL_0:2;
(inferior_realsequence seq) . k <= seq . m by A1, A12, Th40;
then (inferior_realsequence seq) . k1 <= seq . m by A11, XXREAL_0:2;
then r - s < seq . m by A9, XXREAL_0:2;
hence |.((seq . m) - r).| < s by A13, Th1; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r).| < s ; :: thesis: verum

end;

hence seq is convergent by SEQ_2:def 6; :: thesis: verum

end;

assume A14: seq is convergent ; :: thesis: ( seq is bounded & lim_sup seq = lim_inf seq )
then consider r being Real such that
A15: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - r).| < p by SEQ_2:def 6;
A16: seq is bounded by A14;
A17: for p being Real st 0 < p holds
ex n being Nat st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p )

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) )
assume 0 < p ; :: thesis: ex n being Nat st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p )
then consider n being Nat such that
A18: for m being Nat st n <= m holds
|.((seq . m) - r).| < p by A15;
A19: for m being Nat st n <= m holds
( r - p <= seq . m & seq . m <= r + p )

proof

let m be Nat; :: thesis: ( n <= m implies ( r - p <= seq . m & seq . m <= r + p ) )
assume n <= m ; :: thesis: ( r - p <= seq . m & seq . m <= r + p )
then |.((seq . m) - r).| < p by A18;
hence ( r - p <= seq . m & seq . m <= r + p ) by Th1; :: thesis: verum

end;

then for m being Nat st n <= m holds
seq . m <= r + p ;
then A20: (superior_realsequence seq) . n <= r + p by A16, Th45;
for m being Nat st n <= m holds
r - p <= seq . m by A19;
then r - p <= (inferior_realsequence seq) . n by A16, Th43;
hence ex n being Nat st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) by A20; :: thesis: verum

end;

A21: ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by A16, Th56;
A22: for p being Real st 0 < p holds
( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p )

proof

let p be Real; :: thesis: ( 0 < p implies ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) )
assume 0 < p ; :: thesis: ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p )
then consider n being Nat such that
A23: ( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) by A17;
( (inferior_realsequence seq) . n <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= (superior_realsequence seq) . n ) by A21, Th7, Th8;
hence ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) by A23, XXREAL_0:2; :: thesis: verum

end;

reconsider r = r as Real ;
A24: for p being Real st 0 < p holds
lower_bound (superior_realsequence seq) <= r + p by A22;
then A25: lower_bound (superior_realsequence seq) <= r by XREAL_1:41;
for p being Real st 0 < p holds
r <= (upper_bound (inferior_realsequence seq)) + p

proof

let p be Real; :: thesis: ( 0 < p implies r <= (upper_bound (inferior_realsequence seq)) + p )
assume 0 < p ; :: thesis: r <= (upper_bound (inferior_realsequence seq)) + p
then r - p <= upper_bound (inferior_realsequence seq) by A22;
hence r <= (upper_bound (inferior_realsequence seq)) + p by XREAL_1:20; :: thesis: verum

end;

then A26: r <= upper_bound (inferior_realsequence seq) by XREAL_1:41;
A27: upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) by A14, Th55;
lower_bound (superior_realsequence seq) <= r by A24, XREAL_1:41;
then upper_bound (inferior_realsequence seq) <= r by A27, XXREAL_0:2;
then r = upper_bound (inferior_realsequence seq) by A26, XXREAL_0:1;
hence ( seq is bounded & lim_sup seq = lim_inf seq ) by A14, A27, A25, XXREAL_0:1; :: thesis: verum