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 A1: ( 0 < i & i <= 2 |^ n ) ; :: thesis: ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)
then A2: 0 * 2 < i * 2 by XREAL_1:70;
then consider k being Nat such that
A3: i * 2 = k + 1 by NAT_1:6;
A4: k in NAT by ORDINAL1:def 13;
i * 2 <= (2 |^ n) * 2 by A1, XREAL_1:66;
then i * 2 <= 2 |^ (n + 1) by NEWTON:11;
then ( 0 <= k & k <= 2 |^ (n + 1) ) by A2, A3, NAT_1:13;
then A5: ((i * 2) - 1) / (2 |^ (n + 1)) in dyadic (n + 1) by A3, A4, Def3;
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
A6: ( 0 <= s & s <= 2 |^ n & ((i * 2) - 1) / (2 |^ (n + 1)) = s / (2 |^ n) ) by Def3;
A7: ( 2 |^ n <> 0 & 2 |^ (n + 1) <> 0 ) by NEWTON:102;
then ((i * 2) - 1) * (2 |^ n) = s * (2 |^ (n + 1)) by A6, XCMPLX_1:96;
then ((i * 2) - 1) * (2 |^ n) = s * ((2 |^ n) * 2) by NEWTON:11;
then ((i * 2) - 1) * (2 |^ n) = (s * 2) * (2 |^ n) ;
then ((i * 2) - 1) / (2 |^ n) = (s * 2) / (2 |^ n) by A7, XCMPLX_1:95;
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;

hence ((i * 2) - 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) by A5, XBOOLE_0:def 5; :: thesis: verum