let r be Real; :: thesis: for a, b being Real_Sequence st 0 < r & a . 0 <= b . 0 & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) holds
ex c being Real st
( ( for j being Nat holds
( a . j <= c & c <= b . j ) ) & ex k being Nat st
( c - r < a . k & b . k < c + r ) )
let a, b be Real_Sequence; :: thesis: ( 0 < r & a . 0 <= b . 0 & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) implies ex c being Real st
( ( for j being Nat holds
( a . j <= c & c <= b . j ) ) & ex k being Nat st
( c - r < a . k & b . k < c + r ) ) )
assume that
A1: 0 < r and
A2: a . 0 <= b . 0 and
A3: for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ; :: thesis: ex c being Real st
( ( for j being Nat holds
( a . j <= c & c <= b . j ) ) & ex k being Nat st
( c - r < a . k & b . k < c + r ) )
not meet (IntervalSequence (a,b)) is empty by A2, A3, Th32;
then consider y being object such that
A4: y in meet (IntervalSequence (a,b)) ;
A5: y in meet (rng (IntervalSequence (a,b))) by A4, FUNCT_6:def 4;
A6: dom (IntervalSequence (a,b)) = NAT by FUNCT_2:def 1;
set f = IntervalSequence (a,b);
(IntervalSequence (a,b)) . 0 in rng (IntervalSequence (a,b)) by A6, FUNCT_1:3;
then y in (IntervalSequence (a,b)) . 0 by A5, SETFAM_1:def 1;
then A8: y in product <*[.(a . 0),(b . 0).]*> by Def1;
consider g being Function such that
A10: y = g and
dom g = dom <*[.(a . 0),(b . 0).]*> and
for t being object st t in dom <*[.(a . 0),(b . 0).]*> holds
g . t in <*[.(a . 0),(b . 0).]*> . t by A8, CARD_3:def 5;
y is Element of (TOP-REAL 1) by EUCLID:22, A4;
then consider c being Real such that
A11: y = <*c*> by JORDAN2B:20;
take c ; :: thesis: ( ( for j being Nat holds
( a . j <= c & c <= b . j ) ) & ex k being Nat st
( c - r < a . k & b . k < c + r ) )
A12: now :: thesis: for i being Nat holds
( a . i <= c & c <= b . i )
let i be Nat; :: thesis: ( a . i <= c & c <= b . i )
(IntervalSequence (a,b)) . i in rng (IntervalSequence (a,b)) by A6, ORDINAL1:def 12, FUNCT_1:3;
then y in (IntervalSequence (a,b)) . i by A5, SETFAM_1:def 1;
then y in product <*[.(a . i),(b . i).]*> by Def1;
then consider h being Function such that
A13: y = h and
dom h = dom <*[.(a . i),(b . i).]*> and
A14: for t being object st t in dom <*[.(a . i),(b . i).]*> holds
h . t in <*[.(a . i),(b . i).]*> . t by CARD_3:def 5;
A15: dom <*[.(a . i),(b . i).]*> = Seg 1 by FINSEQ_1:def 8;
1 in Seg 1 by TARSKI:def 1, FINSEQ_1:2;
then h . 1 in <*[.(a . i),(b . i).]*> . 1 by A14, A15;
then g . 1 in [.(a . i),(b . i).] by A10, A13, FINSEQ_1:def 8;
then c in [.(a . i),(b . i).] by A10, A11, FINSEQ_1:def 8;
hence ( a . i <= c & c <= b . i ) by XXREAL_1:1; :: thesis: verum
end;
hence for j being Nat holds
( a . j <= c & c <= b . j ) ; :: thesis: ex k being Nat st
( c - r < a . k & b . k < c + r )
thus ex k being Nat st
( c - r < a . k & b . k < c + r ) :: thesis: verum
proof
A16: IntervalSequence (a,b) is SetSequence of (Euclid 1) by Th17;
then A17: for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i ) by A2, A3, Th28;
reconsider S = IntervalSequence (a,b) as non-empty pointwise_bounded closed SetSequence of (Euclid 1) by A17, Th22;
A18: ( diameter S is convergent & lim (diameter S) = 0 ) by A2, A3, Th31;
consider m0 being Nat such that
A19: for l being Nat st m0 <= l holds
|.(((diameter S) . l) - 0).| < r by A1, A18, SEQ_2:def 7;
a . m0 <= b . m0 by A16, A2, A3, Th28;
then (a . m0) - (a . m0) <= (b . m0) - (a . m0) by XREAL_1:9;
then |.((b . m0) - (a . m0)).| = (b . m0) - (a . m0) by ABSVALUE:def 1;
then |.(((diameter S) . m0) - 0).| = (b . m0) - (a . m0) by A2, A3, Th28;
then A20: (b . m0) - (a . m0) < r by A19;
c - (a . m0) <= (b . m0) - (a . m0) by A12, XREAL_1:9;
then A21: c - (a . m0) < r by A20, XXREAL_0:2;
take m0 ; :: thesis: ( c - r < a . m0 & b . m0 < c + r )
(c - (a . m0)) + (a . m0) < r + (a . m0) by A21, XREAL_1:8;
then c - r < ((a . m0) + r) - r by XREAL_1:9;
hence c - r < a . m0 ; :: thesis: b . m0 < c + r
(b . m0) - c <= (b . m0) - (a . m0) by A12, XREAL_1:10;
then (b . m0) - c < r by A20, XXREAL_0:2;
then ((b . m0) - c) + c < r + c by XREAL_1:8;
hence b . m0 < c + r ; :: thesis: verum
end;