let n be Nat; :: thesis: for x1, x2 being Element of dyadic (n + 1) st x1 < x2 & not x1 in dyadic n & not x2 in dyadic n holds

((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1))

let x1, x2 be Element of dyadic (n + 1); :: thesis: ( x1 < x2 & not x1 in dyadic n & not x2 in dyadic n implies ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1)) )

assume that

A1: x1 < x2 and

A2: not x1 in dyadic n and

A3: not x2 in dyadic n ; :: thesis: ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1))

consider k2 being Element of NAT such that

A4: ( axis x2 = 2 * k2 or axis x2 = (2 * k2) + 1 ) by SCHEME1:1;

A5: axis x2 <> k2 * 2

A8: ( axis x1 = 2 * k1 or axis x1 = (2 * k1) + 1 ) by SCHEME1:1;

A9: not axis x1 = k1 * 2

then ((k1 * 2) + 1) + (- 1) < ((k2 * 2) + 1) + (- 1) by XREAL_1:6;

then (k1 * 2) / 2 < (k2 * 2) / 2 by XREAL_1:74;

then k1 + 1 <= k2 by NAT_1:13;

then ( 0 < 2 |^ (n + 1) & (k1 + 1) * 2 <= k2 * 2 ) by NEWTON:83, XREAL_1:64;

hence ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1)) by A8, A4, A9, A5, XREAL_1:72; :: thesis: verum

((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1))

let x1, x2 be Element of dyadic (n + 1); :: thesis: ( x1 < x2 & not x1 in dyadic n & not x2 in dyadic n implies ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1)) )

assume that

A1: x1 < x2 and

A2: not x1 in dyadic n and

A3: not x2 in dyadic n ; :: thesis: ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1))

consider k2 being Element of NAT such that

A4: ( axis x2 = 2 * k2 or axis x2 = (2 * k2) + 1 ) by SCHEME1:1;

A5: axis x2 <> k2 * 2

proof

consider k1 being Element of NAT such that
assume A6:
axis x2 = k2 * 2
; :: thesis: contradiction

then x2 = (k2 * 2) / (2 |^ (n + 1)) by Th10;

then A7: x2 = (k2 * 2) / ((2 |^ n) * 2) by NEWTON:6

.= (k2 / (2 |^ n)) * (2 / 2) by XCMPLX_1:76

.= k2 / (2 |^ n) ;

k2 * 2 <= 2 |^ (n + 1) by A6, Th10;

then k2 * 2 <= (2 |^ n) * 2 by NEWTON:6;

then k2 <= ((2 |^ n) * 2) / 2 by XREAL_1:77;

hence contradiction by A3, A7, Def1; :: thesis: verum

end;then x2 = (k2 * 2) / (2 |^ (n + 1)) by Th10;

then A7: x2 = (k2 * 2) / ((2 |^ n) * 2) by NEWTON:6

.= (k2 / (2 |^ n)) * (2 / 2) by XCMPLX_1:76

.= k2 / (2 |^ n) ;

k2 * 2 <= 2 |^ (n + 1) by A6, Th10;

then k2 * 2 <= (2 |^ n) * 2 by NEWTON:6;

then k2 <= ((2 |^ n) * 2) / 2 by XREAL_1:77;

hence contradiction by A3, A7, Def1; :: thesis: verum

A8: ( axis x1 = 2 * k1 or axis x1 = (2 * k1) + 1 ) by SCHEME1:1;

A9: not axis x1 = k1 * 2

proof

then
(k1 * 2) + 1 < (k2 * 2) + 1
by A1, A8, A4, A5, Th14;
assume A10:
axis x1 = k1 * 2
; :: thesis: contradiction

then x1 = (k1 * 2) / (2 |^ (n + 1)) by Th10;

then A11: x1 = (k1 * 2) / ((2 |^ n) * 2) by NEWTON:6

.= (k1 / (2 |^ n)) * (2 / 2) by XCMPLX_1:76

.= k1 / (2 |^ n) ;

k1 * 2 <= 2 |^ (n + 1) by A10, Th10;

then k1 * 2 <= (2 |^ n) * 2 by NEWTON:6;

then k1 <= ((2 |^ n) * 2) / 2 by XREAL_1:77;

hence contradiction by A2, A11, Def1; :: thesis: verum

end;then x1 = (k1 * 2) / (2 |^ (n + 1)) by Th10;

then A11: x1 = (k1 * 2) / ((2 |^ n) * 2) by NEWTON:6

.= (k1 / (2 |^ n)) * (2 / 2) by XCMPLX_1:76

.= k1 / (2 |^ n) ;

k1 * 2 <= 2 |^ (n + 1) by A10, Th10;

then k1 * 2 <= (2 |^ n) * 2 by NEWTON:6;

then k1 <= ((2 |^ n) * 2) / 2 by XREAL_1:77;

hence contradiction by A2, A11, Def1; :: thesis: verum

then ((k1 * 2) + 1) + (- 1) < ((k2 * 2) + 1) + (- 1) by XREAL_1:6;

then (k1 * 2) / 2 < (k2 * 2) / 2 by XREAL_1:74;

then k1 + 1 <= k2 by NAT_1:13;

then ( 0 < 2 |^ (n + 1) & (k1 + 1) * 2 <= k2 * 2 ) by NEWTON:83, XREAL_1:64;

hence ((axis x1) + 1) / (2 |^ (n + 1)) <= ((axis x2) - 1) / (2 |^ (n + 1)) by A8, A4, A9, A5, XREAL_1:72; :: thesis: verum