let a, b be Real_Sequence; :: thesis: ( ( 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 for i being Nat
for r being Real st r = 2 |^ i & r <> 0 holds
(b . i) - (a . i) <= ((b . 0) - (a . 0)) / r )
assume A1: 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: for i being Nat
for r being Real st r = 2 |^ i & r <> 0 holds
(b . i) - (a . i) <= ((b . 0) - (a . 0)) / r
defpred S1[ object ] means ex i being Nat ex r being Real st
( $1 = i & r = 2 |^ i & r <> 0 & (b . i) - (a . i) <= ((b . 0) - (a . 0)) / r );
A2: S1[ 0 ]
proof
reconsider i0 = 0 as Nat ;
reconsider r0 = 2 |^ 0 as Real ;
take i0 ; :: thesis: ex r being Real st
( 0 = i0 & r = 2 |^ i0 & r <> 0 & (b . i0) - (a . i0) <= ((b . 0) - (a . 0)) / r )
take r0 ; :: thesis: ( 0 = i0 & r0 = 2 |^ i0 & r0 <> 0 & (b . i0) - (a . i0) <= ((b . 0) - (a . 0)) / r0 )
2 |^ 0 = 1 by NEWTON:4;
hence ( 0 = i0 & r0 = 2 |^ i0 & r0 <> 0 & (b . i0) - (a . i0) <= ((b . 0) - (a . 0)) / r0 ) ; :: thesis: verum
end;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then consider i1 being Nat, r1 being Real such that
A4: k = i1 and
A5: r1 = 2 |^ i1 and
r1 <> 0 and
A6: (b . i1) - (a . i1) <= ((b . 0) - (a . 0)) / r1 ;
reconsider i0 = k + 1 as Nat ;
reconsider r0 = 2 |^ (k + 1) as Real ;
A7: r0 <> 0 by NEWTON:87;
(b . i0) - (a . i0) <= ((b . 0) - (a . 0)) / r0
proof
A8: ( ( a . (k + 1) = a . k & b . (k + 1) = ((a . k) + (b . k)) / 2 ) or ( a . (k + 1) = ((a . k) + (b . k)) / 2 & b . (k + 1) = b . k ) ) by A1;
A9: ((b . i1) - (a . i1)) / 2 <= (((b . 0) - (a . 0)) / r1) / 2 by A6, XREAL_1:72;
r1 * 2 = r0 by A4, A5, NEWTON:6;
hence (b . i0) - (a . i0) <= ((b . 0) - (a . 0)) / r0 by A8, A4, XCMPLX_1:78, A9; :: thesis: verum
end;
hence S1[k + 1] by A7; :: thesis: verum
end;
A10: for k being Nat holds S1[k] from NAT_1:sch 2(A2, A3);
 let i be Nat; :: thesis: for r being Real st r = 2 |^ i & r <> 0 holds
(b . i) - (a . i) <= ((b . 0) - (a . 0)) / r
let r be Real; :: thesis: ( r = 2 |^ i & r <> 0 implies (b . i) - (a . i) <= ((b . 0) - (a . 0)) / r )
assume that
A11: r = 2 |^ i and
r <> 0 ; :: thesis: (b . i) - (a . i) <= ((b . 0) - (a . 0)) / r
consider i0 being Nat, r0 being Real such that
A12: i = i0 and
A13: ( r0 = 2 |^ i0 & r0 <> 0 & (b . i0) - (a . i0) <= ((b . 0) - (a . 0)) / r0 ) by A10;
thus (b . i) - (a . i) <= ((b . 0) - (a . 0)) / r by A11, A12, A13; :: thesis: verum