let n be Element of 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 Element of NAT such that
A1: ( 0 <= i & i <= 2 |^ n & x = i / (2 |^ n) ) by Def3;
( 0 / (2 |^ n) <= i / (2 |^ n) & i / (2 |^ n) <= (2 |^ n) / (2 |^ n) ) by A1, XREAL_1:74;
hence ( 0 <= x & x <= 1 ) by A1, XCMPLX_1:60; :: thesis: verum