let n be Element of 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,(n + 1)) + 1) / (2 |^ (n + 1)) <= ((axis x2,(n + 1)) - 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,(n + 1)) + 1) / (2 |^ (n + 1)) <= ((axis x2,(n + 1)) - 1) / (2 |^ (n + 1)) )
assume A1: ( x1 < x2 & not x1 in dyadic n & not x2 in dyadic n ) ; :: thesis: ((axis x1,(n + 1)) + 1) / (2 |^ (n + 1)) <= ((axis x2,(n + 1)) - 1) / (2 |^ (n + 1))
consider k1 being Element of NAT such that
A2: ( axis x1,(n + 1) = 2 * k1 or axis x1,(n + 1) = (2 * k1) + 1 ) by SCHEME1:1;
consider k2 being Element of NAT such that
A3: ( axis x2,(n + 1) = 2 * k2 or axis x2,(n + 1) = (2 * k2) + 1 ) by SCHEME1:1;
A4: not axis x1,(n + 1) = k1 * 2

proof

assume axis x1,(n + 1) = k1 * 2 ; :: thesis: contradiction
then A5: ( x1 = (k1 * 2) / (2 |^ (n + 1)) & 0 <= k1 * 2 & k1 * 2 <= 2 |^ (n + 1) ) by Th16, NAT_1:2;
then A6: x1 = (k1 * 2) / ((2 |^ n) * 2) by NEWTON:11
.= (k1 / (2 |^ n)) * (2 / 2) by XCMPLX_1:77
.= k1 / (2 |^ n) ;
k1 * 2 <= (2 |^ n) * 2 by A5, NEWTON:11;
then k1 <= ((2 |^ n) * 2) / 2 by XREAL_1:79;
then ( 0 <= k1 & k1 <= 2 |^ n ) by NAT_1:2;
hence contradiction by A1, A6, Def3; :: thesis: verum

end;

A7: axis x2,(n + 1) <> k2 * 2

proof

assume axis x2,(n + 1) = k2 * 2 ; :: thesis: contradiction
then A8: ( x2 = (k2 * 2) / (2 |^ (n + 1)) & 0 <= k2 * 2 & k2 * 2 <= 2 |^ (n + 1) ) by Th16, NAT_1:2;
then A9: x2 = (k2 * 2) / ((2 |^ n) * 2) by NEWTON:11
.= (k2 / (2 |^ n)) * (2 / 2) by XCMPLX_1:77
.= k2 / (2 |^ n) ;
k2 * 2 <= (2 |^ n) * 2 by A8, NEWTON:11;
then k2 <= ((2 |^ n) * 2) / 2 by XREAL_1:79;
then ( 0 <= k2 & k2 <= 2 |^ n ) by NAT_1:2;
hence contradiction by A1, A9, Def3; :: thesis: verum

end;

A10: ( 2 |^ n <> 0 & 0 < 2 |^ (n + 1) ) by NEWTON:102;
(k1 * 2) + 1 < (k2 * 2) + 1 by A1, A2, A3, A4, A7, Th21;
then ( ((k1 * 2) + 1) + (- 1) < ((k2 * 2) + 1) + (- 1) & ((k1 * 2) + 1) + (- 1) = (k1 * 2) + (1 + (- 1)) & ((k2 * 2) + 1) + (- 1) = (k2 * 2) + (1 + (- 1)) ) by XREAL_1:8;
then ( (k1 * 2) / 2 < (k2 * 2) / 2 & (k1 * 2) / 2 = k1 * (2 / 2) & (k2 * 2) / 2 = k2 * (2 / 2) ) by XREAL_1:76;
then k1 + 1 <= k2 by NAT_1:13;
then (k1 + 1) * 2 <= k2 * 2 by XREAL_1:66;
hence ((axis x1,(n + 1)) + 1) / (2 |^ (n + 1)) <= ((axis x2,(n + 1)) - 1) / (2 |^ (n + 1)) by A2, A3, A4, A7, A10, XREAL_1:74; :: thesis: verum