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

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

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

i * 2 <= (2 |^ n) * 2
by A2, XREAL_1:64;
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;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

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