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
proof
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;
consider k1 being Element of NAT such that
A8: ( axis x1 = 2 * k1 or axis x1 = (2 * k1) + 1 ) by SCHEME1:1;
A9: not axis x1 = k1 * 2
proof
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 (k1 * 2) + 1 < (k2 * 2) + 1 by A1, A8, A4, A5, Th14;
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