let d be Dyadic; :: thesis: for n being Nat holds
( d in (DYADIC (n + 1)) \ (DYADIC n) iff ex i being Integer st d = ((2 * i) + 1) / (2 |^ (n + 1)) )
let n be Nat; :: thesis: ( d in (DYADIC (n + 1)) \ (DYADIC n) iff ex i being Integer st d = ((2 * i) + 1) / (2 |^ (n + 1)) )
thus ( d in (DYADIC (n + 1)) \ (DYADIC n) implies ex i being Integer st d = ((2 * i) + 1) / (2 |^ (n + 1)) ) :: thesis: ( ex i being Integer st d = ((2 * i) + 1) / (2 |^ (n + 1)) implies d in (DYADIC (n + 1)) \ (DYADIC n) )

proof

assume A1: d in (DYADIC (n + 1)) \ (DYADIC n) ; :: thesis: ex i being Integer st d = ((2 * i) + 1) / (2 |^ (n + 1))
then d in DYADIC (n + 1) by XBOOLE_0:def 5;
then consider i being Integer such that
A2: d = i / (2 |^ (n + 1)) by Def4;
i is odd

proof

assume i is even ; :: thesis: contradiction
then consider j being Integer such that
A3: i = 2 * j by ABIAN:11;
d = (j * 2) / (2 * (2 |^ n)) by A3, A2, NEWTON:6;
then d = j / (2 |^ n) by XCMPLX_1:91;
then d in DYADIC n by Def4;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum

end;

then consider j being Integer such that
A4: i = (2 * j) + 1 by ABIAN:1;
take j ; :: thesis: d = ((2 * j) + 1) / (2 |^ (n + 1))
thus d = ((2 * j) + 1) / (2 |^ (n + 1)) by A2, A4; :: thesis: verum

end;

given i being Integer such that A5: d = ((2 * i) + 1) / (2 |^ (n + 1)) ; :: thesis: d in (DYADIC (n + 1)) \ (DYADIC n)
A6: d in DYADIC (n + 1) by Def4, A5;
not d in DYADIC n

proof

assume d in DYADIC n ; :: thesis: contradiction
then consider j being Integer such that
A7: d = j / (2 |^ n) by Def4;
A8: 2 |^ (n + 1) = 2 * (2 |^ n) by NEWTON:6;
j * (2 |^ (n + 1)) = ((2 * i) + 1) * (2 |^ n) by A7, A5, XCMPLX_1:95;
then (j * 2) * (2 |^ n) = ((2 * i) + 1) * (2 |^ n) by A8;
hence contradiction by XCMPLX_1:5; :: thesis: verum

end;

hence d in (DYADIC (n + 1)) \ (DYADIC n) by A6, XBOOLE_0:def 5; :: thesis: verum