let n be Element of NAT ; :: thesis: for x being Element of dyadic (n + 1) st not x in dyadic n holds
( ((axis x,(n + 1)) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x,(n + 1)) + 1) / (2 |^ (n + 1)) in dyadic n )
let x be Element of dyadic (n + 1); :: thesis: ( not x in dyadic n implies ( ((axis x,(n + 1)) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x,(n + 1)) + 1) / (2 |^ (n + 1)) in dyadic n ) )
assume A1: not x in dyadic n ; :: thesis: ( ((axis x,(n + 1)) - 1) / (2 |^ (n + 1)) in dyadic n & ((axis x,(n + 1)) + 1) / (2 |^ (n + 1)) in dyadic n )
thus ((axis x,(n + 1)) - 1) / (2 |^ (n + 1)) in dyadic n :: thesis: ((axis x,(n + 1)) + 1) / (2 |^ (n + 1)) in dyadic n

proof

consider a being Real such that
A2: a = ((axis x,(n + 1)) - 1) / (2 |^ (n + 1)) ;
ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )

proof

consider s being Element of NAT such that
A3: 0 <= s and
A4: s <= 2 |^ (n + 1) and
A5: x = s / (2 |^ (n + 1)) by Def3;
consider k being Element of NAT such that
A6: ( s = 2 * k or s = (2 * k) + 1 ) by SCHEME1:1;

now

per cases ( s = k * 2 or s = (k * 2) + 1 ) by A6;

case A7: s = k * 2 ; :: thesis: ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )

then x = (k * 2) / ((2 |^ n) * 2) by A5, NEWTON:11;
then A8: x = k / (2 |^ n) by XCMPLX_1:92;
k * 2 <= (2 |^ n) * 2 by A4, A7, NEWTON:11;
then A9: k <= ((2 |^ n) * 2) / 2 by XREAL_1:79;
0 <= k by A3, A7, XREAL_1:134;
hence ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) ) by A1, A9, A8, Def3; :: thesis: verum

end;

case A10: s = (k * 2) + 1 ; :: thesis: ex k, i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )

A11: (2 |^ (n + 1)) - 1 <= 2 |^ (n + 1) by XREAL_1:46;
k * 2 <= (2 |^ (n + 1)) - 1 by A4, A10, XREAL_1:21;
then k * 2 <= 2 |^ (n + 1) by A11, XXREAL_0:2;
then k * 2 <= (2 |^ n) * 2 by NEWTON:11;
then A12: k <= ((2 |^ n) * 2) / 2 by XREAL_1:79;
take k = k; :: thesis: ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )
A13: 0 <= k by NAT_1:2;
a = (((k * 2) + 1) - 1) / (2 |^ (n + 1)) by A2, A5, A10, Def7
.= (k * 2) / ((2 |^ n) * 2) by NEWTON:11
.= (k / (2 |^ n)) * (2 / 2) by XCMPLX_1:77
.= k / (2 |^ n) ;
hence ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) ) by A12, A13; :: thesis: verum

end;

end;

end;

hence ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) ) ; :: thesis: verum

end;

hence ((axis x,(n + 1)) - 1) / (2 |^ (n + 1)) in dyadic n by A2, Def3; :: thesis: verum

end;

thus ((axis x,(n + 1)) + 1) / (2 |^ (n + 1)) in dyadic n :: thesis: verum

proof

consider a being Real such that
A14: a = ((axis x,(n + 1)) + 1) / (2 |^ (n + 1)) ;
ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )

proof

consider s being Element of NAT such that
A15: 0 <= s and
A16: s <= 2 |^ (n + 1) and
A17: x = s / (2 |^ (n + 1)) by Def3;
consider k being Element of NAT such that
A18: ( s = 2 * k or s = (2 * k) + 1 ) by SCHEME1:1;

now

per cases ( s = k * 2 or s = (k * 2) + 1 ) by A18;

case A19: s = k * 2 ; :: thesis: ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )

then x = (k * 2) / ((2 |^ n) * 2) by A17, NEWTON:11;
then A20: x = k / (2 |^ n) by XCMPLX_1:92;
k * 2 <= (2 |^ n) * 2 by A16, A19, NEWTON:11;
then A21: k <= ((2 |^ n) * 2) / 2 by XREAL_1:79;
0 <= k by A15, A19, XREAL_1:134;
hence ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) ) by A1, A21, A20, Def3; :: thesis: verum

end;

case A22: s = (k * 2) + 1 ; :: thesis: ex l, i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )

consider l being Element of NAT such that
A23: l = k + 1 ;
s <> 2 |^ (n + 1)

proof

A24: 2 |^ (n + 1) <> 0 by NEWTON:102;
assume s = 2 |^ (n + 1) ; :: thesis: contradiction
then x = 1 by A17, A24, XCMPLX_1:60;
hence contradiction by A1, Th12; :: thesis: verum

end;

then (((k * 2) + 1) + 1) + (- 1) < 2 |^ (n + 1) by A16, A22, XXREAL_0:1;
then l * 2 <= 2 |^ (n + 1) by A23, NAT_1:13;
then l * 2 <= (2 |^ n) * 2 by NEWTON:11;
then A25: l <= ((2 |^ n) * 2) / 2 by XREAL_1:79;
take l = l; :: thesis: ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )
A26: 0 <= l by NAT_1:2;
a = (((k * 2) + 1) + 1) / (2 |^ (n + 1)) by A14, A17, A22, Def7
.= ((k + 1) * 2) / ((2 |^ n) * 2) by NEWTON:11
.= ((k + 1) / (2 |^ n)) * (2 / 2) by XCMPLX_1:77
.= l / (2 |^ n) by A23 ;
hence ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) ) by A25, A26; :: thesis: verum

end;

end;

end;

hence ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) ) ; :: thesis: verum

end;

hence ((axis x,(n + 1)) + 1) / (2 |^ (n + 1)) in dyadic n by A14, Def3; :: thesis: verum

end;