let a, b be Real_Sequence; :: thesis: for S being SetSequence of (Euclid 1) st a . 0 <= b . 0 & S = IntervalSequence (a,b) & ( 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
( diameter S is convergent & lim (diameter S) = 0 )
let S be SetSequence of (Euclid 1); :: thesis: ( a . 0 <= b . 0 & S = IntervalSequence (a,b) & ( 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 ( diameter S is convergent & lim (diameter S) = 0 ) )
assume that
A1: a . 0 <= b . 0 and
A2: S = IntervalSequence (a,b) 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: ( diameter S is convergent & lim (diameter S) = 0 )

per cases ( a . 0 = b . 0 or a . 0 < b . 0 ) by A1, XXREAL_0:1;

suppose A4: a . 0 = b . 0 ; :: thesis: ( diameter S is convergent & lim (diameter S) = 0 )

for x, y being object st x in dom (diameter S) & y in dom (diameter S) holds
(diameter S) . x = (diameter S) . y

proof

let x, y be object ; :: thesis: ( x in dom (diameter S) & y in dom (diameter S) implies (diameter S) . x = (diameter S) . y )
assume that
A5: x in dom (diameter S) and
A6: y in dom (diameter S) ; :: thesis: (diameter S) . x = (diameter S) . y
( (diameter S) . x = 0 & (diameter S) . y = 0 ) by A5, A6, A4, A2, A3, Th29;
hence (diameter S) . x = (diameter S) . y ; :: thesis: verum

end;

then A7: diameter S is constant ;
hence diameter S is convergent ; :: thesis: lim (diameter S) = 0
lim (diameter S) = (diameter S) . 0 by A7, SEQ_4:26;
hence lim (diameter S) = 0 by A4, A2, A3, Th29; :: thesis: verum

end;

suppose a . 0 < b . 0 ; :: thesis: ( diameter S is convergent & lim (diameter S) = 0 )

then A8: (a . 0) - (a . 0) < (b . 0) - (a . 0) by XREAL_1:14;
A9: diameter S = b + (- a)

proof

now :: thesis: for i being Nat holds (diameter S) . i = (b . i) + ((- a) . i)

let i be Nat; :: thesis: (diameter S) . i = (b . i) + ((- a) . i)
(- a) . i = - (a . i) by SEQ_1:10;
then (b . i) - (a . i) = (b . i) + ((- a) . i) ;
hence (diameter S) . i = (b . i) + ((- a) . i) by A1, A2, A3, Th28; :: thesis: verum

end;

hence diameter S = b + (- a) by SEQ_1:7; :: thesis: verum

end;

set S2 = diameter S;
A10: for i being Nat holds a . i <= b . i by A1, A3, Th27;
A11: a is non-decreasing by A1, A2, A3, Th28;
b is non-increasing by A1, A2, A3, Th28;
then A12: ( a is convergent & b is convergent ) by A10, A11, Th26;
lim (diameter S) = 0

proof

for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((diameter S) . m) - 0).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((diameter S) . m) - 0).| < p )
assume A13: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((diameter S) . m) - 0).| < p

A14: now :: thesis: ex n0 being Nat st
for m being Nat st n0 <= m holds
((b . 0) - (a . 0)) / (2 to_power m) < p

0 + 1 < (((b . 0) - (a . 0)) / p) + 1 by A13, A8, XREAL_1:8;
then A15: 0 <= log (2,((((b . 0) - (a . 0)) / p) + 1)) by Th2;
reconsider i0 = [/(log (2,((((b . 0) - (a . 0)) / p) + 1)))\] as Integer ;
A16: log (2,((((b . 0) - (a . 0)) / p) + 1)) <= i0 by INT_1:def 7;
then A17: i0 in NAT by A15, INT_1:3;
A18: (log (2,((((b . 0) - (a . 0)) / p) + 1))) + 0 < i0 + 1 by A16, XREAL_1:8;
reconsider n0 = i0 + 1 as Nat by A17;
take n0 = n0; :: thesis: for m being Nat st n0 <= m holds
((b . 0) - (a . 0)) / (2 to_power m) < p
let m be Nat; :: thesis: ( n0 <= m implies ((b . 0) - (a . 0)) / (2 to_power m) < p )
assume A19: n0 <= m ; :: thesis: ((b . 0) - (a . 0)) / (2 to_power m) < p
A20: 0 < 2 to_power n0 by POWER:34;
2 to_power (log (2,((((b . 0) - (a . 0)) / p) + 1))) < 2 to_power n0 by A18, POWER:39;
then A21: (((b . 0) - (a . 0)) / p) + 1 < 2 to_power n0 by A13, A8, POWER:def 3;
((b . 0) - (a . 0)) / p < (((b . 0) - (a . 0)) / p) + 1 by XREAL_1:29;
then ((b . 0) - (a . 0)) / p < 2 to_power n0 by A21, XXREAL_0:2;
then (((b . 0) - (a . 0)) / p) * p < (2 to_power n0) * p by A13, XREAL_1:68;
then (b . 0) - (a . 0) < p * (2 to_power n0) by A13, XCMPLX_1:87;
then ((b . 0) - (a . 0)) / (2 to_power n0) < (p * (2 to_power n0)) / (2 to_power n0) by A20, XREAL_1:74;
then A22: ((b . 0) - (a . 0)) / (2 to_power n0) < p by A20, XCMPLX_1:89;
A23: 2 to_power n0 <= 2 to_power m by A19, NAT_6:1;
0 < 2 to_power n0 by POWER:34;
then ((b . 0) - (a . 0)) / (2 to_power m) <= ((b . 0) - (a . 0)) / (2 to_power n0) by A23, A8, XREAL_1:118;
hence ((b . 0) - (a . 0)) / (2 to_power m) < p by A22, XXREAL_0:2; :: thesis: verum

end;

now :: thesis: ex n0 being Nat st
for m being Nat st n0 <= m holds
|.(((diameter S) . m) - 0).| < p

consider n0 being Nat such that
A24: for m being Nat st n0 <= m holds
((b . 0) - (a . 0)) / (2 to_power m) < p by A14;
take n0 = n0; :: thesis: for m being Nat st n0 <= m holds
|.(((diameter S) . m) - 0).| < p

hereby :: thesis: verum

let m be Nat; :: thesis: ( n0 <= m implies |.(((diameter S) . m) - 0).| < p )
assume A25: n0 <= m ; :: thesis: |.(((diameter S) . m) - 0).| < p
a . m <= b . m by A1, A2, A3, Th28;
then A26: (a . m) - (a . m) <= (b . m) - (a . m) by XREAL_1:9;
(b - a) . m = (b + (- a)) . m by SEQ_1:11
.= (b . m) + ((- a) . m) by SEQ_1:7
.= (b . m) + (- (a . m)) by SEQ_1:10
.= (b . m) - (a . m) ;
then A27: |.(((diameter S) . m) - 0).| = |.((b . m) - (a . m)).| by A9, SEQ_1:11
.= (b . m) - (a . m) by A26, ABSVALUE:def 1 ;
reconsider m0 = m as Element of NAT by ORDINAL1:def 12;
2 |^ m0 is Element of NAT ;
then reconsider r = 2 |^ m as Real ;
r <> 0 by NEWTON:83;
then A28: |.(((diameter S) . m) - 0).| <= ((b . 0) - (a . 0)) / r by A27, Th30, A3;
((b . 0) - (a . 0)) / (2 to_power m) < p by A24, A25;
hence |.(((diameter S) . m) - 0).| < p by A28, XXREAL_0:2; :: thesis: verum

end;

end;

hence ex n being Nat st
for m being Nat st n <= m holds
|.(((diameter S) . m) - 0).| < p ; :: thesis: verum

end;

hence lim (diameter S) = 0 by A12, A9, SEQ_2:def 7; :: thesis: verum

end;

hence ( diameter S is convergent & lim (diameter S) = 0 ) by A12, A9; :: thesis: verum

end;

end;