let i1, i2 be Integer; :: thesis: for n1, n2 being Nat st i1 / (2 |^ n1) < i2 / (2 |^ n2) holds
( i1 / (2 |^ n1) < (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) & (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) <= (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) & (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) < i2 / (2 |^ n2) )
let n1, n2 be Nat; :: thesis: ( i1 / (2 |^ n1) < i2 / (2 |^ n2) implies ( i1 / (2 |^ n1) < (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) & (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) <= (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) & (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) < i2 / (2 |^ n2) ) )
assume i1 / (2 |^ n1) < i2 / (2 |^ n2) ; :: thesis: ( i1 / (2 |^ n1) < (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) & (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) <= (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) & (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) < i2 / (2 |^ n2) )
then (i1 * (2 |^ n2)) + 1 <= i2 * (2 |^ n1) by INT_1:7, XREAL_1:102;
then A1: ((i1 * (2 |^ n2)) + 1) * 2 <= (i2 * (2 |^ n1)) * 2 by XREAL_1:64;
2 |^ ((n1 + n2) + 1) = 2 |^ (n1 + (n2 + 1))
.= (2 |^ n1) * (2 |^ (n2 + 1)) by NEWTON:8
.= (2 |^ n1) * (2 * (2 |^ n2)) by NEWTON:6 ;
then ((i1 * (2 |^ n2)) * 2) / (2 |^ ((n1 + n2) + 1)) = (i1 * ((2 |^ n2) * 2)) / ((2 |^ n1) * (2 * (2 |^ n2)))
.= i1 / (2 |^ n1) by XCMPLX_1:91 ;
hence i1 / (2 |^ n1) < (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) by XREAL_1:29, XREAL_1:74; :: thesis: ( (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) <= (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) & (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) < i2 / (2 |^ n2) )
(((i1 * (2 |^ n2)) * 2) + 1) + 1 <= (i2 * (2 |^ n1)) * 2 by A1;
then ((i1 * (2 |^ n2)) * 2) + 1 <= ((i2 * (2 |^ n1)) * 2) - 1 by XREAL_1:19;
hence (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) <= (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) by XREAL_1:72; :: thesis: (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) < i2 / (2 |^ n2)
A2: ((i2 * (2 |^ n1)) * 2) - 1 < (((i2 * (2 |^ n1)) * 2) - 1) + 1 by XREAL_1:29;
2 |^ ((n1 + n2) + 1) = 2 |^ (n2 + (n1 + 1))
.= (2 |^ n2) * (2 |^ (n1 + 1)) by NEWTON:8
.= (2 |^ n2) * (2 * (2 |^ n1)) by NEWTON:6 ;
then ((i2 * (2 |^ n1)) * 2) / (2 |^ ((n1 + n2) + 1)) = (i2 * ((2 |^ n1) * 2)) / ((2 |^ n2) * (2 * (2 |^ n1)))
.= i2 / (2 |^ n2) by XCMPLX_1:91 ;
hence (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) < i2 / (2 |^ n2) by A2, XREAL_1:74; :: thesis: verum