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
0 <= i and
A1: i < 2 |^ n ; :: thesis: ((i * 2) + 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n)
A2: 0 + 1 <= i + 1 by XREAL_1:6;
consider s being Nat such that
A3: s = i + 1 ;
A4: (s * 2) - 1 = (i * 2) + (1 + 0) by A3;
s <= 2 |^ n by A1, A3, NAT_1:13;
hence ((i * 2) + 1) / (2 |^ (n + 1)) in (dyadic (n + 1)) \ (dyadic n) by A2, A4, Th7; :: thesis: verum