let n, m, p be Nat; :: thesis: ( (2 * m) + 1 < 2 |^ p implies born (uDyadic . (n + (((2 * m) + 1) / (2 |^ p)))) = (n + p) + 1 )
set d = n + (((2 * m) + 1) / (2 |^ p));
assume A1: ( (2 * m) + 1 < 2 |^ p & born (uDyadic . (n + (((2 * m) + 1) / (2 |^ p)))) <> (n + p) + 1 ) ; :: thesis: contradiction
A2: not uDyadic . (n + (((2 * m) + 1) / (2 |^ p))) == uDyadic . (n + p)

proof

assume uDyadic . (n + (((2 * m) + 1) / (2 |^ p))) == uDyadic . (n + p) ; :: thesis: contradiction
then ( n + (((2 * m) + 1) / (2 |^ p)) <= n + p & n + p <= n + (((2 * m) + 1) / (2 |^ p)) ) by Th24;
then n + (((2 * m) + 1) / (2 |^ p)) = n + p by XXREAL_0:1;
then p * (2 |^ p) < 1 * (2 |^ p) by A1, XCMPLX_1:87;
then p = 0 by NAT_1:14, XREAL_1:64;
then 2 |^ p = 1 + 0 by NEWTON:4;
hence contradiction by A1, NAT_1:13; :: thesis: verum

end;

n + p < (n + p) + 1 by NAT_1:13;
then A3: ( 0_No <= uDyadic . (n + (((2 * m) + 1) / (2 |^ p))) & uDyadic . (n + (((2 * m) + 1) / (2 |^ p))) in Day ((n + p) + 1) ) by A1, Th25;
for O being Ordinal st uDyadic . (n + (((2 * m) + 1) / (2 |^ p))) in Day O holds
(n + p) + 1 c= O

proof

let O be Ordinal; :: thesis: ( uDyadic . (n + (((2 * m) + 1) / (2 |^ p))) in Day O implies (n + p) + 1 c= O )
assume that
A4: uDyadic . (n + (((2 * m) + 1) / (2 |^ p))) in Day O and
A5: not (n + p) + 1 c= O ; :: thesis: contradiction
A6: ( O in (n + p) + 1 & (n + p) + 1 = Segm ((n + p) + 1) ) by A5, ORDINAL1:16;
reconsider O = O as Nat by A5;
O < (n + p) + 1 by A6, NAT_1:44;
then ( Segm O = O & O <= n + p & n + p = Segm (n + p) ) by NAT_1:13;
then Day O c= Day (n + p) by NAT_1:39, SURREAL0:35;
then consider x, y, p1 being Nat such that
A7: ( uDyadic . (n + (((2 * m) + 1) / (2 |^ p))) == uDyadic . (x + (y / (2 |^ p1))) & y < 2 |^ p1 & x + p1 < n + p ) by A4, Th25, A2, A3;
( n + (((2 * m) + 1) / (2 |^ p)) <= x + (y / (2 |^ p1)) & x + (y / (2 |^ p1)) <= n + (((2 * m) + 1) / (2 |^ p)) ) by A7, Th24;
then A8: n + (((2 * m) + 1) / (2 |^ p)) = x + (y / (2 |^ p1)) by XXREAL_0:1;
( 0 <= ((2 * m) + 1) / (2 |^ p) & ((2 * m) + 1) / (2 |^ p) < 1 & 0 <= y / (2 |^ p1) & y / (2 |^ p1) < 1 ) by A1, A7, XREAL_1:191;
then ( n + 0 <= n + (((2 * m) + 1) / (2 |^ p)) & n + (((2 * m) + 1) / (2 |^ p)) < n + 1 & x + 0 <= x + (y / (2 |^ p1)) & x + (y / (2 |^ p1)) < x + 1 ) by XREAL_1:6;
then ( n < x + 1 & x < n + 1 ) by A8, XXREAL_0:2;
then ( n <= x & x <= n ) by NAT_1:13;
then A9: x = n by XXREAL_0:1;
then p1 < p by A7, XREAL_1:6;
then p1 + 1 <= p by NAT_1:13;
then reconsider P = p - (p1 + 1) as Nat by NAT_1:21;
p = (p1 + 1) + P ;
then A10: ( 2 |^ p = (2 |^ (p1 + 1)) * (2 |^ P) & 2 |^ (p1 + 1) = 2 * (2 |^ p1) ) by NEWTON:6, NEWTON:8;
((2 * m) + 1) * (2 |^ p1) = y * (2 |^ p) by A8, A9, XCMPLX_1:95
.= ((y * (2 |^ P)) * 2) * (2 |^ p1) by A10 ;
hence contradiction by XCMPLX_1:5; :: thesis: verum

end;

hence contradiction by A1, SURREAL0:def 18, A3; :: thesis: verum