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

( ((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

thus
((axis x) + 1) / (2 |^ (n + 1)) in dyadic n
:: thesis: verum
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) )

end;A2: a = ((axis x) - 1) / (2 |^ (n + 1)) ;

ex i being Nat st

( i <= 2 |^ n & a = i / (2 |^ n) )

proof

hence
((axis x) - 1) / (2 |^ (n + 1)) in dyadic n
by A2, Def1; :: thesis: verum
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;

( i <= 2 |^ n & a = i / (2 |^ n) ) ; :: thesis: verum

end;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) ) ) )end;

hence
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;

end;

case A6:
s = k * 2
; :: thesis: ex i being Nat st

( i <= 2 |^ n & a = i / (2 |^ n) )

( 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;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

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) )

( 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;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

( i <= 2 |^ n & a = i / (2 |^ 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) )

end;ex i being Nat st

( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) )

proof

hence
((axis x) + 1) / (2 |^ (n + 1)) in dyadic n
by Def1; :: thesis: verum
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;

( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) ; :: thesis: verum

end;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) ) ) )end;

hence
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;

end;

case A14:
s = k * 2
; :: thesis: ex i being Nat st

( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) )

( 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;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

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) )

( 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)

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;A17: l = k + 1 ;

s <> 2 |^ (n + 1)

proof

then
(((k * 2) + 1) + 1) + (- 1) < 2 |^ (n + 1)
by A11, A16, XXREAL_0:1;
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;assume s = 2 |^ (n + 1) ; :: thesis: contradiction

then x = 1 by A12, A18, XCMPLX_1:60;

hence contradiction by A1, Th6; :: thesis: verum

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

( i <= 2 |^ n & ((axis x) + 1) / (2 |^ (n + 1)) = i / (2 |^ n) ) ; :: thesis: verum