let n, i be Element of 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)
A3: 0 * 2 < i * 2 by A1, XREAL_1:68;
then consider k being Nat such that
A4: i * 2 = k + 1 by NAT_1:6;
A5: 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 Element of NAT such that
s <= 2 |^ n and
A6: ((i * 2) - 1) / (2 |^ (n + 1)) = s / (2 |^ n) by Def3;
A7: 2 |^ n <> 0 by NEWTON:83;
2 |^ (n + 1) <> 0 by NEWTON:83;
then ((i * 2) - 1) * (2 |^ n) = s * (2 |^ (n + 1)) by A6, A7, 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 A7, XCMPLX_1:94;
then (i * 2) + (- 1) = s * 2 by A7, XCMPLX_1:53;
then (2 * i) + 0 = (2 * s) + 1 ;
hence contradiction by NAT_1:18; :: thesis: verum

end;

i * 2 <= (2 |^ n) * 2 by A2, XREAL_1:64;
then i * 2 <= 2 |^ (n + 1) by NEWTON:6;
then A8: k <= 2 |^ (n + 1) by A4, NAT_1:13;
( k in NAT & 0 <= k ) by A3, A4, NAT_1:13, ORDINAL1:def 12;
then ((i * 2) - 1) / (2 |^ (n + 1)) in dyadic (n + 1) by A4, A8, Def3;
hence ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) by A5, XBOOLE_0:def 5; :: thesis: verum