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 A4, NEWTON:6;
then A7: x = k / (2 |^ n) by XCMPLX_1:91;
k * 2 <= (2 |^ n) * 2 by A3, A6, NEWTON:6;
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 A3, A8, XREAL_1:19;
then k * 2 <= 2 |^ (n + 1) by A9, XXREAL_0:2;
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 A2, Def1; :: 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 A12, NEWTON:6;
then A15: x = k / (2 |^ n) by XCMPLX_1:91;
k * 2 <= (2 |^ n) * 2 by A11, A14, NEWTON:6;
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 A1, A15, Def1; :: 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 A12, A18, XCMPLX_1:60;
hence contradiction by A1, Th6; :: thesis: verum

end;

then (((k * 2) + 1) + 1) + (- 1) < 2 |^ (n + 1) by A11, A16, XXREAL_0:1;
then l * 2 <= 2 |^ (n + 1) by A17, NAT_1:13;
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 A12, A16, Def5
.= ((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;