let n, i be Nat; :: thesis: ( 0 < i & i <= 2 |^ n implies ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) )
assume that
A1: 0 < i and
A2: i <= 2 |^ n ; :: thesis: ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)
0 * 2 < i * 2 by A1, XREAL_1:68;
then consider k being Nat such that
A3: i * 2 = k + 1 by NAT_1:6;
A4: not ((i * 2) - 1) / (2 |^ (n + 1)) in dyadic n
proof
assume ((i * 2) - 1) / (2 |^ (n + 1)) in dyadic n ; :: thesis: contradiction
then consider s being Nat such that
s <= 2 |^ n and
A5: ((i * 2) - 1) / (2 |^ (n + 1)) = s / (2 |^ n) by Def1;
A6: 2 |^ n <> 0 by NEWTON:83;
2 |^ (n + 1) <> 0 by NEWTON:83;
then ((i * 2) - 1) * (2 |^ n) = s * (2 |^ (n + 1)) by A5, A6, XCMPLX_1:95;
then ((i * 2) - 1) * (2 |^ n) = s * ((2 |^ n) * 2) by NEWTON:6;
then ((i * 2) - 1) * (2 |^ n) = (s * 2) * (2 |^ n) ;
then ((i * 2) - 1) / (2 |^ n) = (s * 2) / (2 |^ n) by A6, XCMPLX_1:94;
then (i * 2) + (- 1) = s * 2 by A6, XCMPLX_1:53;
then (2 * i) + 0 = (2 * s) + 1 ;
then 0 = 1 by NAT_1:18;
hence contradiction ; :: thesis: verum
end;
i * 2 <= (2 |^ n) * 2 by A2, XREAL_1:64;
then i * 2 <= 2 |^ (n + 1) by NEWTON:6;
then A7: k <= 2 |^ (n + 1) by A3, NAT_1:13;
((i * 2) - 1) / (2 |^ (n + 1)) in dyadic (n + 1) by A3, A7, Def1;
hence ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) by A4, XBOOLE_0:def 5; :: thesis: verum