let p be Nat; :: thesis: ( ( for d being Dyadic holds uDyadic . d is Surreal ) & ( for i, j being Integer
for si, sj being Surreal st si = uDyadic . (i / (2 |^ p)) & sj = uDyadic . (j / (2 |^ p)) holds
( i < j iff si < sj ) ) )
defpred S₁[ Nat] means ( ( for d being Dyadic st d in DYADIC $1 holds
uDyadic . d is Surreal ) & ( for i, j being Integer
for si, sj being Surreal st si = uDyadic . (i / (2 |^ $1)) & sj = uDyadic . (j / (2 |^ $1)) holds
( i < j iff si < sj ) ) );
A1: S₁[ 0 ]

proof

A2: 2 |^ 0 = 1 by NEWTON:4;
thus for d being Dyadic st d in DYADIC 0 holds
uDyadic . d is Surreal :: thesis: for i, j being Integer
for si, sj being Surreal st si = uDyadic . (i / (2 |^ 0)) & sj = uDyadic . (j / (2 |^ 0)) holds
( i < j iff si < sj )

proof

let d be Dyadic; :: thesis: ( d in DYADIC 0 implies uDyadic . d is Surreal )
assume d in DYADIC 0 ; :: thesis: uDyadic . d is Surreal
then reconsider i = d as Integer by Th21;
uDyadic . d = uInt . i by Def5;
hence uDyadic . d is Surreal ; :: thesis: verum

end;

let i, j be Integer; :: thesis: for si, sj being Surreal st si = uDyadic . (i / (2 |^ 0)) & sj = uDyadic . (j / (2 |^ 0)) holds
( i < j iff si < sj )
let si, sj be Surreal; :: thesis: ( si = uDyadic . (i / (2 |^ 0)) & sj = uDyadic . (j / (2 |^ 0)) implies ( i < j iff si < sj ) )
assume A3: ( si = uDyadic . (i / (2 |^ 0)) & sj = uDyadic . (j / (2 |^ 0)) ) ; :: thesis: ( i < j iff si < sj )
( si = uInt . i & sj = uInt . j ) by A2, A3, Def5;
hence ( i < j iff si < sj ) by Th9; :: 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;
thus for d being Dyadic st d in DYADIC (n + 1) holds
uDyadic . d is Surreal :: thesis: for i, j being Integer
for si, sj being Surreal st si = uDyadic . (i / (2 |^ (n + 1))) & sj = uDyadic . (j / (2 |^ (n + 1))) holds
( i < j iff si < sj )

proof

let d be Dyadic; :: thesis: ( d in DYADIC (n + 1) implies uDyadic . d is Surreal )
assume A6: d in DYADIC (n + 1) ; :: thesis: uDyadic . d is Surreal

per cases ( d in DYADIC n or not d in DYADIC n ) ;

suppose d in DYADIC n ; :: thesis: uDyadic . d is Surreal

hence uDyadic . d is Surreal by A5; :: thesis: verum

end;

suppose not d in DYADIC n ; :: thesis: uDyadic . d is Surreal

then d in (DYADIC (n + 1)) \ (DYADIC n) by A6, XBOOLE_0:def 5;
then consider i being Integer such that
A7: d = ((2 * i) + 1) / (2 |^ (n + 1)) by Th20;
( i / (2 |^ n) in DYADIC n & (i + 1) / (2 |^ n) in DYADIC n ) by Def4;
then reconsider si = uDyadic . (i / (2 |^ n)), si1 = uDyadic . ((i + 1) / (2 |^ n)) as Surreal by A5;
i + 0 < i + 1 by XREAL_1:6;
then A8: si < si1 by A5;
uDyadic . d = [{si},{si1}] by Def5, A7;
hence uDyadic . d is Surreal by A8, SURREALO:22; :: thesis: verum

end;

end;

end;

let i, j be Integer; :: thesis: for si, sj being Surreal st si = uDyadic . (i / (2 |^ (n + 1))) & sj = uDyadic . (j / (2 |^ (n + 1))) holds
( i < j iff si < sj )
let si, sj be Surreal; :: thesis: ( si = uDyadic . (i / (2 |^ (n + 1))) & sj = uDyadic . (j / (2 |^ (n + 1))) implies ( i < j iff si < sj ) )
assume A9: ( si = uDyadic . (i / (2 |^ (n + 1))) & sj = uDyadic . (j / (2 |^ (n + 1))) ) ; :: thesis: ( i < j iff si < sj )
A10: 2 |^ (n + 1) = 2 * (2 |^ n) by NEWTON:6;

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

suppose i is even ; :: thesis: ( i < j iff si < sj )

then consider i1 being Integer such that
A11: i = 2 * i1 by ABIAN:11;
A12: i / (2 |^ (n + 1)) = i1 / (2 |^ n) by A11, A10, XCMPLX_1:91;

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

suppose j is even ; :: thesis: ( i < j iff si < sj )

then consider j1 being Integer such that
A13: j = 2 * j1 by ABIAN:11;
A14: j / (2 |^ (n + 1)) = j1 / (2 |^ n) by A13, A10, XCMPLX_1:91;
( i1 < j1 iff si < sj ) by A12, A14, A9, A5;
hence ( i < j iff si < sj ) by A11, A13, XREAL_1:64, XREAL_1:68; :: thesis: verum

end;

suppose j is odd ; :: thesis: ( i < j iff si < sj )

then consider j1 being Integer such that
A15: j = (2 * j1) + 1 by ABIAN:1;
( j1 / (2 |^ n) in DYADIC n & (j1 + 1) / (2 |^ n) in DYADIC n ) by Def4;
then reconsider Dn = uDyadic . (j1 / (2 |^ n)), D1n = uDyadic . ((j1 + 1) / (2 |^ n)) as Surreal by A5;
A16: sj = [{Dn},{D1n}] by A15, A9, Def5;
A17: ( L_ sj << {sj} & {sj} << R_ sj ) by SURREALO:11;
thus ( i < j implies si < sj ) :: thesis: ( si < sj implies i < j )

proof

assume i < j ; :: thesis: si < sj
then i1 <= j1 by XREAL_1:68, A11, A15, INT_1:7;
then not Dn < si by A5, A12, A9;
hence si < sj by A16, SURREALO:4, SURREALO:21, A17; :: thesis: verum

end;

assume A18: ( si < sj & j <= i ) ; :: thesis: contradiction
then (2 * j1) + 1 < 2 * i1 by A11, A15, XXREAL_0:1;
then ( 2 * (j1 + 1) = ((2 * j1) + 1) + 1 & ((2 * j1) + 1) + 1 <= 2 * i1 ) by INT_1:7;
then not i1 < j1 + 1 by XREAL_1:68;
then D1n <= si by A5, A12, A9;
then D1n <= sj by A18, SURREALO:4;
hence contradiction by A16, SURREALO:21, A17; :: thesis: verum

end;

end;

end;

suppose i is odd ; :: thesis: ( i < j iff si < sj )

then consider i1 being Integer such that
A19: i = (2 * i1) + 1 by ABIAN:1;
( i1 / (2 |^ n) in DYADIC n & (i1 + 1) / (2 |^ n) in DYADIC n ) by Def4;
then reconsider Sn = uDyadic . (i1 / (2 |^ n)), S1n = uDyadic . ((i1 + 1) / (2 |^ n)) as Surreal by A5;
A20: si = [{Sn},{S1n}] by A19, A9, Def5;
A21: ( L_ si << {si} & {si} << R_ si ) by SURREALO:11;

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

suppose j is even ; :: thesis: ( i < j iff si < sj )

then consider j1 being Integer such that
A22: j = 2 * j1 by ABIAN:11;
A23: j / (2 |^ (n + 1)) = j1 / (2 |^ n) by A22, A10, XCMPLX_1:91;
thus ( i < j implies si < sj ) :: thesis: ( si < sj implies i < j )

proof

assume i < j ; :: thesis: si < sj
then ( 2 * (i1 + 1) = ((2 * i1) + 1) + 1 & ((2 * i1) + 1) + 1 <= 2 * j1 ) by A19, A22, INT_1:7;
then not j1 < i1 + 1 by XREAL_1:68;
then not sj < S1n by A5, A9, A23;
hence si < sj by A21, A20, SURREALO:4, SURREALO:21; :: thesis: verum

end;

assume A24: ( si < sj & j <= i ) ; :: thesis: contradiction
then 2 * j1 < (2 * i1) + 1 by A19, A22, XXREAL_0:1;
then j1 <= i1 by XREAL_1:68, INT_1:7;
then sj <= Sn by A5, A9, A23;
then sj <= si by A21, A20, SURREALO:21, SURREALO:4;
hence contradiction by A24; :: thesis: verum

end;

suppose j is odd ; :: thesis: ( i < j iff si < sj )

then consider j1 being Integer such that
A25: j = (2 * j1) + 1 by ABIAN:1;
( j1 / (2 |^ n) in DYADIC n & (j1 + 1) / (2 |^ n) in DYADIC n ) by Def4;
then reconsider Dn = uDyadic . (j1 / (2 |^ n)), D1n = uDyadic . ((j1 + 1) / (2 |^ n)) as Surreal by A5;
A26: sj = [{Dn},{D1n}] by A25, A9, Def5;
A27: ( L_ sj << {sj} & {sj} << R_ sj ) by SURREALO:11;
thus ( i < j implies si < sj ) :: thesis: ( si < sj implies i < j )

proof

assume i < j ; :: thesis: si < sj
then ( 2 * (i1 + 1) = ((2 * i1) + 1) + 1 & ((2 * i1) + 1) + 1 <= (2 * j1) + 1 ) by A19, A25, INT_1:7;
then 2 * (i1 + 1) < (2 * j1) + 1 by XXREAL_0:1;
then i1 + 1 <= j1 by XREAL_1:68, INT_1:7;
then S1n <= Dn by A5;
then S1n <= sj by A26, SURREALO:4, SURREALO:21, A27;
hence si < sj by A21, A20, SURREALO:4, SURREALO:21; :: thesis: verum

end;

assume A28: ( si < sj & j <= i ) ; :: thesis: contradiction
then 2 * j1 <= 2 * i1 by A19, A25, XREAL_1:6;
then A29: j1 <= i1 by XREAL_1:68;
j <> i by A9, A28, SURREALO:3;
then j1 < i1 by A25, A19, A29, XXREAL_0:1;
then j1 + 1 <= i1 by INT_1:7;
then D1n <= Sn by A5;
then D1n <= si by A21, A20, SURREALO:4, SURREALO:21;
then sj <= si by A27, A26, SURREALO:21, SURREALO:4;
hence contradiction by A28; :: thesis: verum

end;

end;

end;

end;

end;

A30: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A4);
thus for d being Dyadic holds uDyadic . d is Surreal :: thesis: for i, j being Integer
for si, sj being Surreal st si = uDyadic . (i / (2 |^ p)) & sj = uDyadic . (j / (2 |^ p)) holds
( i < j iff si < sj )

proof

let d be Dyadic; :: thesis: uDyadic . d is Surreal
consider i being Integer, n being Nat such that
A31: d = i / (2 |^ n) by Th18;
d in DYADIC n by A31, Def4;
hence uDyadic . d is Surreal by A30; :: thesis: verum

end;

thus for i, j being Integer
for si, sj being Surreal st si = uDyadic . (i / (2 |^ p)) & sj = uDyadic . (j / (2 |^ p)) holds
( i < j iff si < sj ) by A30; :: thesis: verum