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 () . k1 <= a + 1
proof
assume A3: for k1 being Element of NAT holds not () . k1 <= a + 1 ; :: thesis: contradiction
now :: thesis: for x being ExtReal st x in rng () holds
a + 1 <= x
let x be ExtReal; :: thesis: ( x in rng () implies a + 1 <= x )
assume x in rng () ; :: thesis: a + 1 <= x
then ex n being object st
( n in dom () & x = () . n ) by FUNCT_1:def 3;
hence a + 1 <= x by A3; :: thesis: verum
end;
then a + 1 is LowerBound of rng () by XXREAL_2:def 2;
then a + 1 <= a by ;
hence contradiction by XREAL_1:29; :: thesis: verum
end;
then consider k1 being Element of NAT such that
A4: (superior_realsequence seq) . k1 <= a + 1 ;
set K2 = a - 1;
ex k2 being Element of NAT st a - 1 <= () . k2
proof
assume A5: for k2 being Element of NAT holds not a - 1 <= () . k2 ; :: thesis: contradiction
now :: thesis: for x being ExtReal st x in rng () holds
x <= a - 1
let x be ExtReal; :: thesis: ( x in rng () implies x <= a - 1 )
assume x in rng () ; :: thesis: x <= a - 1
then ex n being object st
( n in dom () & x = () . n ) by FUNCT_1:def 3;
hence x <= a - 1 by A5; :: thesis: verum
end;
then a - 1 is UpperBound of rng () by XXREAL_2:def 1;
then a <= a - 1 by XXREAL_2:def 3;
then a + 0 < (a - 1) + 1 by XREAL_1:8;
hence contradiction ; :: thesis: verum
end;
then consider k2 being Element of NAT such that
A6: a - 1 <= () . k2 ;
take k = max (k1,k2); :: thesis: seq ^\ k is bounded
k2 <= k by XXREAL_0:25;
then (inferior_realsequence seq) . k2 <= () . k by Th7;
then A7: a - 1 <= () . k by ;
k1 <= k by XXREAL_0:25;
then (superior_realsequence seq) . k <= () . k1 by Th7;
then A8: (superior_realsequence seq) . k <= a + 1 by ;
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 <= () . k by Th7;
then A12: (superior_realsequence seq) . n <= a + 1 by ;
(inferior_realsequence seq) . k <= () . n by ;
then A13: a - 1 <= () . n by ;
seq . n <= () . n by Th8;
hence ( seq . n <= a + 1 & a - 1 <= seq . n ) by ; :: thesis: verum
end;
now :: thesis: for x being ExtReal st x in rng (seq ^\ k) holds
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 ;
hence x <= a + 1 by ; :: thesis: verum
end;
then a + 1 is UpperBound of rng (seq ^\ k) by XXREAL_2:def 1;
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
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 ;
hence a - 1 <= x by ; :: thesis: verum
end;
then a - 1 is LowerBound of rng (seq ^\ k) by XXREAL_2:def 2;
hence rng (seq ^\ k) is bounded_below by XXREAL_2:def 9; :: according to RINFSUP2:def 3 :: thesis: verum