let d be Dyadic; :: thesis: ( d is Integer or ex p being Nat ex i being Integer st d = ((2 * i) + 1) / (2 |^ (p + 1)) )
assume A1: d is not Integer ; :: thesis: ex p being Nat ex i being Integer st d = ((2 * i) + 1) / (2 |^ (p + 1))
then A2: not d in INT ;
consider i being Integer, n being Nat such that
A3: d = i / (2 |^ n) by Th18;
defpred S₁[ Nat] means d in DYADIC ($1 + 1);
n <> 0 by A2, Th21, A3, Def4;
then reconsider n1 = n - 1 as Nat by NAT_1:20;
d in DYADIC (n1 + 1) by A3, Def4;
then A4: ex n being Nat st S₁[n] ;
consider m being Nat such that
A5: ( S₁[m] & ( for n being Nat st S₁[n] holds
m <= n ) ) from NAT_1:sch 5(A4);
not d in DYADIC m

proof

assume A6: d in DYADIC m ; :: thesis: contradiction
then m <> 0 by A1, Th21;
then reconsider m1 = m - 1 as Nat by NAT_1:20;
m1 + 1 <= m1 by A6, A5;
hence contradiction by NAT_1:13; :: thesis: verum

end;

then d in (DYADIC (m + 1)) \ (DYADIC m) by A5, XBOOLE_0:def 5;
then ex i being Integer st d = ((2 * i) + 1) / (2 |^ (m + 1)) by Th20;
hence ex p being Nat ex i being Integer st d = ((2 * i) + 1) / (2 |^ (p + 1)) ; :: thesis: verum