let n, p be Nat; :: thesis: for x being Surreal st p > 0 holds
( [{(uDyadic . (n / (2 |^ p)))},{(uDyadic . ((n + 2) / (2 |^ p)))}] is Surreal & ( x = [{(uDyadic . (n / (2 |^ p)))},{(uDyadic . ((n + 2) / (2 |^ p)))}] implies x == uDyadic . ((n + 1) / (2 |^ p)) ) )
let x be Surreal; :: thesis: ( p > 0 implies ( [{(uDyadic . (n / (2 |^ p)))},{(uDyadic . ((n + 2) / (2 |^ p)))}] is Surreal & ( x = [{(uDyadic . (n / (2 |^ p)))},{(uDyadic . ((n + 2) / (2 |^ p)))}] implies x == uDyadic . ((n + 1) / (2 |^ p)) ) ) )
assume A1: p > 0 ; :: thesis: ( [{(uDyadic . (n / (2 |^ p)))},{(uDyadic . ((n + 2) / (2 |^ p)))}] is Surreal & ( x = [{(uDyadic . (n / (2 |^ p)))},{(uDyadic . ((n + 2) / (2 |^ p)))}] implies x == uDyadic . ((n + 1) / (2 |^ p)) ) )
reconsider P = p - 1 as Nat by A1, NAT_1:20;
set p1 = P + 1;
n + 0 < n + 2 by XREAL_1:6;
then n / (2 |^ p) < (n + 2) / (2 |^ p) by XREAL_1:74;
hence [{(uDyadic . (n / (2 |^ p)))},{(uDyadic . ((n + 2) / (2 |^ p)))}] is Surreal by SURREALO:22, Th24; :: thesis: ( x = [{(uDyadic . (n / (2 |^ p)))},{(uDyadic . ((n + 2) / (2 |^ p)))}] implies x == uDyadic . ((n + 1) / (2 |^ p)) )
assume A2: x = [{(uDyadic . (n / (2 |^ p)))},{(uDyadic . ((n + 2) / (2 |^ p)))}] ; :: thesis: x == uDyadic . ((n + 1) / (2 |^ p))
A3: 2 * (2 |^ P) = 2 |^ (P + 1) by NEWTON:6;

per cases ( n is even or n is odd ) ;

suppose n is even ; :: thesis: x == uDyadic . ((n + 1) / (2 |^ p))

then consider k being Nat such that
A4: n = 2 * k by ABIAN:def 2;
( k / (2 |^ P) = n / (2 |^ (P + 1)) & (k + 1) / (2 |^ P) = (2 * (k + 1)) / (2 |^ (P + 1)) ) by A4, XCMPLX_1:91, A3;
hence x == uDyadic . ((n + 1) / (2 |^ p)) by A4, A2, Def5; :: thesis: verum

end;

suppose n is odd ; :: thesis: x == uDyadic . ((n + 1) / (2 |^ p))

then consider k being Nat such that
A5: n = (2 * k) + 1 by ABIAN:9;
set D = uDyadic . ((n + 1) / (2 |^ p));
( n + 0 < n + 1 & (n + 1) + 0 < (n + 1) + 1 ) by XREAL_1:6;
then ( n / (2 |^ p) < (n + 1) / (2 |^ p) & (n + 1) / (2 |^ p) < ((n + 1) + 1) / (2 |^ p) ) by XREAL_1:74;
then A6: ( L_ x << {(uDyadic . ((n + 1) / (2 |^ p)))} & {(uDyadic . ((n + 1) / (2 |^ p)))} << R_ x ) by A2, SURREALO:21, Th24;

per cases ( (n + 1) / (2 |^ p) is Integer or not (n + 1) / (2 |^ p) is Integer ) ;

suppose (n + 1) / (2 |^ p) is Integer ; :: thesis: x == uDyadic . ((n + 1) / (2 |^ p))

then reconsider N = (n + 1) / (2 |^ p) as Integer ;
N <> 0 ;
then reconsider N1 = N - 1 as Nat by NAT_1:20;
A7: ( (N * (2 |^ P)) * 2 = N * (2 |^ p) & N * (2 |^ p) = n + 1 & n + 1 = 2 * (k + 1) ) by A3, XCMPLX_1:87, A5;
N = N1 + 1 ;
then A8: ( uDyadic . ((n + 1) / (2 |^ p)) = uInt . N & uInt . N = [{(uInt . N1)},{}] ) by Def1, Def5;
then A9: {x} << R_ (uDyadic . ((n + 1) / (2 |^ p))) ;
(N * (2 |^ p)) - (1 * (2 |^ p)) <= (N * (2 |^ p)) - 1 by XREAL_1:10, NAT_1:14;
then ( N1 * (2 |^ p) <= n & n = (N * (2 |^ p)) - 1 ) by A7;
then N1 <= n / (2 |^ p) by XREAL_1:77;
then ( uInt . N1 = uDyadic . N1 & uDyadic . N1 <= uDyadic . (n / (2 |^ p)) ) by Def5, Th24;
then ( not L_ x << {(uInt . N1)} or not {x} << R_ (uInt . N1) ) by A2, SURREALO:21;
then not x <= uInt . N1 by SURREAL0:43;
then L_ (uDyadic . ((n + 1) / (2 |^ p))) << {x} by A8, SURREALO:21;
hence x == uDyadic . ((n + 1) / (2 |^ p)) by A9, A6, SURREAL0:43; :: thesis: verum

end;

suppose (n + 1) / (2 |^ p) is not Integer ; :: thesis: x == uDyadic . ((n + 1) / (2 |^ p))

then consider n3, m3, p3 being Nat such that
A10: ( (n + 1) / (2 |^ p) = n3 + (((2 * m3) + 1) / (2 |^ (p3 + 1))) & (2 * m3) + 1 < 2 |^ (p3 + 1) ) by Th28;
set i3 = m3 + (n3 * (2 |^ p3));
A11: 2 |^ (p3 + 1) = 2 * (2 |^ p3) by NEWTON:6;
then A12: (n + 1) / (2 |^ p) = ((n3 * (2 * (2 |^ p3))) + ((2 * m3) + 1)) / (2 |^ (p3 + 1)) by A10, XCMPLX_1:113
.= ((2 * (m3 + (n3 * (2 |^ p3)))) + 1) / (2 |^ (p3 + 1)) ;
(((2 * k) + 1) + 1) * (2 |^ (p3 + 1)) = ((2 * (m3 + (n3 * (2 |^ p3)))) + 1) * (2 |^ p) by A12, A5, XCMPLX_1:95;
then ((k + 1) * (2 |^ (p3 + 1))) * 2 = (((2 * (m3 + (n3 * (2 |^ p3)))) + 1) * (2 |^ P)) * 2 by A3;
then 2 |^ (p3 + 1) divides 2 |^ P by NEWTON02:67, INT_1:def 3;
then reconsider pp = P - (p3 + 1) as Nat by NAT_1:21, PEPIN:31;
set M = 2 |^ pp;
P = pp + (p3 + 1) ;
then A13: 2 |^ P = (2 |^ pp) * (2 |^ (p3 + 1)) by NEWTON:8;
(n + 1) / (2 |^ p) = ((2 * (2 |^ pp)) * ((2 * (m3 + (n3 * (2 |^ p3)))) + 1)) / ((2 * (2 |^ pp)) * (2 |^ (p3 + 1))) by A12, XCMPLX_1:91
.= ((2 * (2 |^ pp)) * ((2 * (m3 + (n3 * (2 |^ p3)))) + 1)) / (2 |^ p) by A13, A3 ;
then A14: n + 1 = (2 * (2 |^ pp)) * ((2 * (m3 + (n3 * (2 |^ p3)))) + 1) by XCMPLX_1:53;
set D = uDyadic . ((n + 1) / (2 |^ p));
A15: (m3 + (n3 * (2 |^ p3))) / (2 |^ p3) = (((2 * 2) * (2 |^ pp)) * (m3 + (n3 * (2 |^ p3)))) / (((2 * 2) * (2 |^ pp)) * (2 |^ p3)) by XCMPLX_1:91
.= (((2 * 2) * (2 |^ pp)) * (m3 + (n3 * (2 |^ p3)))) / (2 |^ p) by A13, A3, A11 ;
0 <= ((2 |^ pp) + (2 |^ pp)) - 1 by XREAL_1:48, NAT_1:14;
then (((2 * 2) * (2 |^ pp)) * (m3 + (n3 * (2 |^ p3)))) + 0 <= (((2 * 2) * (2 |^ pp)) * (m3 + (n3 * (2 |^ p3)))) + ((2 * (2 |^ pp)) - 1) by XREAL_1:6;
then not uDyadic . (n / (2 |^ p)) < uDyadic . ((m3 + (n3 * (2 |^ p3))) / (2 |^ p3)) by A14, A15, Th24, XREAL_1:72;
then ( not L_ x << {(uDyadic . ((m3 + (n3 * (2 |^ p3))) / (2 |^ p3)))} or not {x} << R_ (uDyadic . ((m3 + (n3 * (2 |^ p3))) / (2 |^ p3))) ) by A2, SURREALO:21;
then A16: not x <= uDyadic . ((m3 + (n3 * (2 |^ p3))) / (2 |^ p3)) by SURREAL0:43;
A17: ((m3 + (n3 * (2 |^ p3))) + 1) / (2 |^ p3) = (((2 * 2) * (2 |^ pp)) * ((m3 + (n3 * (2 |^ p3))) + 1)) / (((2 * 2) * (2 |^ pp)) * (2 |^ p3)) by XCMPLX_1:91
.= (((2 * 2) * (2 |^ pp)) * ((m3 + (n3 * (2 |^ p3))) + 1)) / (2 |^ p) by A13, A3, A11 ;
((((2 * (2 |^ pp)) * 2) * (m3 + (n3 * (2 |^ p3)))) + (2 * (2 |^ pp))) + 1 <= ((((2 * 2) * (2 |^ pp)) * (m3 + (n3 * (2 |^ p3)))) + (2 * (2 |^ pp))) + (2 * (2 |^ pp)) by NAT_1:14, XREAL_1:6;
then not uDyadic . (((m3 + (n3 * (2 |^ p3))) + 1) / (2 |^ p3)) < uDyadic . ((n + 2) / (2 |^ p)) by A14, A17, Th24, XREAL_1:72;
then ( not L_ (uDyadic . (((m3 + (n3 * (2 |^ p3))) + 1) / (2 |^ p3))) << {x} or not {(uDyadic . (((m3 + (n3 * (2 |^ p3))) + 1) / (2 |^ p3)))} << R_ x ) by A2, SURREALO:21;
then A18: x < uDyadic . (((m3 + (n3 * (2 |^ p3))) + 1) / (2 |^ p3)) by SURREAL0:43;
uDyadic . ((n + 1) / (2 |^ p)) = [{(uDyadic . ((m3 + (n3 * (2 |^ p3))) / (2 |^ p3)))},{(uDyadic . (((m3 + (n3 * (2 |^ p3))) + 1) / (2 |^ p3)))}] by A12, Def5;
then ( L_ (uDyadic . ((n + 1) / (2 |^ p))) << {x} & {x} << R_ (uDyadic . ((n + 1) / (2 |^ p))) ) by A16, A18, SURREALO:21;
hence x == uDyadic . ((n + 1) / (2 |^ p)) by A6, SURREAL0:43; :: thesis: verum

end;

end;

end;

end;