let r be Rational; :: thesis: ( r is dyadic-like iff ex i being Integer ex n being Nat st r = i / (2 |^ n) )
thus ( r is dyadic-like implies ex i being Integer ex n being Nat st r = i / (2 |^ n) ) :: thesis: ( ex i being Integer ex n being Nat st r = i / (2 |^ n) implies r is dyadic-like )

proof

assume r is dyadic-like ; :: thesis: ex i being Integer ex n being Nat st r = i / (2 |^ n)
then consider n being Nat such that
A1: denominator r = 2 |^ n ;
take numerator r ; :: thesis: ex n being Nat st r = (numerator r) / (2 |^ n)
take n ; :: thesis: r = (numerator r) / (2 |^ n)
thus r = (numerator r) / (2 |^ n) by A1, RAT_1:15; :: thesis: verum

end;

given i being Integer, n being Nat such that A2: r = i / (2 |^ n) ; :: thesis: r is dyadic-like
consider w being Nat such that
A3: ( i = (numerator r) * w & 2 |^ n = (denominator r) * w ) by A2, RAT_1:27;
consider t being Element of NAT such that
A4: ( w = 2 |^ t & t <= n ) by INT_2:28, A3, INT_1:def 3, PEPIN:34;
reconsider nt = n - t as Nat by A4, NAT_1:21;
n = t + nt ;
then (denominator r) * (2 |^ t) = (2 |^ nt) * (2 |^ t) by A4, A3, NEWTON:8;
hence r is dyadic-like by XCMPLX_1:5; :: thesis: verum