let d be Dyadic; :: thesis: ( 0 <= d & d is not Integer implies ex n, m, p being Nat st
( d = n + (((2 * m) + 1) / (2 |^ (p + 1))) & (2 * m) + 1 < 2 |^ (p + 1) ) )
assume A1: ( 0 <= d & d is not Integer ) ; :: thesis: ex n, m, p being Nat st
( d = n + (((2 * m) + 1) / (2 |^ (p + 1))) & (2 * m) + 1 < 2 |^ (p + 1) )
then consider p being Nat, i being Integer such that
A2: d = ((2 * i) + 1) / (2 |^ (p + 1)) by Th23;
i >= 0

proof

assume i < 0 ; :: thesis: contradiction
then i + 1 <= 0 by INT_1:7;
then (i + 1) + i < 0 + 0 by XREAL_1:6;
hence contradiction by A1, A2; :: thesis: verum

end;

then reconsider i = i as Element of NAT by INT_1:3;
set DV = ((2 * i) + 1) div (2 |^ (p + 1));
set MD = ((2 * i) + 1) mod (2 |^ (p + 1));
A3: 2 |^ (p + 1) = 2 * (2 |^ p) by NEWTON:6;
A4: (2 * i) + 1 = ((((2 * i) + 1) div (2 |^ (p + 1))) * (2 |^ (p + 1))) + (((2 * i) + 1) mod (2 |^ (p + 1))) by INT_1:59;
then (2 * i) + 1 >= ((((2 * i) + 1) div (2 |^ (p + 1))) * (2 |^ p)) * 2 by A3, NAT_1:11;
then (2 * i) + 1 > ((((2 * i) + 1) div (2 |^ (p + 1))) * (2 |^ p)) * 2 by XXREAL_0:1;
then i >= (((2 * i) + 1) div (2 |^ (p + 1))) * (2 |^ p) by XREAL_1:68, NAT_1:13;
then reconsider M = i - ((((2 * i) + 1) div (2 |^ (p + 1))) * (2 |^ p)) as Nat by NAT_1:21;
take ((2 * i) + 1) div (2 |^ (p + 1)) ; :: thesis: ex m, p being Nat st
( d = (((2 * i) + 1) div (2 |^ (p + 1))) + (((2 * m) + 1) / (2 |^ (p + 1))) & (2 * m) + 1 < 2 |^ (p + 1) )
take M ; :: thesis: ex p being Nat st
( d = (((2 * i) + 1) div (2 |^ (p + 1))) + (((2 * M) + 1) / (2 |^ (p + 1))) & (2 * M) + 1 < 2 |^ (p + 1) )
take p ; :: thesis: ( d = (((2 * i) + 1) div (2 |^ (p + 1))) + (((2 * M) + 1) / (2 |^ (p + 1))) & (2 * M) + 1 < 2 |^ (p + 1) )
A5: ((2 * i) + 1) mod (2 |^ (p + 1)) = ((2 * i) + 1) - ((((2 * i) + 1) div (2 |^ (p + 1))) * (2 |^ (p + 1))) by A4
.= (2 * M) + 1 by A3 ;
thus d = (((((2 * i) + 1) div (2 |^ (p + 1))) * (2 |^ (p + 1))) + (((2 * i) + 1) mod (2 |^ (p + 1)))) / (2 |^ (p + 1)) by INT_1:59, A2
.= (((2 * i) + 1) div (2 |^ (p + 1))) + (((2 * M) + 1) / (2 |^ (p + 1))) by A5, XCMPLX_1:113 ; :: thesis: (2 * M) + 1 < 2 |^ (p + 1)
thus (2 * M) + 1 < 2 |^ (p + 1) by A5, INT_1:58; :: thesis: verum