let seq be ExtREAL_sequence; :: thesis: ( lim_sup seq = lim_inf seq & lim_inf seq in REAL implies ex k being Nat st seq ^\ k is bounded )

assume that

A1: lim_sup seq = lim_inf seq and

A2: lim_inf seq in REAL ; :: thesis: ex k being Nat st seq ^\ k is bounded

reconsider a = lim_inf seq as Real by A2;

set K1 = a + 1;

ex k1 being Element of NAT st (superior_realsequence seq) . k1 <= a + 1

A4: (superior_realsequence seq) . k1 <= a + 1 ;

set K2 = a - 1;

ex k2 being Element of NAT st a - 1 <= (inferior_realsequence seq) . k2

A6: a - 1 <= (inferior_realsequence seq) . k2 ;

take k = max (k1,k2); :: thesis: seq ^\ k is bounded

k2 <= k by XXREAL_0:25;

then (inferior_realsequence seq) . k2 <= (inferior_realsequence seq) . k by Th7;

then A7: a - 1 <= (inferior_realsequence seq) . k by A6, XXREAL_0:2;

k1 <= k by XXREAL_0:25;

then (superior_realsequence seq) . k <= (superior_realsequence seq) . k1 by Th7;

then A8: (superior_realsequence seq) . k <= a + 1 by A4, XXREAL_0:2;

A9: for n being Element of NAT st k <= n holds

( seq . n <= a + 1 & a - 1 <= seq . n )

hence rng (seq ^\ k) is bounded_above by XXREAL_2:def 10; :: according to RINFSUP2:def 4,RINFSUP2:def 5 :: thesis: seq ^\ k is bounded_below

hence rng (seq ^\ k) is bounded_below by XXREAL_2:def 9; :: according to RINFSUP2:def 3 :: thesis: verum

assume that

A1: lim_sup seq = lim_inf seq and

A2: lim_inf seq in REAL ; :: thesis: ex k being Nat st seq ^\ k is bounded

reconsider a = lim_inf seq as Real by A2;

set K1 = a + 1;

ex k1 being Element of NAT st (superior_realsequence seq) . k1 <= a + 1

proof

then consider k1 being Element of NAT such that
assume A3:
for k1 being Element of NAT holds not (superior_realsequence seq) . k1 <= a + 1
; :: thesis: contradiction

then a + 1 <= a by A1, XXREAL_2:def 4;

hence contradiction by XREAL_1:29; :: thesis: verum

end;now :: thesis: for x being ExtReal st x in rng (superior_realsequence seq) holds

a + 1 <= x

then
a + 1 is LowerBound of rng (superior_realsequence seq)
by XXREAL_2:def 2;a + 1 <= x

let x be ExtReal; :: thesis: ( x in rng (superior_realsequence seq) implies a + 1 <= x )

assume x in rng (superior_realsequence seq) ; :: thesis: a + 1 <= x

then ex n being object st

( n in dom (superior_realsequence seq) & x = (superior_realsequence seq) . n ) by FUNCT_1:def 3;

hence a + 1 <= x by A3; :: thesis: verum

end;assume x in rng (superior_realsequence seq) ; :: thesis: a + 1 <= x

then ex n being object st

( n in dom (superior_realsequence seq) & x = (superior_realsequence seq) . n ) by FUNCT_1:def 3;

hence a + 1 <= x by A3; :: thesis: verum

then a + 1 <= a by A1, XXREAL_2:def 4;

hence contradiction by XREAL_1:29; :: thesis: verum

A4: (superior_realsequence seq) . k1 <= a + 1 ;

set K2 = a - 1;

ex k2 being Element of NAT st a - 1 <= (inferior_realsequence seq) . k2

proof

then consider k2 being Element of NAT such that
assume A5:
for k2 being Element of NAT holds not a - 1 <= (inferior_realsequence seq) . k2
; :: thesis: contradiction

then a <= a - 1 by XXREAL_2:def 3;

then a + 0 < (a - 1) + 1 by XREAL_1:8;

hence contradiction ; :: thesis: verum

end;now :: thesis: for x being ExtReal st x in rng (inferior_realsequence seq) holds

x <= a - 1

then
a - 1 is UpperBound of rng (inferior_realsequence seq)
by XXREAL_2:def 1;x <= a - 1

let x be ExtReal; :: thesis: ( x in rng (inferior_realsequence seq) implies x <= a - 1 )

assume x in rng (inferior_realsequence seq) ; :: thesis: x <= a - 1

then ex n being object st

( n in dom (inferior_realsequence seq) & x = (inferior_realsequence seq) . n ) by FUNCT_1:def 3;

hence x <= a - 1 by A5; :: thesis: verum

end;assume x in rng (inferior_realsequence seq) ; :: thesis: x <= a - 1

then ex n being object st

( n in dom (inferior_realsequence seq) & x = (inferior_realsequence seq) . n ) by FUNCT_1:def 3;

hence x <= a - 1 by A5; :: thesis: verum

then a <= a - 1 by XXREAL_2:def 3;

then a + 0 < (a - 1) + 1 by XREAL_1:8;

hence contradiction ; :: thesis: verum

A6: a - 1 <= (inferior_realsequence seq) . k2 ;

take k = max (k1,k2); :: thesis: seq ^\ k is bounded

k2 <= k by XXREAL_0:25;

then (inferior_realsequence seq) . k2 <= (inferior_realsequence seq) . k by Th7;

then A7: a - 1 <= (inferior_realsequence seq) . k by A6, XXREAL_0:2;

k1 <= k by XXREAL_0:25;

then (superior_realsequence seq) . k <= (superior_realsequence seq) . k1 by Th7;

then A8: (superior_realsequence seq) . k <= a + 1 by A4, XXREAL_0:2;

A9: for n being Element of NAT st k <= n holds

( seq . n <= a + 1 & a - 1 <= seq . n )

proof

let n be Element of NAT ; :: thesis: ( k <= n implies ( seq . n <= a + 1 & a - 1 <= seq . n ) )

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

assume A11: k <= n ; :: thesis: ( seq . n <= a + 1 & a - 1 <= seq . n )

then (superior_realsequence seq) . n <= (superior_realsequence seq) . k by Th7;

then A12: (superior_realsequence seq) . n <= a + 1 by A8, XXREAL_0:2;

(inferior_realsequence seq) . k <= (inferior_realsequence seq) . n by A11, Th7;

then A13: a - 1 <= (inferior_realsequence seq) . n by A7, XXREAL_0:2;

seq . n <= (superior_realsequence seq) . n by Th8;

hence ( seq . n <= a + 1 & a - 1 <= seq . n ) by A12, A13, A10, XXREAL_0:2; :: thesis: verum

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

assume A11: k <= n ; :: thesis: ( seq . n <= a + 1 & a - 1 <= seq . n )

then (superior_realsequence seq) . n <= (superior_realsequence seq) . k by Th7;

then A12: (superior_realsequence seq) . n <= a + 1 by A8, XXREAL_0:2;

(inferior_realsequence seq) . k <= (inferior_realsequence seq) . n by A11, Th7;

then A13: a - 1 <= (inferior_realsequence seq) . n by A7, XXREAL_0:2;

seq . n <= (superior_realsequence seq) . n by Th8;

hence ( seq . n <= a + 1 & a - 1 <= seq . n ) by A12, A13, A10, XXREAL_0:2; :: thesis: verum

now :: thesis: for x being ExtReal st x in rng (seq ^\ k) holds

x <= a + 1

then
a + 1 is UpperBound of rng (seq ^\ k)
by XXREAL_2:def 1;x <= a + 1

let x be ExtReal; :: thesis: ( x in rng (seq ^\ k) implies x <= a + 1 )

assume x in rng (seq ^\ k) ; :: thesis: x <= a + 1

then consider n being object such that

A14: n in dom (seq ^\ k) and

A15: x = (seq ^\ k) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A14;

A16: k <= n + k by NAT_1:11;

x = seq . (n + k) by A15, NAT_1:def 3;

hence x <= a + 1 by A9, A16; :: thesis: verum

end;assume x in rng (seq ^\ k) ; :: thesis: x <= a + 1

then consider n being object such that

A14: n in dom (seq ^\ k) and

A15: x = (seq ^\ k) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A14;

A16: k <= n + k by NAT_1:11;

x = seq . (n + k) by A15, NAT_1:def 3;

hence x <= a + 1 by A9, A16; :: thesis: verum

hence rng (seq ^\ k) is bounded_above by XXREAL_2:def 10; :: according to RINFSUP2:def 4,RINFSUP2:def 5 :: thesis: seq ^\ k is bounded_below

now :: thesis: for x being ExtReal st x in rng (seq ^\ k) holds

a - 1 <= x

then
a - 1 is LowerBound of rng (seq ^\ k)
by XXREAL_2:def 2;a - 1 <= x

let x be ExtReal; :: thesis: ( x in rng (seq ^\ k) implies a - 1 <= x )

assume x in rng (seq ^\ k) ; :: thesis: a - 1 <= x

then consider n being object such that

A17: n in dom (seq ^\ k) and

A18: x = (seq ^\ k) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A17;

A19: k <= n + k by NAT_1:11;

x = seq . (n + k) by A18, NAT_1:def 3;

hence a - 1 <= x by A9, A19; :: thesis: verum

end;assume x in rng (seq ^\ k) ; :: thesis: a - 1 <= x

then consider n being object such that

A17: n in dom (seq ^\ k) and

A18: x = (seq ^\ k) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A17;

A19: k <= n + k by NAT_1:11;

x = seq . (n + k) by A18, NAT_1:def 3;

hence a - 1 <= x by A9, A19; :: thesis: verum

hence rng (seq ^\ k) is bounded_below by XXREAL_2:def 9; :: according to RINFSUP2:def 3 :: thesis: verum