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 & s <= 2 |^ (n + 1) & x = s / (2 |^ (n + 1)) ) by Def3;
consider k being Element of NAT such that
A4: ( s = 2 * k or s = (2 * k) + 1 ) by SCHEME1:1;
now
per cases ( s = k * 2 or s = (k * 2) + 1 ) by A4;
case s = k * 2 ; :: thesis: ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )
then ( 0 <= k * 2 & k * 2 <= (2 |^ n) * 2 & x = (k * 2) / ((2 |^ n) * 2) ) by A3, NEWTON:11;
then ( 0 <= k & k <= ((2 |^ n) * 2) / 2 & x = k / (2 |^ n) ) by XREAL_1:134, XCMPLX_1:92, XREAL_1:79;
hence ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) ) by A1, Def3; :: thesis: verum
end;
case A5: s = (k * 2) + 1 ; :: thesis: ex k, i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )
then A6: a = (((k * 2) + 1) - 1) / (2 |^ (n + 1)) by A2, A3, Def7
.= (k * 2) / ((2 |^ n) * 2) by NEWTON:11
.= (k / (2 |^ n)) * (2 / 2) by XCMPLX_1:77
.= k / (2 |^ n) ;
take k = k; :: thesis: ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )
( 0 <= k & k <= 2 |^ n )
proof
thus 0 <= k by NAT_1:2; :: thesis: k <= 2 |^ n
A7: k * 2 <= (2 |^ (n + 1)) - 1 by A3, A5, XREAL_1:21;
(2 |^ (n + 1)) - 1 <= 2 |^ (n + 1) by XREAL_1:46;
then k * 2 <= 2 |^ (n + 1) by A7, XXREAL_0:2;
then k * 2 <= (2 |^ n) * 2 by NEWTON:11;
then ( k <= ((2 |^ n) * 2) / 2 & 2 <> 0 ) by XREAL_1:79;
hence k <= 2 |^ n ; :: thesis: verum
end;
hence ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) ) by A6; :: 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
A8: 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
A9: ( 0 <= s & s <= 2 |^ (n + 1) & x = s / (2 |^ (n + 1)) ) by Def3;
consider k being Element of NAT such that
A10: ( s = 2 * k or s = (2 * k) + 1 ) by SCHEME1:1;
now
per cases ( s = k * 2 or s = (k * 2) + 1 ) by A10;
case s = k * 2 ; :: thesis: ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )
then ( 0 <= k * 2 & k * 2 <= (2 |^ n) * 2 & x = (k * 2) / ((2 |^ n) * 2) ) by A9, NEWTON:11;
then ( 0 <= k & k <= ((2 |^ n) * 2) / 2 & x = k / (2 |^ n) ) by XREAL_1:134, XCMPLX_1:92, XREAL_1:79;
hence ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) ) by A1, Def3; :: thesis: verum
end;
case A11: 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
A12: l = k + 1 ;
A13: s <> 2 |^ (n + 1)
proof
assume A14: s = 2 |^ (n + 1) ; :: thesis: contradiction
2 |^ (n + 1) <> 0 by NEWTON:102;
then x = 1 by A9, A14, XCMPLX_1:60;
hence contradiction by A1, Th12; :: thesis: verum
end;
A15: a = (((k * 2) + 1) + 1) / (2 |^ (n + 1)) by A8, A9, A11, Def7
.= ((k + 1) * 2) / ((2 |^ n) * 2) by NEWTON:11
.= ((k + 1) / (2 |^ n)) * (2 / 2) by XCMPLX_1:77
.= l / (2 |^ n) by A12 ;
take l = l; :: thesis: ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) )
( 0 <= l & l <= 2 |^ n )
proof
(((k * 2) + 1) + 1) + (- 1) < 2 |^ (n + 1) by A9, A11, A13, XXREAL_0:1;
then l * 2 <= 2 |^ (n + 1) by A12, NAT_1:13;
then l * 2 <= (2 |^ n) * 2 by NEWTON:11;
then ( l <= ((2 |^ n) * 2) / 2 & 2 <> 0 ) by XREAL_1:79;
hence ( 0 <= l & l <= 2 |^ n ) by NAT_1:2; :: thesis: verum
end;
hence ex i being Element of NAT st
( 0 <= i & i <= 2 |^ n & a = i / (2 |^ n) ) by A15; :: 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 A8, Def3; :: thesis: verum
end;