let n be Nat; :: thesis: for x being Element of dyadic (n + 1) st not x in dyadic n holds
( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n )

let x be Element of dyadic (n + 1); :: thesis: ( not x in dyadic n implies ( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n ) )
assume A1: not x in dyadic n ; :: thesis: ( ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n )
thus ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n :: thesis: ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n
proof
consider a being Real such that
A2: a = ((axis x) - 1) / (2 |^ (n + 1)) ;
ex i being Nat st
( i <= 2 |^ n & a = i / (2 |^ n) )
proof
consider s being Nat such that
A3: s <= 2 |^ (n + 1) and
A4: x = s / (2 |^ (n + 1)) by Def1;
consider k being Element of NAT such that
A5: ( s = 2 * k or s = (2 * k) + 1 ) by SCHEME1:1;
now :: thesis: ( ( s = k * 2 & ex i being Nat st
( i <= 2 |^ n & a = i / (2 |^ n) ) ) or ( s = (k * 2) + 1 & ex k being Element of NAT ex i being Nat st
( i <= 2 |^ n & a = i / (2 |^ n) ) ) )
per cases ( s = k * 2 or s = (k * 2) + 1 ) by A5;
case A6: s = k * 2 ; :: thesis: ex i being Nat st
( i <= 2 |^ n & a = i / (2 |^ n) )

then x = (k * 2) / ((2 |^ n) * 2) by ;
then A7: x = k / (2 |^ n) by XCMPLX_1:91;
k * 2 <= (2 |^ n) * 2 by ;
then k <= ((2 |^ n) * 2) / 2 by XREAL_1:77;
hence ex i being Nat st
( i <= 2 |^ n & a = i / (2 |^ n) ) by A1, A7, Def1; :: thesis: verum
end;
case A8: s = (k * 2) + 1 ; :: thesis: ex k being Element of NAT ex i being Nat st
( i <= 2 |^ n & a = i / (2 |^ n) )

A9: (2 |^ (n + 1)) - 1 <= 2 |^ (n + 1) by XREAL_1:44;
k * 2 <= (2 |^ (n + 1)) - 1 by ;
then k * 2 <= 2 |^ (n + 1) by ;
then k * 2 <= (2 |^ n) * 2 by NEWTON:6;
then A10: k <= ((2 |^ n) * 2) / 2 by XREAL_1:77;
take k = k; :: thesis: ex i being Nat st
( i <= 2 |^ n & a = i / (2 |^ n) )

a = (((k * 2) + 1) - 1) / (2 |^ (n + 1)) by A2, A4, A8, Def5
.= (k * 2) / ((2 |^ n) * 2) by NEWTON:6
.= (k / (2 |^ n)) * (2 / 2) by XCMPLX_1:76
.= k / (2 |^ n) ;
hence ex i being Nat st
( i <= 2 |^ n & a = i / (2 |^ n) ) by A10; :: thesis: verum
end;
end;
end;
hence ex i being Nat st
( i <= 2 |^ n & a = i / (2 |^ n) ) ; :: thesis: verum
end;
hence ((axis x) - 1) / (2 |^ (n + 1)) in dyadic n by ; :: thesis: verum
end;
thus ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n :: thesis: verum
proof
set a = ((axis x) + 1) / (2 |^ (n + 1));
ex i being Nat st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) )
proof
consider s being Nat such that
A11: s <= 2 |^ (n + 1) and
A12: x = s / (2 |^ (n + 1)) by Def1;
consider k being Element of NAT such that
A13: ( s = 2 * k or s = (2 * k) + 1 ) by SCHEME1:1;
now :: thesis: ( ( s = k * 2 & ex i being Nat st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) ) or ( s = (k * 2) + 1 & ex l, i being Nat st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) ) )
per cases ( s = k * 2 or s = (k * 2) + 1 ) by A13;
case A14: s = k * 2 ; :: thesis: ex i being Nat st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) )

then x = (k * 2) / ((2 |^ n) * 2) by ;
then A15: x = k / (2 |^ n) by XCMPLX_1:91;
k * 2 <= (2 |^ n) * 2 by ;
then k <= ((2 |^ n) * 2) / 2 by XREAL_1:77;
hence ex i being Nat st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) by ; :: thesis: verum
end;
case A16: s = (k * 2) + 1 ; :: thesis: ex l, i being Nat st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) )

consider l being Nat such that
A17: l = k + 1 ;
s <> 2 |^ (n + 1)
proof
A18: 2 |^ (n + 1) <> 0 by NEWTON:83;
assume s = 2 |^ (n + 1) ; :: thesis: contradiction
then x = 1 by ;
hence contradiction by A1, Th6; :: thesis: verum
end;
then (((k * 2) + 1) + 1) + (- 1) < 2 |^ (n + 1) by ;
then l * 2 <= 2 |^ (n + 1) by ;
then l * 2 <= (2 |^ n) * 2 by NEWTON:6;
then A19: l <= ((2 |^ n) * 2) / 2 by XREAL_1:77;
take l = l; :: thesis: ex i being Nat st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) )

((axis x) + 1) / (2 |^ (n + 1)) = (((k * 2) + 1) + 1) / (2 |^ (n + 1)) by
.= ((k + 1) * 2) / ((2 |^ n) * 2) by NEWTON:6
.= ((k + 1) / (2 |^ n)) * (2 / 2) by XCMPLX_1:76
.= l / (2 |^ n) by A17 ;
hence ex i being Nat st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) by A19; :: thesis: verum
end;
end;
end;
hence ex i being Nat st
( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) ; :: thesis: verum
end;
hence ((axis x) + 1) / (2 |^ (n + 1)) in dyadic n by Def1; :: thesis: verum
end;