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