let n be Nat; :: thesis: for x being Real st x in dyadic n holds

( 0 <= x & x <= 1 )

let x be Real; :: thesis: ( x in dyadic n implies ( 0 <= x & x <= 1 ) )

assume x in dyadic n ; :: thesis: ( 0 <= x & x <= 1 )

then consider i being Nat such that

A1: i <= 2 |^ n and

A2: x = i / (2 |^ n) by Def1;

( 0 / (2 |^ n) <= i / (2 |^ n) & i / (2 |^ n) <= (2 |^ n) / (2 |^ n) ) by A1, XREAL_1:72;

hence ( 0 <= x & x <= 1 ) by A2, XCMPLX_1:60; :: thesis: verum

( 0 <= x & x <= 1 )

let x be Real; :: thesis: ( x in dyadic n implies ( 0 <= x & x <= 1 ) )

assume x in dyadic n ; :: thesis: ( 0 <= x & x <= 1 )

then consider i being Nat such that

A1: i <= 2 |^ n and

A2: x = i / (2 |^ n) by Def1;

( 0 / (2 |^ n) <= i / (2 |^ n) & i / (2 |^ n) <= (2 |^ n) / (2 |^ n) ) by A1, XREAL_1:72;

hence ( 0 <= x & x <= 1 ) by A2, XCMPLX_1:60; :: thesis: verum