let seq be Real_Sequence; ( ( 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 )
( seq is convergent implies ( seq is bounded & lim_sup seq = lim_inf seq ) )proof
reconsider r =
lower_bound (superior_realsequence seq) as
real number ;
assume that A1:
seq is
bounded
and A2:
lim_sup seq = lim_inf seq
;
seq is convergent
A3:
inferior_realsequence seq is
bounded
by A1, Th58;
A4:
inferior_realsequence seq is
non-decreasing
by A1, Th52;
A5:
superior_realsequence seq is
non-increasing
by A1, Th53;
A6:
superior_realsequence seq is
bounded
by A1, Th58;
for
s being
real number st
0 < s holds
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
abs ((seq . m) - r) < s
proof
let s be
real number ;
( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < s )
assume A7:
0 < s
;
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < s
consider k2 being
Element of
NAT such that A8:
(superior_realsequence seq) . k2 < r + s
by A6, A7, Th8;
consider k1 being
Element of
NAT such that A9:
r - s < (inferior_realsequence seq) . k1
by A2, A3, A7, Th7;
reconsider k =
max k1,
k2 as
Element of
NAT ;
k2 <= k
by XXREAL_0:25;
then A10:
(superior_realsequence seq) . k <= (superior_realsequence seq) . k2
by A5, SEQM_3:14;
k1 <= k
by XXREAL_0:25;
then A11:
(inferior_realsequence seq) . k1 <= (inferior_realsequence seq) . k
by A4, SEQM_3:12;
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
abs ((seq . m) - r) < s
proof
take
k
;
for m being Element of NAT st k <= m holds
abs ((seq . m) - r) < s
let m be
Element of
NAT ;
( k <= m implies abs ((seq . m) - r) < s )
assume
k <= m
;
abs ((seq . m) - r) < s
then consider k3 being
Nat such that A12:
m = k + k3
by NAT_1:10;
A13:
k3 in NAT
by ORDINAL1:def 13;
then
seq . m <= (superior_realsequence seq) . k
by A1, A12, Th43;
then
seq . m <= (superior_realsequence seq) . k2
by A10, XXREAL_0:2;
then A14:
seq . m < r + s
by A8, XXREAL_0:2;
(inferior_realsequence seq) . k <= seq . m
by A1, A12, A13, Th42;
then
(inferior_realsequence seq) . k1 <= seq . m
by A11, XXREAL_0:2;
then
r - s < seq . m
by A9, XXREAL_0:2;
hence
abs ((seq . m) - r) < s
by A14, Th1;
verum
end;
hence
ex
n being
Element of
NAT st
for
m being
Element of
NAT st
n <= m holds
abs ((seq . m) - r) < s
;
verum
end;
hence
seq is
convergent
by SEQ_2:def 6;
verum
end;
assume A15:
seq is convergent
; ( seq is bounded & lim_sup seq = lim_inf seq )
then consider r being real number such that
A16:
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < p
by SEQ_2:def 6;
A17:
seq is bounded
by A15, SEQ_2:27;
A18:
for p being real number st 0 < p holds
ex n being Element of NAT st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p )
A22:
( superior_realsequence seq is bounded & inferior_realsequence seq is bounded )
by A17, Th58;
A23:
for p being real number st 0 < p holds
( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p )
reconsider r = r as Real by XREAL_0:def 1;
A25:
for p being real number st 0 < p holds
lower_bound (superior_realsequence seq) <= r + p
by A23;
then A26:
lower_bound (superior_realsequence seq) <= r
by XREAL_1:43;
for p being real number st 0 < p holds
r <= (upper_bound (inferior_realsequence seq)) + p
then A27:
r <= upper_bound (inferior_realsequence seq)
by XREAL_1:43;
A28:
upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq)
by A15, Th57, SEQ_2:27;
lower_bound (superior_realsequence seq) <= r
by A25, XREAL_1:43;
then
upper_bound (inferior_realsequence seq) <= r
by A28, XXREAL_0:2;
then
r = upper_bound (inferior_realsequence seq)
by A27, XXREAL_0:1;
hence
( seq is bounded & lim_sup seq = lim_inf seq )
by A15, A28, A26, SEQ_2:27, XXREAL_0:1; verum