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