let z be Surreal; :: thesis: for n being Nat holds
( ( 0_No <= z & z in Day n & not z == uDyadic . n implies ex x, y, p being Nat st
( z == uDyadic . (x + (y / (2 |^ p))) & y < 2 |^ p & x + p < n ) ) & ( for x, y, p being Nat st y < 2 |^ p & x + p < n holds
( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day n ) ) )
let n be Nat; :: thesis: ( ( 0_No <= z & z in Day n & not z == uDyadic . n implies ex x, y, p being Nat st
( z == uDyadic . (x + (y / (2 |^ p))) & y < 2 |^ p & x + p < n ) ) & ( for x, y, p being Nat st y < 2 |^ p & x + p < n holds
( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day n ) ) )
defpred S₁[ Nat] means ( ( for s being Surreal st s in Day $1 & 0_No <= s & not s == uDyadic . $1 holds
ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < $1 ) ) & ( for x, y, p being Nat st y < 2 |^ p & x + p < $1 holds
( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day $1 ) ) );
A1: S₁[ 0 ]

proof

A2: ( 0_No = uInt . 0 & uInt . 0 = uDyadic . 0 ) by Def1, Def5;
thus for s being Surreal st s in Day 0 & 0_No <= s & not s == uDyadic . 0 holds
ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < 0 ) by A2, SURREAL0:2, TARSKI:def 1; :: thesis: for x, y, p being Nat st y < 2 |^ p & x + p < 0 holds
( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day 0 )
let x, y, p be Nat; :: thesis: ( y < 2 |^ p & x + p < 0 implies ( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day 0 ) )
assume A3: ( y < 2 |^ p & x + p < 0 ) ; :: thesis: ( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day 0 )
thus ( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day 0 ) by A3; :: thesis: verum

end;

A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
A6: ( 0_No = uInt . 0 & uInt . 0 = uDyadic . 0 ) by Def1, Def5;
n < n + 1 by NAT_1:13;
then A7: ( Segm n c= Segm (n + 1) & n in Segm (n + 1) ) by NAT_1:39, NAT_1:44;
then A8: Day n c= Day (n + 1) by SURREAL0:35;
thus for s being Surreal st s in Day (n + 1) & 0_No <= s & not s == uDyadic . (n + 1) holds
ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) :: thesis: for x, y, p being Nat st y < 2 |^ p & x + p < n + 1 holds
( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day (n + 1) )

proof

let s be Surreal; :: thesis: ( s in Day (n + 1) & 0_No <= s & not s == uDyadic . (n + 1) implies ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) )
assume A9: ( s in Day (n + 1) & 0_No <= s ) ; :: thesis: ( s == uDyadic . (n + 1) or ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) )
set c = Unique_No s;
A10: Unique_No s == s by SURREALO:def 10;
then A11: 0_No <= Unique_No s by A9, SURREALO:4;

per cases ( Unique_No s in Day n or not Unique_No s in Day n ) ;

suppose Unique_No s in Day n ; :: thesis: ( s == uDyadic . (n + 1) or ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) )

per cases then ( Unique_No s == uDyadic . n or ex d being Dyadic ex x, y, p being Nat st
( Unique_No s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n ) ) by A10, A9, SURREALO:4, A5;

suppose A12: Unique_No s == uDyadic . n ; :: thesis: ( s == uDyadic . (n + 1) or ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) )

ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )

proof

take d = n; :: thesis: ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )
take x = n; :: thesis: ex y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )
take y = 0 ; :: thesis: ex p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )
take p = 0 ; :: thesis: ( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )
thus ( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) by A12, A10, SURREALO:4, NAT_1:13; :: thesis: verum

end;

hence ( s == uDyadic . (n + 1) or ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) ) ; :: thesis: verum

end;

suppose ex d being Dyadic ex x, y, p being Nat st
( Unique_No s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n ) ; :: thesis: ( s == uDyadic . (n + 1) or ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) )

then consider d being Dyadic, x, y, p being Nat such that
A13: ( Unique_No s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n ) ;
( x + p < n + 1 & s == uDyadic . d ) by SURREALO:4, A10, A13, NAT_1:13;
hence ( s == uDyadic . (n + 1) or ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) ) by A13; :: thesis: verum

end;

end;

end;

suppose A14: not Unique_No s in Day n ; :: thesis: ( s == uDyadic . (n + 1) or ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) )

A15: born_eq (Unique_No s) = born (Unique_No s) by SURREALO:48;
A16: ( born_eq (Unique_No s) = born_eq s & born_eq s c= born s & born s c= n + 1 ) by A9, SURREAL0:def 18, SURREALO:def 5, SURREALO:33, SURREALO:def 10;
then A17: born_eq (Unique_No s) c= n + 1 by XBOOLE_1:1;
A18: Unique_No s in Day (born (Unique_No s)) by SURREAL0:def 18;
A19: n + 1 c= born_eq (Unique_No s)

proof

assume not n + 1 c= born_eq (Unique_No s) ; :: thesis: contradiction
then ( born_eq (Unique_No s) in Segm (n + 1) & Segm (n + 1) = succ (Segm n) ) by ORDINAL1:16, NAT_1:38;
then Day (born (Unique_No s)) c= Day n by SURREAL0:35, A15, ORDINAL1:22;
hence contradiction by A14, A18; :: thesis: verum

end;

then A20: n + 1 = born (Unique_No s) by A15, A17, XBOOLE_0:def 10;
assume A21: not s == uDyadic . (n + 1) ; :: thesis: ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )

per cases ( Unique_No s = 0_No or Unique_No s <> 0_No ) ;

suppose A22: Unique_No s = 0_No ; :: thesis: ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )

take d = 0 ; :: thesis: ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )
take x = 0 ; :: thesis: ex y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )
take y = 0 ; :: thesis: ex p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )
take p = 0 ; :: thesis: ( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )
thus ( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) by A22, SURREALO:def 10, A6; :: thesis: verum

end;

suppose A23: Unique_No s <> 0_No ; :: thesis: ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )

R_ (Unique_No s) <> {}

proof

assume A24: R_ (Unique_No s) = {} ; :: thesis: contradiction
then L_ (Unique_No s) <> {} by A23;
then card (L_ (Unique_No s)) = 1 by SURREALO:8, SURREALO:44, A15, A16;
then consider y being object such that
A25: L_ (Unique_No s) = {y} by CARD_2:42;
y in L_ (Unique_No s) by A25, TARSKI:def 1;
then reconsider y = y as Surreal by SURREAL0:def 16;
A26: not Unique_No s == 0_No by A23, SURREALO:50;
Unique_No s = [{y},{}] by A24, A25;
then consider k being Nat such that
A27: ( Unique_No s == uInt . (k + 1) & uInt . k <= y & y < uInt . (k + 1) & k in born (Unique_No s) ) by A26, Th16, A15, A16, Th17;
Unique_No s = uInt . (k + 1) by A27, SURREALO:50;
then ( Unique_No s = uInt . (n + 1) & uInt . (n + 1) = uDyadic . (n + 1) ) by A20, Th4, Def5;
hence contradiction by SURREALO:def 10, A21; :: thesis: verum

end;

then card (R_ (Unique_No s)) = 1 by A15, A16, SURREALO:8, SURREALO:45;
then consider c2 being object such that
A28: R_ (Unique_No s) = {c2} by CARD_2:42;
c2 in R_ (Unique_No s) by A28, TARSKI:def 1;
then reconsider c2 = c2 as Surreal by SURREAL0:def 16;
L_ (Unique_No s) <> {}

proof

assume A29: L_ (Unique_No s) = {} ; :: thesis: contradiction
- (Unique_No s) = [(-- (R_ (Unique_No s))),(-- (L_ (Unique_No s)))] by SURREALR:7;
then A30: - (Unique_No s) = [{(- c2)},{}] by A29, A28, SURREALR:21, SURREALR:22;
not Unique_No s == 0_No by A23, SURREALO:50;
then not - (Unique_No s) == 0_No by SURREALR:23, SURREALR:10;
then c2 <= 0_No by A30, Th16, SURREALR:23, SURREALR:10;
then ( not L_ 0_No << {(Unique_No s)} or not {0_No} << R_ (Unique_No s) ) by A28, SURREALO:21;
hence contradiction by A11, SURREAL0:43; :: thesis: verum

end;

then card (L_ (Unique_No s)) = 1 by A15, A16, SURREALO:8, SURREALO:44;
then consider c1 being object such that
A31: L_ (Unique_No s) = {c1} by CARD_2:42;
c1 in L_ (Unique_No s) by A31, TARSKI:def 1;
then reconsider c1 = c1 as Surreal by SURREAL0:def 16;
A32: Unique_No s = [{c1},{c2}] by A28, A31;
not Unique_No s == 0_No by A23, SURREALO:50;
then A33: ( not L_ (Unique_No s) << {0_No} or not {(Unique_No s)} << R_ 0_No ) by A10, A9, SURREAL0:43, SURREALO:4;
then 0_No <= c1 by A31, SURREALO:21;
then A34: 0_No <= c2 by A32, SURREALO:4, SURREALO:22;
( c1 in L_ (Unique_No s) & c2 in R_ (Unique_No s) ) by A28, A31, TARSKI:def 1;
then ( c1 in (L_ (Unique_No s)) \/ (R_ (Unique_No s)) & c2 in (L_ (Unique_No s)) \/ (R_ (Unique_No s)) ) by XBOOLE_0:def 3;
then A35: ( born c1 in n + 1 & born c2 in n + 1 & n + 1 = Segm (n + 1) ) by A20, SURREALO:1;
then reconsider b1 = born c1, b2 = born c2 as Nat ;
( b1 < n + 1 & b2 < n + 1 ) by A35, NAT_1:44;
then ( b1 <= n & b2 <= n & n = Segm n ) by NAT_1:13;
then ( Segm b1 c= n & Segm b2 c= n ) by NAT_1:39;
then A36: ( c1 in Day b1 & Day b1 c= Day n & c2 in Day b2 & Day b2 c= Day n ) by SURREAL0:35, SURREAL0:def 18;
A37: uDyadic . n = uInt . n by Def5;
not c1 == uDyadic . n

proof

assume c1 == uDyadic . n ; :: thesis: contradiction
then uInt . n < c2 by A37, A32, SURREALO:4, SURREALO:22;
hence contradiction by Th2, A36; :: thesis: verum

end;

then consider d1 being Dyadic, x1, y1, p1 being Nat such that
A38: ( c1 == uDyadic . d1 & y1 < 2 |^ p1 & d1 = x1 + (y1 / (2 |^ p1)) & x1 + p1 < n ) by A36, A33, A31, SURREALO:21, A5;
y1 / (2 |^ p1) < 1 by A38, XREAL_1:189;
then A39: d1 < x1 + 1 by A38, XREAL_1:6;
A40: born (Unique_No s) = born_eq (Unique_No s) by SURREALO:48;

per cases ( c2 == uDyadic . n or ex d being Dyadic ex x, y, p being Nat st
( c2 == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n ) ) by A5, A34, A36;

suppose A41: c2 == uDyadic . n ; :: thesis: ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )

A42: x1 + 1 = n

proof

assume A43: x1 + 1 <> n ; :: thesis: contradiction
x1 <= x1 + p1 by NAT_1:11;
then x1 < n by A38, XXREAL_0:2;
then x1 + 1 <= n by NAT_1:13;
then x1 + 1 < n by A43, XXREAL_0:1;
then A44: ( 2 <= x1 + 2 & x1 + 2 = (x1 + 1) + 1 & (x1 + 1) + 1 <= n ) by NAT_1:11, NAT_1:13;
then reconsider N2 = n - 2 as Nat by NAT_1:21, XXREAL_0:2;
x1 + 2 <= N2 + 2 by A44;
then x1 <= N2 by XREAL_1:6;
then x1 + 1 <= N2 + 1 by XREAL_1:6;
then d1 < N2 + 1 by A39, XXREAL_0:2;
then c1 < uDyadic . (N2 + 1) by A38, SURREALO:4, Th24;
then A45: {c1} << {(uDyadic . (N2 + 1))} by SURREALO:21;
N2 + 1 < (N2 + 1) + 1 by NAT_1:13;
then uDyadic . (N2 + 1) < c2 by A41, SURREALO:4, Th24;
then {(uDyadic . (N2 + 1))} << {c2} by SURREALO:21;
then A46: born (Unique_No s) c= born (uDyadic . (N2 + 1)) by A45, A28, A31, A40, SURREALO:51;
uDyadic . (N2 + 1) = uInt . (N2 + 1) by Def5;
then Segm (n + 1) c= Segm (N2 + 1) by A46, A20, Th4;
then n + 1 <= N2 + 1 by NAT_1:39;
then n + 1 <= (N2 + 1) + 1 by NAT_1:13;
hence contradiction by NAT_1:13; :: thesis: verum

end;

(x1 + p1) + 1 <= n by A38, NAT_1:13;
then n + p1 <= n + 0 by A42;
then A47: ( p1 = 0 & 2 |^ 0 = 1 ) by XREAL_1:6, NEWTON:4;
then c1 == uDyadic . x1 by A38, NAT_1:14;
then A48: {c1} <==> {(uDyadic . x1)} by SURREALO:32;
A49: {c2} <==> {(uDyadic . (x1 + 1))} by A41, A42, SURREALO:32;
( uDyadic . x1 = uDyadic . (x1 / (2 |^ 0)) & uDyadic . (x1 + 1) = uDyadic . ((x1 + 1) / (2 |^ 0)) ) by A47;
then uDyadic . (((2 * x1) + 1) / (2 |^ (0 + 1))) = [{(uDyadic . x1)},{(uDyadic . (x1 + 1))}] by Def5;
then Unique_No s == uDyadic . (((2 * x1) + 1) / (2 |^ (0 + 1))) by SURREALO:29, A48, A49, A32;
then A50: s == uDyadic . (((2 * x1) + 1) / (2 |^ 1)) by SURREALO:4, A10;
A51: ((2 * x1) + 1) / (2 |^ 1) = x1 + (1 / (2 |^ 1)) ;
x1 + 1 < n + 1 by A42, NAT_1:13;
hence ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) by A50, A51; :: thesis: verum

end;

suppose ex d being Dyadic ex x, y, p being Nat st
( c2 == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n ) ; :: thesis: ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )

then consider d2 being Dyadic, x2, y2, p2 being Nat such that
A52: ( c2 == uDyadic . d2 & y2 < 2 |^ p2 & d2 = x2 + (y2 / (2 |^ p2)) & x2 + p2 < n ) ;
c1 < uDyadic . d2 by A32, SURREALO:4, SURREALO:22, A52;
then A53: uDyadic . d1 < uDyadic . d2 by A38, SURREALO:4;
y2 / (2 |^ p2) < 1 by A52, XREAL_1:189;
then A54: d2 < x2 + 1 by A52, XREAL_1:6;
A55: x1 + 0 <= d1 by A38, XREAL_1:6;

per cases ( x1 <> x2 or x1 = x2 ) ;

suppose A56: x1 <> x2 ; :: thesis: ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )

x1 < x2

proof

assume x2 <= x1 ; :: thesis: contradiction
then x2 < x1 by A56, XXREAL_0:1;
then x2 + 1 <= x1 by NAT_1:13;
then d2 < x1 by A54, XXREAL_0:2;
hence contradiction by A53, Th24, A55, XXREAL_0:2; :: thesis: verum

end;

then A57: x1 + 1 <= x2 by NAT_1:13;
x2 + 0 <= d2 by A52, XREAL_1:6;
then A58: x1 + 1 <= d2 by A57, XXREAL_0:2;
A59: d2 = x1 + 1

proof

assume d2 <> x1 + 1 ; :: thesis: contradiction
then x1 + 1 < d2 by A58, XXREAL_0:1;
then ( c1 < uDyadic . (x1 + 1) & uDyadic . (x1 + 1) < c2 ) by A38, SURREALO:4, A52, A39, Th24;
then ( {c1} << {(uDyadic . (x1 + 1))} & {(uDyadic . (x1 + 1))} << {c2} ) by SURREALO:21;
then ( born (Unique_No s) c= born (uDyadic . (x1 + 1)) & born (uDyadic . (x1 + 1)) = born (uInt . (x1 + 1)) & born (uInt . (x1 + 1)) = x1 + 1 ) by A40, SURREALO:51, A28, A31, Def5, Th4;
then Segm (n + 1) c= Segm (x1 + 1) by A19, A15, XBOOLE_1:1;
then n + 1 <= x1 + 1 by NAT_1:39;
then ( n + 1 <= x2 & x2 <= x2 + p2 ) by NAT_1:11, A57, XXREAL_0:2;
then n + 1 <= x2 + p2 by XXREAL_0:2;
hence contradiction by NAT_1:13, A52; :: thesis: verum

end;

y1 + 1 = 2 |^ p1

proof

A60: y1 + 1 <= 2 |^ p1 by A38, NAT_1:13;
assume y1 + 1 <> 2 |^ p1 ; :: thesis: contradiction
then A61: ( y1 < y1 + 1 & y1 + 1 < 2 |^ p1 ) by NAT_1:13, A60, XXREAL_0:1;
then ( y1 / (2 |^ p1) < (y1 + 1) / (2 |^ p1) & (y1 + 1) / (2 |^ p1) < (2 |^ p1) / (2 |^ p1) & (2 |^ p1) / (2 |^ p1) = 1 ) by XREAL_1:74, XCMPLX_1:60;
then ( d1 < x1 + ((y1 + 1) / (2 |^ p1)) & x1 + ((y1 + 1) / (2 |^ p1)) < x1 + 1 ) by A38, XREAL_1:6;
then ( d1 < x1 + ((y1 + 1) / (2 |^ p1)) & x1 + ((y1 + 1) / (2 |^ p1)) < d2 ) by A58, XXREAL_0:2;
then ( c1 < uDyadic . (x1 + ((y1 + 1) / (2 |^ p1))) & uDyadic . (x1 + ((y1 + 1) / (2 |^ p1))) < c2 ) by Th24, A52, A38, SURREALO:4;
then ( {c1} << {(uDyadic . (x1 + ((y1 + 1) / (2 |^ p1))))} & {(uDyadic . (x1 + ((y1 + 1) / (2 |^ p1))))} << {c2} ) by SURREALO:21;
then A62: n + 1 c= born (uDyadic . (x1 + ((y1 + 1) / (2 |^ p1)))) by A40, SURREALO:51, A20, A28, A31;
uDyadic . (x1 + ((y1 + 1) / (2 |^ p1))) in Day n by A38, A5, A61;
then born (uDyadic . (x1 + ((y1 + 1) / (2 |^ p1)))) c= n by SURREAL0:def 18;
then Segm (n + 1) c= Segm n by XBOOLE_1:1, A62;
then n + 1 <= n by NAT_1:39;
hence contradiction by NAT_1:13; :: thesis: verum

end;

then A63: (((x1 * (2 |^ p1)) + y1) + 1) / (2 |^ p1) = ((x1 + 1) * (2 |^ p1)) / (2 |^ p1)
.= (x1 + 1) * ((2 |^ p1) / (2 |^ p1)) by XCMPLX_1:74
.= d2 by A59, XCMPLX_1:88 ;
A64: d1 = ((x1 * (2 |^ p1)) + y1) / (2 |^ p1) by A38, XCMPLX_1:113;
A65: ( {c1} <==> {(uDyadic . d1)} & {c2} <==> {(uDyadic . d2)} ) by A52, A38, SURREALO:32;
uDyadic . (((((x1 * (2 |^ p1)) + y1) * 2) + 1) / (2 |^ (p1 + 1))) = [{(uDyadic . d1)},{(uDyadic . d2)}] by Def5, A64, A63;
then Unique_No s == uDyadic . (((((x1 * (2 |^ p1)) + y1) * 2) + 1) / (2 |^ (p1 + 1))) by A65, SURREALO:29, A32;
then A66: s == uDyadic . (((((x1 * (2 |^ p1)) + y1) * 2) + 1) / (2 |^ (p1 + 1))) by A10, SURREALO:4;
A67: 2 |^ (p1 + 1) = 2 * (2 |^ p1) by NEWTON:6;
then A68: ((((x1 * (2 |^ p1)) + y1) * 2) + 1) / (2 |^ (p1 + 1)) = ((x1 * (2 |^ (p1 + 1))) + ((y1 * 2) + 1)) / (2 |^ (p1 + 1))
.= x1 + (((y1 * 2) + 1) / (2 |^ (p1 + 1))) by XCMPLX_1:113 ;
y1 + 1 <= 2 |^ p1 by A38, NAT_1:13;
then ( ((2 * y1) + 1) + 1 = 2 * (y1 + 1) & 2 * (y1 + 1) <= 2 * (2 |^ p1) ) by XREAL_1:64;
then A69: (2 * y1) + 1 < 2 |^ (p1 + 1) by A67, NAT_1:13;
(x1 + p1) + 1 < n + 1 by A38, XREAL_1:6;
then x1 + (p1 + 1) < n + 1 ;
hence ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) by A66, A68, A69; :: thesis: verum

end;

suppose A70: x1 = x2 ; :: thesis: ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 )

then A71: y1 / (2 |^ p1) < y2 / (2 |^ p2) by A38, A52, A53, Th24, XREAL_1:6;
ex Y1, Y2, p3 being Nat st
( Y1 < Y2 & Y1 < 2 |^ p3 & Y2 < 2 |^ p3 & d1 = x1 + (Y1 / (2 |^ p3)) & d2 = x2 + (Y2 / (2 |^ p3)) & x2 + p3 < n )

proof

per cases ( p2 < p1 or p1 <= p2 ) ;

suppose p2 < p1 ; :: thesis: ex Y1, Y2, p3 being Nat st
( Y1 < Y2 & Y1 < 2 |^ p3 & Y2 < 2 |^ p3 & d1 = x1 + (Y1 / (2 |^ p3)) & d2 = x2 + (Y2 / (2 |^ p3)) & x2 + p3 < n )

then reconsider p = p1 - p2 as Nat by NAT_1:21;
take y1 ; :: thesis: ex Y2, p3 being Nat st
( y1 < Y2 & y1 < 2 |^ p3 & Y2 < 2 |^ p3 & d1 = x1 + (y1 / (2 |^ p3)) & d2 = x2 + (Y2 / (2 |^ p3)) & x2 + p3 < n )
take y3 = y2 * (2 |^ p); :: thesis: ex p3 being Nat st
( y1 < y3 & y1 < 2 |^ p3 & y3 < 2 |^ p3 & d1 = x1 + (y1 / (2 |^ p3)) & d2 = x2 + (y3 / (2 |^ p3)) & x2 + p3 < n )
take p3 = p1; :: thesis: ( y1 < y3 & y1 < 2 |^ p3 & y3 < 2 |^ p3 & d1 = x1 + (y1 / (2 |^ p3)) & d2 = x2 + (y3 / (2 |^ p3)) & x2 + p3 < n )
A72: 2 |^ (p2 + p) = (2 |^ p2) * (2 |^ p) by NEWTON:8;
y2 / (2 |^ p2) = y3 / (2 |^ p3) by A72, XCMPLX_1:91;
hence ( y1 < y3 & y1 < 2 |^ p3 & y3 < 2 |^ p3 & d1 = x1 + (y1 / (2 |^ p3)) & d2 = x2 + (y3 / (2 |^ p3)) & x2 + p3 < n ) by A70, A71, XREAL_1:72, A72, A52, XREAL_1:68, A38; :: thesis: verum

end;

suppose p1 <= p2 ; :: thesis: ex Y1, Y2, p3 being Nat st
( Y1 < Y2 & Y1 < 2 |^ p3 & Y2 < 2 |^ p3 & d1 = x1 + (Y1 / (2 |^ p3)) & d2 = x2 + (Y2 / (2 |^ p3)) & x2 + p3 < n )

then reconsider p = p2 - p1 as Nat by NAT_1:21;
take y3 = y1 * (2 |^ p); :: thesis: ex Y2, p3 being Nat st
( y3 < Y2 & y3 < 2 |^ p3 & Y2 < 2 |^ p3 & d1 = x1 + (y3 / (2 |^ p3)) & d2 = x2 + (Y2 / (2 |^ p3)) & x2 + p3 < n )
take y2 ; :: thesis: ex p3 being Nat st
( y3 < y2 & y3 < 2 |^ p3 & y2 < 2 |^ p3 & d1 = x1 + (y3 / (2 |^ p3)) & d2 = x2 + (y2 / (2 |^ p3)) & x2 + p3 < n )
take p3 = p2; :: thesis: ( y3 < y2 & y3 < 2 |^ p3 & y2 < 2 |^ p3 & d1 = x1 + (y3 / (2 |^ p3)) & d2 = x2 + (y2 / (2 |^ p3)) & x2 + p3 < n )
A73: 2 |^ (p1 + p) = (2 |^ p1) * (2 |^ p) by NEWTON:8;
y1 / (2 |^ p1) = y3 / (2 |^ p3) by A73, XCMPLX_1:91;
hence ( y3 < y2 & y3 < 2 |^ p3 & y2 < 2 |^ p3 & d1 = x1 + (y3 / (2 |^ p3)) & d2 = x2 + (y2 / (2 |^ p3)) & x2 + p3 < n ) by A73, A38, XREAL_1:68, A71, XREAL_1:72, A52; :: thesis: verum

end;

end;

end;

then consider Y1, Y2, p3 being Nat such that
A74: ( Y1 < Y2 & Y1 < 2 |^ p3 & Y2 < 2 |^ p3 & d1 = x1 + (Y1 / (2 |^ p3)) & d2 = x2 + (Y2 / (2 |^ p3)) & x2 + p3 < n ) ;
Y2 - Y1 > 0 by A74, XREAL_1:50;
then reconsider y = Y2 - Y1 as Nat ;
A75: y >= 1 + 0 by A74, XREAL_1:50, NAT_1:13;
A76: y = 1

proof

assume y <> 1 ; :: thesis: contradiction
then A77: y > 1 by A75, XXREAL_0:1;
( Y1 < Y1 + 1 & Y1 + 1 < Y1 + y & Y1 + y = Y2 ) by A77, NAT_1:13, XREAL_1:6;
then ( Y1 / (2 |^ p3) < (Y1 + 1) / (2 |^ p3) & (Y1 + 1) / (2 |^ p3) < Y2 / (2 |^ p3) ) by XREAL_1:74;
then ( uDyadic . d1 < uDyadic . (x1 + ((Y1 + 1) / (2 |^ p3))) & uDyadic . (x1 + ((Y1 + 1) / (2 |^ p3))) < uDyadic . d2 ) by Th24, A74, A70, XREAL_1:6;
then ( c1 < uDyadic . (x1 + ((Y1 + 1) / (2 |^ p3))) & uDyadic . (x1 + ((Y1 + 1) / (2 |^ p3))) < c2 ) by A52, A38, SURREALO:4;
then ( {c1} << {(uDyadic . (x1 + ((Y1 + 1) / (2 |^ p3))))} & {(uDyadic . (x1 + ((Y1 + 1) / (2 |^ p3))))} << {c2} ) by SURREALO:21;
then A78: n + 1 c= born (uDyadic . (x1 + ((Y1 + 1) / (2 |^ p3)))) by A40, SURREALO:51, A20, A28, A31;
Y1 + 1 <= Y2 by A74, NAT_1:13;
then Y1 + 1 < 2 |^ p3 by A74, XXREAL_0:2;
then uDyadic . (x1 + ((Y1 + 1) / (2 |^ p3))) in Day n by A5, A74, A70;
then born (uDyadic . (x1 + ((Y1 + 1) / (2 |^ p3)))) c= n by SURREAL0:def 18;
then Segm (n + 1) c= Segm n by A78, XBOOLE_1:1;
then n + 1 <= n by NAT_1:39;
hence contradiction by NAT_1:13; :: thesis: verum

end;

A79: ( {c1} <==> {(uDyadic . d1)} & {c2} <==> {(uDyadic . d2)} ) by A52, A38, SURREALO:32;
A80: ((x1 * (2 |^ p3)) + Y1) / (2 |^ p3) = d1 by A74, XCMPLX_1:113;
A81: d2 = ((x1 * (2 |^ p3)) + Y2) / (2 |^ p3) by A70, A74, XCMPLX_1:113
.= (((x1 * (2 |^ p3)) + Y1) + 1) / (2 |^ p3) by A76 ;
uDyadic . (((((x1 * (2 |^ p3)) + Y1) * 2) + 1) / (2 |^ (p3 + 1))) = [{(uDyadic . d1)},{(uDyadic . d2)}] by Def5, A80, A81;
then Unique_No s == uDyadic . (((((x1 * (2 |^ p3)) + Y1) * 2) + 1) / (2 |^ (p3 + 1))) by A79, SURREALO:29, A32;
then A82: s == uDyadic . (((((x1 * (2 |^ p3)) + Y1) * 2) + 1) / (2 |^ (p3 + 1))) by A10, SURREALO:4;
A83: 2 |^ (p3 + 1) = 2 * (2 |^ p3) by NEWTON:6;
then A84: ((((x1 * (2 |^ p3)) + Y1) * 2) + 1) / (2 |^ (p3 + 1)) = ((x1 * (2 |^ (p3 + 1))) + ((Y1 * 2) + 1)) / (2 |^ (p3 + 1))
.= x1 + (((Y1 * 2) + 1) / (2 |^ (p3 + 1))) by XCMPLX_1:113 ;
Y1 + 1 <= 2 |^ p3 by A74, NAT_1:13;
then ( ((2 * Y1) + 1) + 1 = 2 * (Y1 + 1) & 2 * (Y1 + 1) <= 2 * (2 |^ p3) ) by XREAL_1:64;
then A85: (2 * Y1) + 1 < 2 |^ (p3 + 1) by A83, NAT_1:13;
(x1 + p3) + 1 < n + 1 by A70, A74, XREAL_1:6;
then x1 + (p3 + 1) < n + 1 ;
hence ex d being Dyadic ex x, y, p being Nat st
( s == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n + 1 ) by A82, A84, A85; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

let x, y, p be Nat; :: thesis: ( y < 2 |^ p & x + p < n + 1 implies ( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day (n + 1) ) )
assume A86: ( y < 2 |^ p & x + p < n + 1 ) ; :: thesis: ( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day (n + 1) )
set d = x + (y / (2 |^ p));
A87: x + p <= n by A86, NAT_1:13;

per cases ( p = 0 or ( y is even & p <> 0 ) or ( y is odd & p <> 0 ) ) ;

suppose A88: p = 0 ; :: thesis: ( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day (n + 1) )

then 2 |^ p = 1 by NEWTON:4;
then y = 0 by A86, NAT_1:14;
then A89: uDyadic . (x + (y / (2 |^ p))) = uInt . x by Def5;
( 0 < x or 0 = x ) ;
then A90: ( uInt . 0 < uInt . x or uInt . 0 = uInt . x ) by Lm4;
Segm x c= Segm (n + 1) by A88, A86, NAT_1:39;
then ( uInt . x in Day x & Day x c= Day (n + 1) ) by Th1, SURREAL0:35;
hence ( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day (n + 1) ) by A90, Def1, A89; :: thesis: verum

end;

suppose A91: ( y is even & p <> 0 ) ; :: thesis: ( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day (n + 1) )

then consider z being Nat such that
A92: y = 2 * z by ABIAN:def 2;
reconsider p1 = p - 1 as Nat by NAT_1:20, A91;
p = p1 + 1 ;
then A93: 2 |^ p = 2 * (2 |^ p1) by NEWTON:6;
then A94: y / (2 |^ p) = z / (2 |^ p1) by A92, XCMPLX_1:91;
A95: z < 2 |^ p1 by A93, A92, A86, XREAL_1:64;
(x + p1) + 1 <= n by A86, NAT_1:13;
then x + p1 < n by NAT_1:13;
then ( 0_No <= uDyadic . (x + (z / (2 |^ p1))) & uDyadic . (x + (z / (2 |^ p1))) in Day n ) by A5, A95;
hence ( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day (n + 1) ) by A8, A94; :: thesis: verum

end;

suppose A96: ( y is odd & p <> 0 ) ; :: thesis: ( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day (n + 1) )

then consider z being Nat such that
A97: y = (2 * z) + 1 by ABIAN:9;
reconsider p1 = p - 1 as Nat by NAT_1:20, A96;
set SD = uDyadic . (((x * (2 |^ p1)) + z) / (2 |^ p1));
set SD1 = uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1));
p = p1 + 1 ;
then A98: 2 |^ p = 2 * (2 |^ p1) by NEWTON:6;
then A99: (x * (2 |^ p)) + y = (2 * ((x * (2 |^ p1)) + z)) + 1 by A97;
x + (y / (2 |^ p)) = ((2 * ((x * (2 |^ p1)) + z)) + 1) / (2 |^ (p1 + 1)) by A99, XCMPLX_1:113;
then A100: uDyadic . (x + (y / (2 |^ p))) = [{(uDyadic . (((x * (2 |^ p1)) + z) / (2 |^ p1)))},{(uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1)))}] by Def5;
A101: z < 2 |^ p1 by XREAL_1:64, A98, A97, A86, NAT_1:13;
(x + p1) + 1 <= n by A86, NAT_1:13;
then A102: x + p1 < n by NAT_1:13;
((x * (2 |^ p1)) + z) / (2 |^ p1) = x + (z / (2 |^ p1)) by XCMPLX_1:113;
then A103: uDyadic . (((x * (2 |^ p1)) + z) / (2 |^ p1)) in Day n by A5, A101, A102;
((2 * z) + 1) + 1 <= 2 * (2 |^ p1) by A98, A97, A86, NAT_1:13;
then 2 * (z + 1) <= 2 * (2 |^ p1) ;
then A104: z + 1 <= 2 |^ p1 by XREAL_1:68;
A105: uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1)) in Day n

proof

((x * (2 |^ p1)) + z) + 1 = (x * (2 |^ p1)) + (z + 1) ;
then A106: (((x * (2 |^ p1)) + z) + 1) / (2 |^ p1) = x + ((z + 1) / (2 |^ p1)) by XCMPLX_1:113;

per cases ( z + 1 = 2 |^ p1 or z + 1 < 2 |^ p1 ) by A104, XXREAL_0:1;

suppose z + 1 = 2 |^ p1 ; :: thesis: uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1)) in Day n

then (((x * (2 |^ p1)) + z) + 1) / (2 |^ p1) = x + 1 by A106, XCMPLX_1:60;
then A107: uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1)) = uInt . (x + 1) by Def5;
( x + 1 <= (x + 1) + p1 & (x + 1) + p1 = x + p ) by NAT_1:11;
then Segm (x + 1) c= Segm n by NAT_1:39, A87, XXREAL_0:2;
then ( uInt . (x + 1) in Day (x + 1) & Day (x + 1) c= Day n ) by SURREAL0:35, Th1;
hence uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1)) in Day n by A107; :: thesis: verum

end;

suppose z + 1 < 2 |^ p1 ; :: thesis: uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1)) in Day n

hence uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1)) in Day n by A102, A5, A106; :: thesis: verum

end;

end;

end;

A108: {(uDyadic . (((x * (2 |^ p1)) + z) / (2 |^ p1)))} << {(uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1)))} by SURREALO:21, SURREALO:22, A100;
for o being object st o in {(uDyadic . (((x * (2 |^ p1)) + z) / (2 |^ p1)))} \/ {(uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1)))} holds
ex O being Ordinal st
( O in n + 1 & o in Day O )

proof

let o be object ; :: thesis: ( o in {(uDyadic . (((x * (2 |^ p1)) + z) / (2 |^ p1)))} \/ {(uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1)))} implies ex O being Ordinal st
( O in n + 1 & o in Day O ) )
assume o in {(uDyadic . (((x * (2 |^ p1)) + z) / (2 |^ p1)))} \/ {(uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1)))} ; :: thesis: ex O being Ordinal st
( O in n + 1 & o in Day O )
then ( o in {(uDyadic . (((x * (2 |^ p1)) + z) / (2 |^ p1)))} or o in {(uDyadic . ((((x * (2 |^ p1)) + z) + 1) / (2 |^ p1)))} ) by XBOOLE_0:def 3;
then o in Day n by A103, A105, TARSKI:def 1;
hence ex O being Ordinal st
( O in n + 1 & o in Day O ) by A7; :: thesis: verum

end;

hence ( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day (n + 1) ) by A6, Th24, A100, SURREAL0:46, A108; :: thesis: verum

end;

end;

end;

A109: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A4);
thus ( 0_No <= z & z in Day n & not z == uDyadic . n implies ex x, y, p being Nat st
( z == uDyadic . (x + (y / (2 |^ p))) & y < 2 |^ p & x + p < n ) ) :: thesis: for x, y, p being Nat st y < 2 |^ p & x + p < n holds
( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day n )

proof

assume ( 0_No <= z & z in Day n & not z == uDyadic . n ) ; :: thesis: ex x, y, p being Nat st
( z == uDyadic . (x + (y / (2 |^ p))) & y < 2 |^ p & x + p < n )
then ex d being Dyadic ex x, y, p being Nat st
( z == uDyadic . d & y < 2 |^ p & d = x + (y / (2 |^ p)) & x + p < n ) by A109;
hence ex x, y, p being Nat st
( z == uDyadic . (x + (y / (2 |^ p))) & y < 2 |^ p & x + p < n ) ; :: thesis: verum

end;

thus for x, y, p being Nat st y < 2 |^ p & x + p < n holds
( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day n ) by A109; :: thesis: verum