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

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