defpred S
1[
Ordinal,
Surreal,
Surreal]
means (
(born $2) (+) (born $3) c= $1 implies $2
* $3
= $3
* $2 );
defpred S
2[
Ordinal,
Surreal,
Surreal]
means (
(born $2) (+) (born $3) c= $1 implies $2
* $3 is
Surreal );
defpred S
3[
Ordinal,
Surreal,
Surreal,
Surreal]
means for x1y, x2y being
Surreal st
(born $2) (+) (born $4) c= $1 &
(born $3) (+) (born $4) c= $1 & $2
== $3 & x1y
= $2
* $4 & x2y
= $3
* $4 holds
x1y
== x2y;
defpred S
4[
Ordinal,
Surreal,
Surreal,
Surreal,
Surreal]
means for x1y2, x2y1, x1y1, x2y2 being
Surreal st
(born $2) (+) (born $4) c= $1 &
(born $3) (+) (born $4) c= $1 &
(born $2) (+) (born $5) c= $1 &
(born $3) (+) (born $5) c= $1 & x1y1
= $2
* $4 & x1y2
= $2
* $5 & x2y1
= $3
* $4 & x2y2
= $3
* $5 & $2
< $3 & $4
< $5 holds
x1y2
+ x2y1
< x1y1
+ x2y2;
defpred S
5[
Ordinal,
Surreal,
Surreal,
Surreal]
means ( $3
< $4 implies ( ( for x being
Surreal st x
in L_ $2 holds
S
4[$1,x,$2,$3,$4] ) & ( for x being
Surreal st x
in R_ $2 holds
S
4[$1,$2,x,$3,$4] ) ) );
defpred S
6[
Ordinal]
means for x, y being
Surreal holds S
1[$1,x,y];
defpred S
7[
Ordinal]
means for x, y being
Surreal holds S
2[$1,x,y];
defpred S
8[
Ordinal]
means for x1, x2, y being
Surreal holds S
3[$1,x1,x2,y];
defpred S
9[
Ordinal]
means for x1, x2, y1, y2 being
Surreal holds S
4[$1,x1,x2,y1,y2];
defpred S
10[
Ordinal]
means ( S
6[$1] & S
7[$1] & S
8[$1] & S
9[$1] );
A1:
for D being Ordinal st ( for C being Ordinal st C in D holds
S10[C] ) holds
S10[D]
proof
let D be
Ordinal;
( ( for C being Ordinal st C in D holds
S10[C] ) implies S10[D] )
assume A2:
for C being Ordinal st C in D holds
S10[C]
;
S10[D]
thus A3:
for x, y being Surreal holds S1[D,x,y]
( S7[D] & S8[D] & S9[D] )
proof
A4:
for x, y being Surreal st (born x) (+) (born y) c= D holds
for X, Y being surreal-membered set st X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) holds
comp (X,x,y,Y) c= comp (Y,y,x,X)
proof
let x, y be
Surreal;
( (born x) (+) (born y) c= D implies for X, Y being surreal-membered set st X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) holds
comp (X,x,y,Y) c= comp (Y,y,x,X) )
assume A5:
(born x) (+) (born y) c= D
;
for X, Y being surreal-membered set st X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) holds
comp (X,x,y,Y) c= comp (Y,y,x,X)
let X, Y be
surreal-membered set ;
( X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) implies comp (X,x,y,Y) c= comp (Y,y,x,X) )
assume A6:
( X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) )
;
comp (X,x,y,Y) c= comp (Y,y,x,X)
let a be
object ;
TARSKI:def 3 ( not a in comp (X,x,y,Y) or a in comp (Y,y,x,X) )
assume
a in comp (X,x,y,Y)
;
a in comp (Y,y,x,X)
then consider x1, y1 being
Surreal such that A7:
( a = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y )
by Def14;
A8:
( (born x1) (+) (born y1) in (born x1) (+) (born y) & (born x) (+) (born y1) in (born x) (+) (born y) & (born x1) (+) (born y) in (born x) (+) (born y) )
by SURREALO:1, A6, A7, ORDINAL7:94;
then
(born x1) (+) (born y1) in (born x) (+) (born y)
by ORDINAL1:10;
then A9:
( x1 * y1 = y1 * x1 & x * y1 = y1 * x & x1 * y = y * x1 )
by A8, A2, A5;
reconsider yx1 = y
* x1, y1x = y1
* x as
Surreal by A8, A2, A5;
(y * x1) +' (y1 * x) =
y1x
+ yx1
by Def11
.=
(y1 * x) +' (y * x1)
;
hence
a in comp (Y,y,x,X)
by A7, Def14, A9;
verum
end;
A10:
for x, y being Surreal st (born x) (+) (born y) c= D holds
for X, Y being surreal-membered set st X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) holds
comp (X,x,y,Y) = comp (Y,y,x,X)
proof
let x, y be
Surreal;
( (born x) (+) (born y) c= D implies for X, Y being surreal-membered set st X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) holds
comp (X,x,y,Y) = comp (Y,y,x,X) )
assume A11:
(born x) (+) (born y) c= D
;
for X, Y being surreal-membered set st X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) holds
comp (X,x,y,Y) = comp (Y,y,x,X)
let X, Y be
surreal-membered set ;
( X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) implies comp (X,x,y,Y) = comp (Y,y,x,X) )
assume A12:
( X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) )
;
comp (X,x,y,Y) = comp (Y,y,x,X)
( comp (X,x,y,Y) c= comp (Y,y,x,X) & comp (Y,y,x,X) c= comp (X,x,y,Y) )
by A11, A12, A4;
hence
comp (X,x,y,Y) = comp (Y,y,x,X)
by XBOOLE_0:def 10;
verum
end;
let x, y be
Surreal;
S1[D,x,y]
assume A13:
(born x) (+) (born y) c= D
;
x * y = y * x
( L_ x c= (L_ x) \/ (R_ x) & R_ x c= (L_ x) \/ (R_ x) & L_ y c= (L_ y) \/ (R_ y) & R_ y c= (L_ y) \/ (R_ y) )
by XBOOLE_1:7;
then A14:
( comp ((L_ x),x,y,(L_ y)) = comp ((L_ y),y,x,(L_ x)) & comp ((R_ x),x,y,(R_ y)) = comp ((R_ y),y,x,(R_ x)) & comp ((L_ x),x,y,(R_ y)) = comp ((R_ y),y,x,(L_ x)) & comp ((R_ x),x,y,(L_ y)) = comp ((L_ y),y,x,(R_ x)) )
by A10, A13;
x
* y =
[((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))),((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))))]
by Th50
.=
y
* x
by A14, Th50
;
hence
x * y = y * x
;
verum
end;
thus
for x, y being Surreal holds S2[D,x,y]
( S8[D] & S9[D] )
proof
let x, y be
Surreal;
S2[D,x,y]
assume A15:
(born x) (+) (born y) c= D
;
x * y is Surreal
set CC =
((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))) \/ ((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))));
A16:
for X, Y being surreal-membered set st X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) holds
comp (X,x,y,Y) is surreal-membered
proof
let X, Y be
surreal-membered set ;
( X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) implies comp (X,x,y,Y) is surreal-membered )
assume A17:
( X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) )
;
comp (X,x,y,Y) is surreal-membered
let z be
object ;
SURREAL0:def 16 ( not z in comp (X,x,y,Y) or z is surreal )
assume
z in comp (X,x,y,Y)
;
z is surreal
then consider x1, y1 being
Surreal such that A18:
( z = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y )
by Def14;
A19:
( (born x1) (+) (born y1) in (born x1) (+) (born y) & (born x) (+) (born y1) in (born x) (+) (born y) & (born x1) (+) (born y) in (born x) (+) (born y) )
by A17, SURREALO:1, A18, ORDINAL7:94;
then
(born x1) (+) (born y1) in (born x) (+) (born y)
by ORDINAL1:10;
then reconsider x1y = x1
* y, xy1 = x
* y1, x1y1 = x1
* y1 as
Surreal by A19, A15, A2;
thus
z is surreal
by A18;
verum
end;
A20:
( L_ x c= (L_ x) \/ (R_ x) & R_ x c= (L_ x) \/ (R_ x) & L_ y c= (L_ y) \/ (R_ y) & R_ y c= (L_ y) \/ (R_ y) )
by XBOOLE_1:7;
defpred S
11[
object ,
object ]
means ( $1 is
Surreal & ( for z being
Surreal st z
= $1 holds
$2
= born z ) );
A21:
for x, y, z being object st S11[x,y] & S11[x,z] holds
y = z
proof
let x, y, z be
object ;
( S11[x,y] & S11[x,z] implies y = z )
assume A22:
( S11[x,y] & S11[x,z] )
;
y = z
reconsider x = x as
Surreal by A22;
thus y =
born x
by A22
.=
z
by A22
;
verum
end;
consider OO being
set such that A23:
for z being object holds
( z in OO iff ex y being object st
( y in ((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))) \/ ((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y)))) & S11[y,z] ) )
from TARSKI_0:sch 1(A21);
for x being set st x in OO holds
x is ordinal
proof
let x be
set ;
( x in OO implies x is ordinal )
assume
x in OO
;
x is ordinal
then consider y being
object such that A24:
( y in ((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))) \/ ((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y)))) & S11[y,x] )
by A23;
reconsider y = y as
Surreal by A24;
x = born y
by A24;
hence
x is ordinal
;
verum
end;
then
OO is ordinal-membered
by ORDINAL6:1;
then reconsider U =
union OO as
Ordinal ;
A25:
for o being object st o in ((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))) \/ ((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y)))) holds
ex O being Ordinal st
( O in succ U & o in Day O )
proof
let o be
object ;
( o in ((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))) \/ ((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y)))) implies ex O being Ordinal st
( O in succ U & o in Day O ) )
assume A26:
o in ((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))) \/ ((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))))
;
ex O being Ordinal st
( O in succ U & o in Day O )
A27:
( comp ((L_ x),x,y,(L_ y)) is surreal-membered & comp ((R_ x),x,y,(R_ y)) is surreal-membered & comp ((L_ x),x,y,(R_ y)) is surreal-membered & comp ((R_ x),x,y,(L_ y)) is surreal-membered )
by A16, A20;
( o in (comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y))) or o in (comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))) )
by A26, XBOOLE_0:def 3;
then
( o in comp ((L_ x),x,y,(L_ y)) or o in comp ((R_ x),x,y,(R_ y)) or o in comp ((L_ x),x,y,(R_ y)) or o in comp ((R_ x),x,y,(L_ y)) )
by XBOOLE_0:def 3;
then reconsider o = o as
Surreal by A27;
S11[o, born o]
;
then
born o c= U
by A23, A26, ZFMISC_1:74;
then A28:
born o in succ U
by ORDINAL1:6, ORDINAL1:12;
o in Day (born o)
by SURREAL0:def 18;
hence
ex O being Ordinal st
( O in succ U & o in Day O )
by A28;
verum
end;
(comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y))) << (comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y)))
proof
let l, r be
Surreal;
SURREAL0:def 20 ( not l in (comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y))) or not r in (comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))) or not r <= l )
assume A29:
( l in (comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y))) & r in (comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))) )
;
not r <= l
per cases
( ( l in comp ((L_ x),x,y,(L_ y)) & r in comp ((L_ x),x,y,(R_ y)) ) or ( l in comp ((R_ x),x,y,(R_ y)) & r in comp ((R_ x),x,y,(L_ y)) ) or ( l in comp ((L_ x),x,y,(L_ y)) & r in comp ((R_ x),x,y,(L_ y)) ) or ( l in comp ((R_ x),x,y,(R_ y)) & r in comp ((L_ x),x,y,(R_ y)) ) )
by A29, XBOOLE_0:def 3;
suppose A30:
( l in comp ((L_ x),x,y,(L_ y)) & r in comp ((L_ x),x,y,(R_ y)) )
;
not r <= l
then consider xL1, yL being
Surreal such that A31:
( l = ((xL1 * y) +' (x * yL)) +' (-' (xL1 * yL)) & xL1 in L_ x & yL in L_ y )
by Def14;
consider xL2, yR being
Surreal such that A32:
( r = ((xL2 * y) +' (x * yR)) +' (-' (xL2 * yR)) & xL2 in L_ x & yR in R_ y )
by Def14, A30;
( xL1 in (L_ x) \/ (R_ x) & xL2 in (L_ x) \/ (R_ x) )
by A31, A32, XBOOLE_0:def 3;
then A33:
( (born xL1) (+) (born y) in (born x) (+) (born y) & (born xL2) (+) (born y) in (born x) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
then reconsider xL1y = xL1
* y, xL2y = xL2
* y as
Surreal by A15, A2;
set BL =
((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y));
A34:
((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) in (born x) (+) (born y)
by A33, ORDINAL3:12;
A35:
( (born xL1) (+) (born y) c= ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) & (born xL2) (+) (born y) c= ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) )
by XBOOLE_1:7;
A36:
( xL1 == xL2 implies xL1y == xL2y )
by A35, A34, A15, A2;
A37:
( yR in (L_ y) \/ (R_ y) & yL in (L_ y) \/ (R_ y) )
by A31, A32, XBOOLE_0:def 3;
then A38:
( (born xL1) (+) (born yL) in (born xL1) (+) (born y) & (born xL1) (+) (born yR) in (born xL1) (+) (born y) & (born xL2) (+) (born yL) in (born xL2) (+) (born y) & (born xL2) (+) (born yR) in (born xL2) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
then
( (born xL1) (+) (born yL) in (born x) (+) (born y) & (born xL1) (+) (born yR) in (born x) (+) (born y) & (born xL2) (+) (born yR) in (born x) (+) (born y) & (born xL2) (+) (born yL) in (born x) (+) (born y) )
by A33, ORDINAL1:10;
then reconsider xL1yR = xL1
* yR, xL2yR = xL2
* yR, xL2yL = xL2
* yL, xL1yL = xL1
* yL as
Surreal by A15, A2;
set BY =
((born x) (+) (born yL)) \/ ((born x) (+) (born yR));
A39:
( (born x) (+) (born yL) in (born x) (+) (born y) & (born x) (+) (born yR) in (born x) (+) (born y) )
by A37, SURREALO:1, ORDINAL7:94;
then reconsider xyL = x
* yL, xyR = x
* yR as
Surreal by A15, A2;
A40:
( (born xL1) (+) (born yR) c= ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) & (born xL2) (+) (born yR) c= ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) & (born xL2) (+) (born yL) c= ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) & (born xL1) (+) (born yL) c= ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) )
by A38, A35, ORDINAL1:def 2;
A41:
( xL1 == xL2 implies xL1yR == xL2yR )
by A40, A34, A15, A2;
L_ y << R_ y
by SURREAL0:45;
then A42:
yL < yR
by A31, A32;
( x <= x & y <= y )
;
then A43:
( L_ x << {x} & {x} << R_ x & x in {x} & L_ y << {y} & {y} << R_ y & y in {y} )
by SURREAL0:43, TARSKI:def 1;
then A44:
( xL1 < x & xL2 < x & yL < y )
by A31, A32;
A45:
((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) in (born x) (+) (born y)
by A39, ORDINAL3:12;
A46:
( (born x) (+) (born yL) c= ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) & (born x) (+) (born yR) c= ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) )
by XBOOLE_1:7;
set BB =
(((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR)));
A47:
(((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) in (born x) (+) (born y)
by A34, A45, ORDINAL3:12;
A48:
( ((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y)) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) )
by XBOOLE_1:7;
then A49:
( (born xL1) (+) (born yL) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born xL1) (+) (born yR) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born x) (+) (born yL) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born x) (+) (born yR) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) )
by A40, A46, XBOOLE_1:1;
A50:
( (born xL1) (+) (born y) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born xL2) (+) (born y) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) )
by A35, A48, XBOOLE_1:1;
A51:
( (born yL) (+) (born xL2) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born yR) (+) (born xL2) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) )
by A40, A48, XBOOLE_1:1;
xL1yR + xyL < xL1yL + xyR
by A47, A15, A2, A49, A42, A44;
then
xyL < (xL1yL + xyR) - xL1yR
by Th42;
then
xyL < xL1yL + (xyR - xL1yR)
by Th37;
then A52:
xyL - xL1yL < xyR - xL1yR
by Th41;
per cases
( xL1 < xL2 or xL2 < xL1 or xL1 == xL2 )
;
suppose A53:
xL1 < xL2
;
not r <= l
xL2yL + xL1y < xL1yL + xL2y
by A53, A44, A49, A50, A51, A47, A15, A2;
then
xL1y < (xL1yL + xL2y) - xL2yL
by Th42;
then
xL1y < xL1yL + (xL2y - xL2yL)
by Th37;
then
xL1y - xL1yL < xL2y - xL2yL
by Th41;
then A54:
(xL1y + (- xL1yL)) + xyL <= (xL2y - xL2yL) + xyL
by Th32;
A55:
(xL2y - xL2yL) + xyL = (xyL - xL2yL) + xL2y
by Th37;
xL2yR + xyL < xL2yL + xyR
by A42, A44, A47, A15, A2, A49, A51;
then
xyL < (xL2yL + xyR) - xL2yR
by Th42;
then
xyL < xL2yL + (xyR - xL2yR)
by Th37;
then
xyL - xL2yL < xyR - xL2yR
by Th41;
then
(xyL - xL2yL) + xL2y < (xyR - xL2yR) + xL2y
by Th32;
then
(xL1y - xL1yL) + xyL < (xyR - xL2yR) + xL2y
by SURREALO:4, A54, A55;
then
xL1y + ((- xL1yL) + xyL) < (xyR + (- xL2yR)) + xL2y
by Th37;
then
xL1y + (xyL - xL1yL) < xyR + (xL2y - xL2yR)
by Th37;
then
(xL1y + xyL) - xL1yL < xyR + (xL2y - xL2yR)
by Th37;
then
(xL1y + xyL) + (- xL1yL) < (xL2y + xyR) + (- xL2yR)
by Th37;
hence
l < r
by A31, A32;
verum
end;
suppose A56:
xL2 < xL1
;
not r <= l
A57:
( (born y) (+) (born xL1) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born yR) (+) (born xL1) c= (((born xL1) (+) (born y)) \/ ((born xL2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) )
by A48, A40, XBOOLE_1:1, A35;
( y < yR & xL2 < xL1 )
by A56, A43, A32;
then
xL1y + xL2yR < xL2y + xL1yR
by A50, A51, A57, A47, A15, A2;
then
xL1y < (xL2y + xL1yR) - xL2yR
by Th42;
then
xL1y < xL1yR + (xL2y - xL2yR)
by Th37;
then
xL1y - xL1yR < xL2y - xL2yR
by Th41;
then
(xL1y - xL1yR) + xyR < (xL2y + (- xL2yR)) + xyR
by Th32;
then
(xL1y - xL1yR) + xyR < (xL2y + xyR) + (- xL2yR)
by Th37;
then A58:
xL1y + (xyR + (- xL1yR)) < (xL2y + xyR) + (- xL2yR)
by Th37;
xL1yR + xyL < xL1yL + xyR
by A42, A44, A47, A15, A2, A49;
then
xyL < (xL1yL + xyR) - xL1yR
by Th42;
then
xyL < xL1yL + (xyR - xL1yR)
by Th37;
then
xyL - xL1yL < xyR - xL1yR
by Th41;
then
xL1y + (xyL - xL1yL) <= xL1y + (xyR - xL1yR)
by Th32;
then
xL1y + (xyL - xL1yL) < (xL2y + xyR) - xL2yR
by A58, SURREALO:4;
then
(xL1y + xyL) + (- xL1yL) < (xL2y + xyR) - xL2yR
by Th37;
hence
l < r
by A31, A32;
verum
end;
suppose A59:
xL1 == xL2
;
not r <= l
then
- xL1yR <= - xL2yR
by A41, Th10;
then A60:
(xL2y + xyR) - xL1yR <= (xL2y + xyR) - xL2yR
by Th32;
xL1y + (xyL - xL1yL) < xL2y + (xyR - xL1yR)
by A59, A36, A52, Th44;
then
xL1y + (xyL - xL1yL) < (xL2y + xyR) - xL1yR
by Th37;
then
xL1y + (xyL - xL1yL) < (xL2y + xyR) - xL2yR
by A60, SURREALO:4;
then
(xL1y + xyL) - xL1yL < (xL2y + xyR) - xL2yR
by Th37;
hence
l < r
by A31, A32;
verum
end;
end;
end;
suppose A61:
( l in comp ((R_ x),x,y,(R_ y)) & r in comp ((R_ x),x,y,(L_ y)) )
;
not r <= l
then consider xR1, yR being
Surreal such that A62:
( l = ((xR1 * y) +' (x * yR)) +' (-' (xR1 * yR)) & xR1 in R_ x & yR in R_ y )
by Def14;
consider xR2, yL being
Surreal such that A63:
( r = ((xR2 * y) +' (x * yL)) +' (-' (xR2 * yL)) & xR2 in R_ x & yL in L_ y )
by Def14, A61;
( xR1 in (L_ x) \/ (R_ x) & xR2 in (L_ x) \/ (R_ x) )
by A62, A63, XBOOLE_0:def 3;
then A64:
( (born xR1) (+) (born y) in (born x) (+) (born y) & (born xR2) (+) (born y) in (born x) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
then reconsider xR1y = xR1
* y, xR2y = xR2
* y as
Surreal by A15, A2;
set BR =
((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y));
A65:
((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) in (born x) (+) (born y)
by A64, ORDINAL3:12;
A66:
( (born xR1) (+) (born y) c= ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) & (born xR2) (+) (born y) c= ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) )
by XBOOLE_1:7;
A67:
( xR1 == xR2 implies xR1y == xR2y )
by A66, A65, A15, A2;
A68:
( yR in (L_ y) \/ (R_ y) & yL in (L_ y) \/ (R_ y) )
by A62, A63, XBOOLE_0:def 3;
then A69:
( (born xR1) (+) (born yL) in (born xR1) (+) (born y) & (born xR1) (+) (born yR) in (born xR1) (+) (born y) & (born xR2) (+) (born yL) in (born xR2) (+) (born y) & (born xR2) (+) (born yR) in (born xR2) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
( (born xR1) (+) (born yL) in (born x) (+) (born y) & (born xR1) (+) (born yR) in (born x) (+) (born y) & (born xR2) (+) (born yR) in (born x) (+) (born y) & (born xR2) (+) (born yL) in (born x) (+) (born y) )
by A69, A64, ORDINAL1:10;
then reconsider xR1yR = xR1
* yR, xR2yR = xR2
* yR, xR2yL = xR2
* yL, xR1yL = xR1
* yL as
Surreal by A15, A2;
set BY =
((born x) (+) (born yL)) \/ ((born x) (+) (born yR));
A70:
( (born x) (+) (born yL) in (born x) (+) (born y) & (born x) (+) (born yR) in (born x) (+) (born y) )
by A68, SURREALO:1, ORDINAL7:94;
then reconsider xyL = x
* yL, xyR = x
* yR as
Surreal by A15, A2;
A71:
( (born xR1) (+) (born yR) c= ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) & (born xR2) (+) (born yR) c= ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) & (born xR2) (+) (born yL) c= ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) & (born xR1) (+) (born yL) c= ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) )
by A69, A66, ORDINAL1:def 2;
A72:
( xR1 == xR2 implies xR1yR == xR2yR )
by A71, A65, A15, A2;
L_ y << R_ y
by SURREAL0:45;
then A73:
yL < yR
by A62, A63;
( x <= x & y <= y )
;
then A74:
( L_ x << {x} & {x} << R_ x & x in {x} & L_ y << {y} & {y} << R_ y & y in {y} )
by SURREAL0:43, TARSKI:def 1;
then A75:
( x < xR1 & x < xR2 & yL < y )
by A62, A63;
A76:
((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) in (born x) (+) (born y)
by A70, ORDINAL3:12;
A77:
( (born x) (+) (born yL) c= ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) & (born x) (+) (born yR) c= ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) )
by XBOOLE_1:7;
set BB =
(((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR)));
A78:
(((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) in (born x) (+) (born y)
by A65, A76, ORDINAL3:12;
A79:
( ((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y)) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & ((born x) (+) (born yL)) \/ ((born x) (+) (born yR)) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) )
by XBOOLE_1:7;
then A80:
( (born xR1) (+) (born yL) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born xR1) (+) (born yR) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born x) (+) (born yL) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born x) (+) (born yR) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) )
by A71, A77, XBOOLE_1:1;
A81:
( (born xR1) (+) (born y) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born xR2) (+) (born y) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) )
by A66, A79, XBOOLE_1:1;
A82:
( (born xR2) (+) (born yL) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) & (born xR2) (+) (born yR) c= (((born xR1) (+) (born y)) \/ ((born xR2) (+) (born y))) \/ (((born x) (+) (born yL)) \/ ((born x) (+) (born yR))) )
by A71, A79, XBOOLE_1:1;
per cases
( xR1 < xR2 or xR2 < xR1 or xR1 == xR2 )
;
suppose A83:
xR1 < xR2
;
not r <= l
( yL < y & xR1 < xR2 )
by A83, A74, A63;
then
xR2yL + xR1y < xR1yL + xR2y
by A80, A81, A82, A78, A15, A2;
then
xR1y < (xR1yL + xR2y) - xR2yL
by Th42;
then
xR1y < xR1yL + (xR2y - xR2yL)
by Th37;
then
xR1y - xR1yL < xR2y - xR2yL
by Th41;
then
(xR1y - xR1yL) + xyL < (xR2y - xR2yL) + xyL
by Th32;
then
((- xR1yL) + xR1y) + xyL < (- xR2yL) + (xR2y + xyL)
by Th37;
then A84:
(xR1y + xyL) - xR1yL < (xR2y + xyL) - xR2yL
by Th37;
xyR + xR1yL < xyL + xR1yR
by A73, A75, A80, A78, A15, A2;
then
(xyR + xR1yL) - xR1yR < xyL
by Th41;
then
xR1yL + (xyR - xR1yR) < xyL
by Th37;
then
xyR + (- xR1yR) < xyL - xR1yL
by Th42;
then
xR1y + (xyR + (- xR1yR)) < xR1y + (xyL + (- xR1yL))
by Th32;
then
(xR1y + xyR) + (- xR1yR) < xR1y + (xyL + (- xR1yL))
by Th37;
then
(xR1y + xyR) + (- xR1yR) <= (xR1y + xyL) + (- xR1yL)
by Th37;
hence
not r <= l
by A62, A63, A84, SURREALO:4;
verum
end;
suppose A85:
xR2 < xR1
;
not r <= l
( y < yR & xR2 < xR1 )
by A85, A74, A62;
then
xR1y + xR2yR < xR2y + xR1yR
by A80, A81, A82, A78, A15, A2;
then
(xR2yR + xR1y) - xR1yR < xR2y
by Th41;
then
xR2yR + (xR1y - xR1yR) < xR2y
by Th37;
then
xR1y + (- xR1yR) < xR2y - xR2yR
by Th42;
then
(xR1y + (- xR1yR)) + xyR < (xR2y + (- xR2yR)) + xyR
by Th32;
then A86:
(xR1y + xyR) + (- xR1yR) < (xR2y + (- xR2yR)) + xyR
by Th37;
xyR + xR2yL < xyL + xR2yR
by A73, A75, A78, A15, A2, A80, A82;
then
xyR < (xR2yR + xyL) - xR2yL
by Th42;
then
xyR < xR2yR + (xyL - xR2yL)
by Th37;
then
xyR - xR2yR < xyL - xR2yL
by Th41;
then
xR2y + ((- xR2yR) + xyR) < xR2y + (xyL + (- xR2yL))
by Th32;
then
(xR2y + (- xR2yR)) + xyR < xR2y + (xyL + (- xR2yL))
by Th37;
then
(xR2y + (- xR2yR)) + xyR <= (xR2y + xyL) + (- xR2yL)
by Th37;
hence
not r <= l
by A62, A63, A86, SURREALO:4;
verum
end;
suppose A87:
xR1 == xR2
;
not r <= l
then
- xR1yR <= - xR2yR
by A72, Th10;
then A88:
(xR1y + xyR) + (- xR1yR) <= (xR1y + xyR) + (- xR2yR)
by Th32;
xyR + xR2yL < xyL + xR2yR
by A75, A73, A80, A82, A78, A15, A2;
then
(xR2yL + xyR) - xR2yR < xyL
by Th41;
then
xR2yL + (xyR - xR2yR) < xyL
by Th37;
then
xyR - xR2yR < xyL - xR2yL
by Th42;
then
xR1y + (xyR - xR2yR) < xR2y + (xyL - xR2yL)
by A87, A67, Th44;
then
xR1y + (xyR - xR2yR) < (xR2y + xyL) - xR2yL
by Th37;
then
(xR1y + xyR) + (- xR2yR) < (xR2y + xyL) + (- xR2yL)
by Th37;
hence
l < r
by A88, SURREALO:4, A62, A63;
verum
end;
end;
end;
suppose A89:
( l in comp ((L_ x),x,y,(L_ y)) & r in comp ((R_ x),x,y,(L_ y)) )
;
not r <= l
then consider xL, yL1 being
Surreal such that A90:
( l = ((xL * y) +' (x * yL1)) +' (-' (xL * yL1)) & xL in L_ x & yL1 in L_ y )
by Def14;
consider xR, yL2 being
Surreal such that A91:
( r = ((xR * y) +' (x * yL2)) +' (-' (xR * yL2)) & xR in R_ x & yL2 in L_ y )
by Def14, A89;
( yL1 in (L_ y) \/ (R_ y) & yL2 in (L_ y) \/ (R_ y) )
by A90, A91, XBOOLE_0:def 3;
then A92:
( (born yL1) (+) (born x) in (born x) (+) (born y) & (born yL2) (+) (born x) in (born x) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
then reconsider yL1x = yL1
* x, yL2x = yL2
* x as
Surreal by A15, A2;
set BL =
((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x));
A93:
((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) in (born x) (+) (born y)
by A92, ORDINAL3:12;
A94:
( (born yL1) (+) (born x) c= ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) & (born yL2) (+) (born x) c= ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) )
by XBOOLE_1:7;
A95:
( yL1 == yL2 implies yL1x == yL2x )
by A94, A93, A15, A2;
A96:
( xR in (L_ x) \/ (R_ x) & xL in (L_ x) \/ (R_ x) )
by A90, A91, XBOOLE_0:def 3;
A97:
( (born yL1) (+) (born xL) in (born yL1) (+) (born x) & (born yL1) (+) (born xR) in (born yL1) (+) (born x) & (born yL2) (+) (born xL) in (born yL2) (+) (born x) & (born yL2) (+) (born xR) in (born yL2) (+) (born x) )
by A96, SURREALO:1, ORDINAL7:94;
then
( (born yL1) (+) (born xL) in (born x) (+) (born y) & (born yL1) (+) (born xR) in (born x) (+) (born y) & (born yL2) (+) (born xR) in (born x) (+) (born y) & (born yL2) (+) (born xL) in (born x) (+) (born y) )
by A92, ORDINAL1:10;
then reconsider yL1xR = yL1
* xR, yL2xR = yL2
* xR, yL2xL = yL2
* xL, yL1xL = yL1
* xL as
Surreal by A15, A2;
set BY =
((born y) (+) (born xL)) \/ ((born y) (+) (born xR));
A98:
( (born y) (+) (born xL) in (born x) (+) (born y) & (born y) (+) (born xR) in (born x) (+) (born y) )
by A96, SURREALO:1, ORDINAL7:94;
then reconsider yxL = y
* xL, yxR = y
* xR as
Surreal by A15, A2;
A99:
( (born yL1) (+) (born xR) c= ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) & (born yL2) (+) (born xR) c= ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) & (born yL2) (+) (born xL) c= ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) & (born yL1) (+) (born xL) c= ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) )
by A97, A94, ORDINAL1:def 2;
A100:
( yL1 == yL2 implies yL1xR == yL2xR )
by A99, A93, A15, A2;
L_ x << R_ x
by SURREAL0:45;
then A101:
xL < xR
by A90, A91;
( x <= x & y <= y )
;
then A102:
( L_ x << {x} & {x} << R_ x & x in {x} & L_ y << {y} & {y} << R_ y & y in {y} )
by SURREAL0:43, TARSKI:def 1;
then A103:
( yL1 < y & yL2 < y & xL < x )
by A90, A91;
A104:
((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) in (born x) (+) (born y)
by A98, ORDINAL3:12;
A105:
( (born y) (+) (born xL) c= ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) & (born y) (+) (born xR) c= ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) )
by XBOOLE_1:7;
set BB =
(((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR)));
A106:
(((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) in (born x) (+) (born y)
by A93, A104, ORDINAL3:12;
A107:
( ((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x)) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) )
by XBOOLE_1:7;
then A108:
( (born yL1) (+) (born xL) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born yL1) (+) (born xR) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born y) (+) (born xL) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born y) (+) (born xR) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) )
by A99, A105, XBOOLE_1:1;
A109:
( (born yL1) (+) (born x) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born yL2) (+) (born x) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) )
by A94, A107, XBOOLE_1:1;
A110:
( (born xL) (+) (born yL2) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born xR) (+) (born yL2) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) )
by A99, A107, XBOOLE_1:1;
yL1xR + yxL < yL1xL + yxR
by A106, A15, A2, A108, A101, A103;
then
yxL < (yL1xL + yxR) - yL1xR
by Th42;
then
yxL < yL1xL + (yxR - yL1xR)
by Th37;
then A111:
yxL - yL1xL < yxR - yL1xR
by Th41;
A112:
( xL * yL2 = yL2xL & x * yL2 = yL2x )
by A2, A106, A15, A109, A110;
A113:
( xL * yL1 = yL1xL & x * yL1 = yL1x )
by A2, A106, A15, A108, A109;
A114:
( xR * yL2 = yL2xR & xR * yL1 = yL1xR )
by A2, A106, A15, A108, A110;
A115: l =
(yxL + yL1x) + (- yL1xL)
by A90, A2, A106, A15, A108, A113
.=
(yL1x + yxL) + (- yL1xL)
;
A116: r =
(yxR + yL2x) + (- yL2xR)
by A91, A2, A106, A15, A108, A112, A114
.=
(yL2x + yxR) + (- yL2xR)
;
per cases
( yL1 < yL2 or yL2 < yL1 or yL1 == yL2 )
;
suppose A117:
yL1 < yL2
;
not r <= l
yL2xL + yL1x < yL1xL + yL2x
by A117, A103, A108, A109, A110, A106, A15, A2;
then
yL1x < (yL1xL + yL2x) - yL2xL
by Th42;
then
yL1x < yL1xL + (yL2x - yL2xL)
by Th37;
then
yL1x - yL1xL < yL2x - yL2xL
by Th41;
then A118:
(yL1x + (- yL1xL)) + yxL <= (yL2x - yL2xL) + yxL
by Th32;
A119:
(yL2x - yL2xL) + yxL = (yxL - yL2xL) + yL2x
by Th37;
yL2xR + yxL < yL2xL + yxR
by A101, A103, A106, A15, A2, A108, A110;
then
yxL < (yL2xL + yxR) - yL2xR
by Th42;
then
yxL < yL2xL + (yxR + (- yL2xR))
by Th37;
then
yxL - yL2xL < yxR + (- yL2xR)
by Th41;
then
(yxL - yL2xL) + yL2x < (yxR + (- yL2xR)) + yL2x
by Th32;
then
(yL1x - yL1xL) + yxL < (yxR + (- yL2xR)) + yL2x
by SURREALO:4, A118, A119;
then
yL1x + ((- yL1xL) + yxL) < (yxR - yL2xR) + yL2x
by Th37;
then
yL1x + (yxL - yL1xL) < yxR + (yL2x - yL2xR)
by Th37;
then
(yL1x + yxL) - yL1xL < yxR + (yL2x - yL2xR)
by Th37;
hence
l < r
by A115, A116, Th37;
verum
end;
suppose A120:
yL2 < yL1
;
not r <= l
A121:
( (born x) (+) (born yL1) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born xR) (+) (born yL1) c= (((born yL1) (+) (born x)) \/ ((born yL2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) )
by A99, XBOOLE_1:1, A94, A107;
( x < xR & yL2 < yL1 )
by A120, A102, A91;
then
yL1x + yL2xR < yL2x + yL1xR
by A109, A110, A121, A106, A15, A2;
then
yL1x < (yL2x + yL1xR) - yL2xR
by Th42;
then
yL1x < yL1xR + (yL2x - yL2xR)
by Th37;
then
yL1x - yL1xR < yL2x - yL2xR
by Th41;
then
(yL1x - yL1xR) + yxR < (yL2x - yL2xR) + yxR
by Th32;
then
(yL1x - yL1xR) + yxR < (yL2x + yxR) - yL2xR
by Th37;
then A122:
yL1x + (yxR + (- yL1xR)) < (yL2x + yxR) + (- yL2xR)
by Th37;
yL1xR + yxL < yL1xL + yxR
by A101, A103, A106, A15, A2, A108;
then
yxL < (yL1xL + yxR) - yL1xR
by Th42;
then
yxL < yL1xL + (yxR - yL1xR)
by Th37;
then
yxL - yL1xL < yxR - yL1xR
by Th41;
then
yL1x + (yxL + (- yL1xL)) <= yL1x + (yxR - yL1xR)
by Th32;
then
yL1x + (yxL + (- yL1xL)) < (yL2x + yxR) + (- yL2xR)
by A122, SURREALO:4;
hence
l < r
by A115, A116, Th37;
verum
end;
suppose A123:
yL1 == yL2
;
not r <= l
then
- yL1xR <= - yL2xR
by Th10, A100;
then A124:
(yL2x + yxR) + (- yL1xR) <= (yL2x + yxR) + (- yL2xR)
by Th32;
yL1x + (yxL + (- yL1xL)) < yL2x + (yxR + (- yL1xR))
by A123, A95, A111, Th44;
then
yL1x + (yxL + (- yL1xL)) < (yL2x + yxR) + (- yL1xR)
by Th37;
then
yL1x + (yxL + (- yL1xL)) < (yL2x + yxR) + (- yL2xR)
by A124, SURREALO:4;
hence
l < r
by Th37, A115, A116;
verum
end;
end;
end;
suppose A125:
( l in comp ((R_ x),x,y,(R_ y)) & r in comp ((L_ x),x,y,(R_ y)) )
;
not r <= l
then consider xR, yR1 being
Surreal such that A126:
( l = ((xR * y) +' (x * yR1)) +' (-' (xR * yR1)) & xR in R_ x & yR1 in R_ y )
by Def14;
consider xL, yR2 being
Surreal such that A127:
( r = ((xL * y) +' (x * yR2)) +' (-' (xL * yR2)) & xL in L_ x & yR2 in R_ y )
by Def14, A125;
( yR1 in (L_ y) \/ (R_ y) & yR2 in (L_ y) \/ (R_ y) )
by A126, A127, XBOOLE_0:def 3;
then A128:
( (born yR1) (+) (born x) in (born y) (+) (born x) & (born yR2) (+) (born x) in (born y) (+) (born x) )
by SURREALO:1, ORDINAL7:94;
then reconsider yR1x = yR1
* x, yR2x = yR2
* x as
Surreal by A15, A2;
set BR =
((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x));
A129:
((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) in (born x) (+) (born y)
by A128, ORDINAL3:12;
A130:
( (born yR1) (+) (born x) c= ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) & (born yR2) (+) (born x) c= ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) )
by XBOOLE_1:7;
A131:
( yR1 == yR2 implies yR1x == yR2x )
by A130, A129, A15, A2;
A132:
( xR in (L_ x) \/ (R_ x) & xL in (L_ x) \/ (R_ x) )
by A126, A127, XBOOLE_0:def 3;
A133:
( (born yR1) (+) (born xL) in (born yR1) (+) (born x) & (born yR1) (+) (born xR) in (born yR1) (+) (born x) & (born yR2) (+) (born xL) in (born yR2) (+) (born x) & (born yR2) (+) (born xR) in (born yR2) (+) (born x) )
by A132, SURREALO:1, ORDINAL7:94;
( (born yR1) (+) (born xL) in (born x) (+) (born y) & (born yR1) (+) (born xR) in (born x) (+) (born y) & (born yR2) (+) (born xR) in (born x) (+) (born y) & (born yR2) (+) (born xL) in (born x) (+) (born y) )
by A128, ORDINAL1:10, A133;
then reconsider yR1xR = yR1
* xR, yR2xR = yR2
* xR, yR2xL = yR2
* xL, yR1xL = yR1
* xL as
Surreal by A15, A2;
set BY =
((born y) (+) (born xL)) \/ ((born y) (+) (born xR));
A134:
( (born y) (+) (born xL) in (born x) (+) (born y) & (born y) (+) (born xR) in (born x) (+) (born y) )
by A132, SURREALO:1, ORDINAL7:94;
then reconsider yxL = y
* xL, yxR = y
* xR as
Surreal by A15, A2;
A135:
( (born yR1) (+) (born xR) c= ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) & (born yR2) (+) (born xR) c= ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) & (born yR2) (+) (born xL) c= ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) & (born yR1) (+) (born xL) c= ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) )
by A133, A130, ORDINAL1:def 2;
A136:
( yR1 == yR2 implies yR1xR == yR2xR )
by A135, A129, A15, A2;
L_ x << R_ x
by SURREAL0:45;
then A137:
xL < xR
by A126, A127;
( x <= x & y <= y )
;
then A138:
( L_ x << {x} & {x} << R_ x & x in {x} & L_ y << {y} & {y} << R_ y & y in {y} )
by SURREAL0:43, TARSKI:def 1;
then A139:
( y < yR1 & y < yR2 & xL < x )
by A126, A127;
A140:
((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) in (born x) (+) (born y)
by A134, ORDINAL3:12;
A141:
( (born y) (+) (born xL) c= ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) & (born y) (+) (born xR) c= ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) )
by XBOOLE_1:7;
set BB =
(((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR)));
A142:
(((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) in (born x) (+) (born y)
by A129, A140, ORDINAL3:12;
A143:
( ((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x)) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & ((born y) (+) (born xL)) \/ ((born y) (+) (born xR)) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) )
by XBOOLE_1:7;
then A144:
( (born yR1) (+) (born xL) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born yR1) (+) (born xR) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born y) (+) (born xL) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born y) (+) (born xR) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) )
by A135, A141, XBOOLE_1:1;
A145:
( (born yR1) (+) (born x) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born yR2) (+) (born x) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) )
by A130, A143, XBOOLE_1:1;
A146:
( (born yR2) (+) (born xL) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) & (born yR2) (+) (born xR) c= (((born yR1) (+) (born x)) \/ ((born yR2) (+) (born x))) \/ (((born y) (+) (born xL)) \/ ((born y) (+) (born xR))) )
by A135, A143, XBOOLE_1:1;
A147:
( xR * y = yxR & xL * y = yxL )
by A2, A142, A15, A144;
A148:
( xL * yR2 = yR2xL & x * yR2 = yR2x )
by A2, A142, A15, A145, A146;
A149:
( xR * yR2 = yR2xR & xR * yR1 = yR1xR )
by A2, A142, A15, A144, A146;
A150: l =
(yxR + yR1x) + (- yR1xR)
by A126, A147, A2, A142, A15, A145, A149
.=
(yR1x + yxR) + (- yR1xR)
;
A151: r =
(yxL + yR2x) + (- yR2xL)
by A127, A2, A142, A15, A144, A148
.=
(yR2x + yxL) + (- yR2xL)
;
per cases
( yR1 < yR2 or yR2 < yR1 or yR1 == yR2 )
;
suppose A152:
yR1 < yR2
;
not r <= l
yR2xL + yR1x < yR1xL + yR2x
by A152, A139, A144, A145, A146, A142, A15, A2;
then
yR1x < (yR1xL + yR2x) - yR2xL
by Th42;
then
yR1x < yR1xL + (yR2x - yR2xL)
by Th37;
then
yR1x - yR1xL < yR2x - yR2xL
by Th41;
then
(yR1x - yR1xL) + yxL < (yR2x - yR2xL) + yxL
by Th32;
then
((- yR1xL) + yR1x) + yxL < (- yR2xL) + (yR2x + yxL)
by Th37;
then A153:
(yR1x + yxL) + (- yR1xL) < (yR2x + yxL) - yR2xL
by Th37;
yxR + yR1xL < yxL + yR1xR
by A137, A139, A144, A142, A15, A2;
then
(yxR + yR1xL) - yR1xR < yxL
by Th41;
then
yR1xL + (yxR - yR1xR) < yxL
by Th37;
then
yxR + (- yR1xR) < yxL - yR1xL
by Th42;
then
yR1x + (yxR - yR1xR) < yR1x + (yxL - yR1xL)
by Th32;
then
(yR1x + yxR) - yR1xR < yR1x + (yxL - yR1xL)
by Th37;
then
(yR1x + yxR) - yR1xR <= (yR1x + yxL) - yR1xL
by Th37;
hence
not r <= l
by A151, A150, A153, SURREALO:4;
verum
end;
suppose A154:
yR2 < yR1
;
not r <= l
( x < xR & yR2 < yR1 )
by A154, A138, A126;
then
yR1x + yR2xR < yR2x + yR1xR
by A144, A145, A146, A142, A15, A2;
then
(yR1x + yR2xR) - yR1xR < yR2x
by Th41;
then
yR2xR + (yR1x - yR1xR) < yR2x
by Th37;
then
yR1x - yR1xR < yR2x - yR2xR
by Th42;
then
(yR1x - yR1xR) + yxR < (yR2x - yR2xR) + yxR
by Th32;
then A155:
(yR1x + yxR) + (- yR1xR) < (yR2x - yR2xR) + yxR
by Th37;
yxR + yR2xL < yxL + yR2xR
by A137, A139, A142, A15, A2, A144, A146;
then
yxR < (yR2xR + yxL) - yR2xL
by Th42;
then
yxR < yR2xR + (yxL - yR2xL)
by Th37;
then
yxR - yR2xR < yxL - yR2xL
by Th41;
then
yR2x + ((- yR2xR) + yxR) < yR2x + (yxL - yR2xL)
by Th32;
then
(yR2x + (- yR2xR)) + yxR < yR2x + (yxL - yR2xL)
by Th37;
then
(yR2x - yR2xR) + yxR <= (yR2x + yxL) - yR2xL
by Th37;
hence
not r <= l
by A151, A150, A155, SURREALO:4;
verum
end;
suppose A156:
yR1 == yR2
;
not r <= l
then
- yR1xR <= - yR2xR
by A136, Th10;
then A157:
(yR1x + yxR) - yR1xR <= (yR1x + yxR) - yR2xR
by Th32;
yxR + yR2xL < yxL + yR2xR
by A139, A137, A144, A146, A142, A15, A2;
then
(yR2xL + yxR) - yR2xR < yxL
by Th41;
then
yR2xL + (yxR - yR2xR) < yxL
by Th37;
then
yxR - yR2xR < yxL - yR2xL
by Th42;
then
yR1x + (yxR - yR2xR) < yR2x + (yxL - yR2xL)
by A156, A131, Th44;
then
yR1x + (yxR - yR2xR) < (yR2x + yxL) - yR2xL
by Th37;
then
(yR1x + yxR) - yR2xR < (yR2x + yxL) - yR2xL
by Th37;
hence
l < r
by A151, A150, A157, SURREALO:4;
verum
end;
end;
end;
end;
end;
then
[((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))),((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))))] in Day (succ U)
by A25, SURREAL0:46;
hence
x * y is Surreal
by Th50;
verum
end;
defpred S
11[
Ordinal]
means for x1, x2, y being
Surreal st
((born x1) (+) (born x2)) (+) (born y) c= $1 holds
( S
3[D,x1,x2,y] & S
5[D,x1,x2,y] );
A158:
for E being Ordinal st ( for C being Ordinal st C in E holds
S11[C] ) holds
S11[E]
proof
let E be
Ordinal;
( ( for C being Ordinal st C in E holds
S11[C] ) implies S11[E] )
assume A159:
for C being Ordinal st C in E holds
S11[C]
;
S11[E]
A160:
for x1, x2, y, x1y, x2y being Surreal st ((born x1) (+) (born x2)) (+) (born y) c= E & (born x1) (+) (born y) c= D & (born x2) (+) (born y) c= D & x1 == x2 & x1y = x1 * y & x2y = x2 * y holds
( L_ x1y << {x2y} & {x2y} << R_ x1y )
proof
let x1, x2, y, x1y, x2y be
Surreal;
( ((born x1) (+) (born x2)) (+) (born y) c= E & (born x1) (+) (born y) c= D & (born x2) (+) (born y) c= D & x1 == x2 & x1y = x1 * y & x2y = x2 * y implies ( L_ x1y << {x2y} & {x2y} << R_ x1y ) )
assume that A161:
((born x1) (+) (born x2)) (+) (born y) c= E
and A162:
( (born x1) (+) (born y) c= D & (born x2) (+) (born y) c= D )
and A163:
( x1 == x2 & x1y = x1 * y & x2y = x2 * y )
;
( L_ x1y << {x2y} & {x2y} << R_ x1y )
A164:
x1y = [((comp ((L_ x1),x1,y,(L_ y))) \/ (comp ((R_ x1),x1,y,(R_ y)))),((comp ((L_ x1),x1,y,(R_ y))) \/ (comp ((R_ x1),x1,y,(L_ y))))]
by A163, Th50;
A165:
( L_ y << {y} & {y} << R_ y & y in {y} )
by SURREALO:11, TARSKI:def 1;
thus
L_ x1y << {x2y}
{x2y} << R_ x1y
proof
let l be
Surreal;
SURREAL0:def 20 for b1 being set holds
( not l in L_ x1y or not b1 in {x2y} or not b1 <= l )let r be
Surreal;
( not l in L_ x1y or not r in {x2y} or not r <= l )
assume A166:
( l in L_ x1y & r in {x2y} )
;
not r <= l
per cases
( l in comp ((R_ x1),x1,y,(R_ y)) or l in comp ((L_ x1),x1,y,(L_ y)) )
by A164, A166, XBOOLE_0:def 3;
suppose
l in comp ((R_ x1),x1,y,(R_ y))
;
not r <= l
then consider x3, y3 being
Surreal such that A167:
( l = ((x3 * y) +' (x1 * y3)) +' (-' (x3 * y3)) & x3 in R_ x1 & y3 in R_ y )
by Def14;
A168:
( {x1} << R_ x1 & x1 in {x1} )
by SURREALO:11, TARSKI:def 1;
A169:
y3 in (L_ y) \/ (R_ y)
by A167, XBOOLE_0:def 3;
then A170:
( (born x1) (+) (born y3) in (born x1) (+) (born y) & (born x2) (+) (born y3) in (born x2) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
then reconsider x1y3 = x1
* y3, x2y3 = x2
* y3 as
Surreal by A2, A162;
set BL =
((born x1) (+) (born y3)) \/ ((born x2) (+) (born y3));
x3 in (L_ x1) \/ (R_ x1)
by A167, XBOOLE_0:def 3;
then A171:
( (born x3) (+) (born y3) in (born x1) (+) (born y3) & (born x3) (+) (born y) in (born x1) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
then A172:
( (born x3) (+) (born y3) in D & (born x3) (+) (born y) in D )
by A170, A162, ORDINAL1:10;
then reconsider x3y3 = x3
* y3, x3y = x3
* y as
Surreal by A2;
A173:
((born x1) (+) (born x2)) (+) (born y3) in ((born x1) (+) (born x2)) (+) (born y)
by A169, SURREALO:1, ORDINAL7:94;
( (born x1) (+) (born y3) c= D & (born x2) (+) (born y3) c= D )
by A170, A162, ORDINAL1:def 2;
then A174:
x1y3 == x2y3
by A173, A163, A161, A159;
((born y) (+) (born x3)) (+) (born x2) in ((born y) (+) (born x1)) (+) (born x2)
by A171, ORDINAL7:94;
then A175:
((born y) (+) (born x3)) (+) (born x2) in (born y) (+) ((born x1) (+) (born x2))
by ORDINAL7:68;
A176:
((born y) (+) (born x3)) (+) (born x2) = ((born y) (+) (born x2)) (+) (born x3)
by ORDINAL7:68;
A177:
(born x2) (+) (born y3) c= D
by A170, A162, ORDINAL1:def 2;
A178:
y3 * x2 = x2y3
by A3, A170, A162, ORDINAL1:def 2;
A179:
( (born x3) (+) (born y) c= D & (born x2) (+) (born y) c= D )
by A171, A162, ORDINAL1:def 2;
A180:
( y * x3 = x3y & y * x2 = x2y )
by A162, A163, A3, A171, A2;
A181:
(born x3) (+) (born y3) c= D
by A171, A170, A162, ORDINAL1:10, ORDINAL1:def 2;
A182:
y3 * x3 = x3y3
by A172, A2;
( y < y3 & x2 < x3 )
by A168, A167, A163, SURREALO:4, A165;
then
x2y3 + x3y < x3y3 + x2y
by A167, A176, A175, A161, A159, A177, A178, A179, A180, A181, A182;
then A183:
(x2y3 + x3y) - x3y3 < x2y
by Th41;
x1y3 + (x3y + (- x3y3)) <= x2y3 + (x3y - x3y3)
by A174, Th32;
then
(x1y3 + x3y) - x3y3 <= x2y3 + (x3y - x3y3)
by Th37;
then
(x1y3 + x3y) - x3y3 <= (x2y3 + x3y) - x3y3
by Th37;
then A184:
(x1y3 + x3y) - x3y3 < x2y
by A183, SURREALO:4;
l = (x3y + x1y3) - x3y3
by A167;
hence
not r <= l
by A166, A184, TARSKI:def 1;
verum
end;
suppose
l in comp ((L_ x1),x1,y,(L_ y))
;
not r <= l
then consider x3, y3 being
Surreal such that A185:
( l = ((x3 * y) +' (x1 * y3)) +' (-' (x3 * y3)) & x3 in L_ x1 & y3 in L_ y )
by Def14;
A186:
( L_ x1 << {x1} & x1 in {x1} )
by SURREALO:11, TARSKI:def 1;
A187:
y3 in (L_ y) \/ (R_ y)
by A185, XBOOLE_0:def 3;
then A188:
( (born x1) (+) (born y3) in (born x1) (+) (born y) & (born x2) (+) (born y3) in (born x2) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
then reconsider x1y3 = x1
* y3, x2y3 = x2
* y3 as
Surreal by A2, A162;
set BL =
((born x1) (+) (born y3)) \/ ((born x2) (+) (born y3));
x3 in (L_ x1) \/ (R_ x1)
by A185, XBOOLE_0:def 3;
then A189:
( (born x3) (+) (born y3) in (born x1) (+) (born y3) & (born x3) (+) (born y) in (born x1) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
then A190:
( (born x3) (+) (born y3) in D & (born x3) (+) (born y) in D )
by A188, A162, ORDINAL1:10;
then reconsider x3y3 = x3
* y3, x3y = x3
* y as
Surreal by A2;
A191:
((born x1) (+) (born x2)) (+) (born y3) in ((born x1) (+) (born x2)) (+) (born y)
by A187, SURREALO:1, ORDINAL7:94;
( (born x1) (+) (born y3) c= D & (born x2) (+) (born y3) c= D )
by A188, A162, ORDINAL1:def 2;
then A192:
x1y3 == x2y3
by A191, A161, A159, A163;
((born y) (+) (born x3)) (+) (born x2) in ((born y) (+) (born x1)) (+) (born x2)
by A189, ORDINAL7:94;
then A193:
((born y) (+) (born x3)) (+) (born x2) in (born y) (+) ((born x1) (+) (born x2))
by ORDINAL7:68;
A194:
(born x2) (+) (born y3) c= D
by A188, A162, ORDINAL1:def 2;
A195:
y3 * x2 = x2y3
by A3, A188, A162, ORDINAL1:def 2;
A196:
( (born x3) (+) (born y) c= D & (born x2) (+) (born y) c= D )
by A189, A162, ORDINAL1:def 2;
A197:
( y * x3 = x3y & y * x2 = x2y )
by A163, A3, A162, A189, ORDINAL1:def 2;
A198:
(born x3) (+) (born y3) c= D
by A188, A162, ORDINAL1:10, A189, ORDINAL1:def 2;
A199:
y3 * x3 = x3y3
by A190, A2;
A200:
( y3 < y & x3 < x2 )
by A186, A185, A163, SURREALO:4, A165;
x2y3 + x3y < x3y3 + x2y
by A185, A200, A194, A195, A196, A197, A198, A199, A193, A161, A159;
then A201:
(x2y3 + x3y) - x3y3 < x2y
by Th41;
x1y3 + (x3y + (- x3y3)) <= x2y3 + (x3y + (- x3y3))
by A192, Th32;
then
(x1y3 + x3y) + (- x3y3) <= x2y3 + (x3y + (- x3y3))
by Th37;
then
(x1y3 + x3y) + (- x3y3) <= (x2y3 + x3y) + (- x3y3)
by Th37;
then A202:
(x1y3 + x3y) + (- x3y3) < x2y
by A201, SURREALO:4;
l = (x3y + x1y3) + (- x3y3)
by A185;
hence
not r <= l
by A166, A202, TARSKI:def 1;
verum
end;
end;
end;
thus
{x2y} << R_ x1y
verum
proof
let l be
Surreal;
SURREAL0:def 20 for b1 being set holds
( not l in {x2y} or not b1 in R_ x1y or not b1 <= l )let r be
Surreal;
( not l in {x2y} or not r in R_ x1y or not r <= l )
assume A203:
( l in {x2y} & r in R_ x1y )
;
not r <= l
per cases
( r in comp ((L_ x1),x1,y,(R_ y)) or r in comp ((R_ x1),x1,y,(L_ y)) )
by XBOOLE_0:def 3, A164, A203;
suppose
r in comp ((L_ x1),x1,y,(R_ y))
;
not r <= l
then consider x3, y3 being
Surreal such that A204:
( r = ((x3 * y) +' (x1 * y3)) +' (-' (x3 * y3)) & x3 in L_ x1 & y3 in R_ y )
by Def14;
A205:
( L_ x1 << {x1} & x1 in {x1} )
by SURREALO:11, TARSKI:def 1;
A206:
y3 in (L_ y) \/ (R_ y)
by A204, XBOOLE_0:def 3;
then A207:
( (born x1) (+) (born y3) in (born x1) (+) (born y) & (born x2) (+) (born y3) in (born x2) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
then reconsider x1y3 = x1
* y3, x2y3 = x2
* y3 as
Surreal by A162, A2;
set BL =
((born x1) (+) (born y3)) \/ ((born x2) (+) (born y3));
x3 in (L_ x1) \/ (R_ x1)
by A204, XBOOLE_0:def 3;
then A208:
( (born x3) (+) (born y3) in (born x1) (+) (born y3) & (born x3) (+) (born y) in (born x1) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
then A209:
( (born x3) (+) (born y3) in D & (born x3) (+) (born y) in D )
by A207, A162, ORDINAL1:10;
then reconsider x3y3 = x3
* y3, x3y = x3
* y as
Surreal by A2;
A210:
((born x1) (+) (born x2)) (+) (born y3) in ((born x1) (+) (born x2)) (+) (born y)
by A206, SURREALO:1, ORDINAL7:94;
( (born x1) (+) (born y3) c= D & (born x2) (+) (born y3) c= D )
by A207, A162, ORDINAL1:def 2;
then A211:
x1y3 == x2y3
by A210, A161, A159, A163;
((born y) (+) (born x3)) (+) (born x2) in ((born y) (+) (born x1)) (+) (born x2)
by A208, ORDINAL7:94;
then A212:
((born y) (+) (born x3)) (+) (born x2) in (born y) (+) ((born x1) (+) (born x2))
by ORDINAL7:68;
A213:
(born x2) (+) (born y3) c= D
by A207, A162, ORDINAL1:def 2;
A214:
y3 * x2 = x2y3
by A3, A207, A162, ORDINAL1:def 2;
A215:
( (born x3) (+) (born y) c= D & (born x2) (+) (born y) c= D )
by A208, A162, ORDINAL1:def 2;
A216:
( y * x3 = x3y & y * x2 = x2y )
by A208, A162, ORDINAL1:def 2, A163, A3;
A217:
(born x3) (+) (born y3) c= D
by A207, A162, ORDINAL1:10, A208, ORDINAL1:def 2;
A218:
y3 * x3 = x3y3
by A209, A2;
A219:
( y < y3 & x3 < x2 )
by A205, A204, A163, SURREALO:4, A165;
x3y3 + x2y < x2y3 + x3y
by A204, A212, A161, A159, A219, A213, A214, A215, A216, A217, A218;
then A220:
x2y < (x2y3 + x3y) - x3y3
by Th42;
x2y3 + (x3y + (- x3y3)) <= x1y3 + (x3y + (- x3y3))
by A211, Th32;
then
(x2y3 + x3y) + (- x3y3) <= x1y3 + (x3y + (- x3y3))
by Th37;
then
(x2y3 + x3y) + (- x3y3) <= (x1y3 + x3y) + (- x3y3)
by Th37;
then A221:
x2y < (x1y3 + x3y) + (- x3y3)
by A220, SURREALO:4;
r = (x3y + x1y3) + (- x3y3)
by A204;
hence
not r <= l
by A203, A221, TARSKI:def 1;
verum
end;
suppose
r in comp ((R_ x1),x1,y,(L_ y))
;
not r <= l
then consider x3, y3 being
Surreal such that A222:
( r = ((x3 * y) +' (x1 * y3)) +' (-' (x3 * y3)) & x3 in R_ x1 & y3 in L_ y )
by Def14;
A223:
( {x1} << R_ x1 & x1 in {x1} )
by SURREALO:11, TARSKI:def 1;
A224:
y3 in (L_ y) \/ (R_ y)
by A222, XBOOLE_0:def 3;
then A225:
( (born x1) (+) (born y3) in (born x1) (+) (born y) & (born x2) (+) (born y3) in (born x2) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
then reconsider x1y3 = x1
* y3, x2y3 = x2
* y3 as
Surreal by A2, A162;
set BL =
((born x1) (+) (born y3)) \/ ((born x2) (+) (born y3));
x3 in (L_ x1) \/ (R_ x1)
by A222, XBOOLE_0:def 3;
then A226:
( (born x3) (+) (born y3) in (born x1) (+) (born y3) & (born x3) (+) (born y) in (born x1) (+) (born y) )
by SURREALO:1, ORDINAL7:94;
then A227:
( (born x3) (+) (born y3) in D & (born x3) (+) (born y) in D )
by A225, A162, ORDINAL1:10;
then reconsider x3y3 = x3
* y3, x3y = x3
* y as
Surreal by A2;
A228:
((born x1) (+) (born x2)) (+) (born y3) in ((born x1) (+) (born x2)) (+) (born y)
by A224, SURREALO:1, ORDINAL7:94;
( (born x1) (+) (born y3) c= D & (born x2) (+) (born y3) c= D )
by A225, A162, ORDINAL1:def 2;
then A229:
x1y3 == x2y3
by A228, A159, A161, A163;
((born y) (+) (born x3)) (+) (born x2) in ((born y) (+) (born x1)) (+) (born x2)
by A226, ORDINAL7:94;
then A230:
((born y) (+) (born x3)) (+) (born x2) in (born y) (+) ((born x1) (+) (born x2))
by ORDINAL7:68;
A231:
((born y) (+) (born x3)) (+) (born x2) = ((born y) (+) (born x2)) (+) (born x3)
by ORDINAL7:68;
A232:
(born x2) (+) (born y3) c= D
by A225, A162, ORDINAL1:def 2;
A233:
y3 * x2 = x2y3
by A3, A225, A162, ORDINAL1:def 2;
A234:
( (born x3) (+) (born y) c= D & (born x2) (+) (born y) c= D )
by A226, A162, ORDINAL1:def 2;
A235:
( y * x3 = x3y & y * x2 = x2y )
by A163, A3, A226, A162, ORDINAL1:def 2;
A236:
(born x3) (+) (born y3) c= D
by A226, A225, A162, ORDINAL1:10, ORDINAL1:def 2;
A237:
y3 * x3 = x3y3
by A3, A227, ORDINAL1:def 2;
A238:
( y3 < y & x2 < x3 )
by A223, A222, A163, SURREALO:4, A165;
x3y3 + x2y < x2y3 + x3y
by A231, A222, A230, A159, A161, A238, A232, A233, A234, A235, A236, A237;
then A239:
x2y < (x2y3 + x3y) - x3y3
by Th42;
x2y3 + (x3y + (- x3y3)) <= x1y3 + (x3y - x3y3)
by A229, Th32;
then
(x2y3 + x3y) - x3y3 <= x1y3 + (x3y - x3y3)
by Th37;
then
(x2y3 + x3y) - x3y3 <= (x1y3 + x3y) - x3y3
by Th37;
then A240:
x2y < (x1y3 + x3y) - x3y3
by A239, SURREALO:4;
r = (x3y + x1y3) - x3y3
by A222;
hence
not r <= l
by A203, A240, TARSKI:def 1;
verum
end;
end;
end;
end;
let x, y1, y2 be
Surreal;
( ((born x) (+) (born y1)) (+) (born y2) c= E implies ( S3[D,x,y1,y2] & S5[D,x,y1,y2] ) )
assume A241:
((born x) (+) (born y1)) (+) (born y2) c= E
;
( S3[D,x,y1,y2] & S5[D,x,y1,y2] )
thus
S3[D,x,y1,y2]
S5[D,x,y1,y2]
assume
y1 < y2
;
( ( for x being Surreal st x in L_ x holds
S4[D,x,x,y1,y2] ) & ( for x being Surreal st x in R_ x holds
S4[D,x,x,y1,y2] ) )
per cases then
( ex y2L being Surreal st
( y2L in L_ y2 & y1 <= y2L & y2L < y2 ) or ex y1R being Surreal st
( y1R in R_ y1 & y1 < y1R & y1R <= y2 ) )
by SURREALO:13;
suppose
ex y2L being Surreal st
( y2L in L_ y2 & y1 <= y2L & y2L < y2 )
;
( ( for x being Surreal st x in L_ x holds
S4[D,x,x,y1,y2] ) & ( for x being Surreal st x in R_ x holds
S4[D,x,x,y1,y2] ) )
then consider y2L being
Surreal such that A244:
( y2L in L_ y2 & y1 <= y2L & y2L < y2 )
;
A245:
for xL being Surreal st xL in L_ x holds
S4[D,xL,x,y1,y2]
proof
let xL be
Surreal;
( xL in L_ x implies S4[D,xL,x,y1,y2] )
assume A246:
xL in L_ x
;
S4[D,xL,x,y1,y2]
let xLy2, xy1, xLy1, xy2 be
Surreal;
( (born xL) (+) (born y1) c= D & (born x) (+) (born y1) c= D & (born xL) (+) (born y2) c= D & (born x) (+) (born y2) c= D & xLy1 = xL * y1 & xLy2 = xL * y2 & xy1 = x * y1 & xy2 = x * y2 & xL < x & y1 < y2 implies xLy2 + xy1 < xLy1 + xy2 )
assume that A247:
( (born xL) (+) (born y1) c= D & (born x) (+) (born y1) c= D & (born xL) (+) (born y2) c= D & (born x) (+) (born y2) c= D )
and A248:
( xLy1 = xL * y1 & xLy2 = xL * y2 & xy1 = x * y1 & xy2 = x * y2 )
and A249:
( xL < x & y1 < y2 )
;
xLy2 + xy1 < xLy1 + xy2
A250:
xy2 = [((comp ((L_ x),x,y2,(L_ y2))) \/ (comp ((R_ x),x,y2,(R_ y2)))),((comp ((L_ x),x,y2,(R_ y2))) \/ (comp ((R_ x),x,y2,(L_ y2))))]
by A248, Th50;
A251:
( L_ xy2 << {xy2} & {xy2} << R_ xy2 & xy2 in {xy2} )
by SURREALO:11, TARSKI:def 1;
A252:
y2L in (L_ y2) \/ (R_ y2)
by A244, XBOOLE_0:def 3;
then A253:
(born x) (+) (born y2L) in (born x) (+) (born y2)
by SURREALO:1, ORDINAL7:94;
then reconsider xy2L = x
* y2L as
Surreal by A2, A247;
A254:
xL in (L_ x) \/ (R_ x)
by A246, XBOOLE_0:def 3;
then A255:
(born xL) (+) (born y2L) in (born x) (+) (born y2L)
by SURREALO:1, ORDINAL7:94;
then A256:
(born xL) (+) (born y2L) in D
by A247, A253, ORDINAL1:10;
then reconsider xLy2L = xL
* y2L as
Surreal by A2;
(xLy2 +' xy2L) +' (-' xLy2L) in comp ((L_ x),x,y2,(L_ y2))
by A246, A244, A248, Def14;
then
(xLy2 +' xy2L) +' (-' xLy2L) in L_ xy2
by A250, XBOOLE_0:def 3;
then
(xLy2 + xy2L) - xLy2L < xy2
by A251;
then A257:
xLy2 + xy2L < xy2 + xLy2L
by Th41;
A258:
((born y1) (+) (born y2)) (+) (born x) = ((born x) (+) (born y1)) (+) (born y2)
by ORDINAL7:68;
A259:
(born y2L) (+) (born x) c= D
by A253, A247, ORDINAL1:def 2;
A260:
( y2L * x = xy2L & y1 * x = xy1 )
by A253, A247, A248, A3, ORDINAL1:def 2;
A261:
(born y2L) (+) (born xL) c= D
by A255, A247, A253, ORDINAL1:10, ORDINAL1:def 2;
A262:
y2L * xL = xLy2L
by A3, A256, ORDINAL1:def 2;
A263:
y1 * xL = xLy1
by A247, A248, A3;
A264:
(born y2L) (+) (born y1) in (born y1) (+) (born y2)
by A252, SURREALO:1, ORDINAL7:94;
then A265:
((born y2L) (+) (born y1)) (+) (born x) in ((born y2) (+) (born y1)) (+) (born x)
by ORDINAL7:94;
then A266:
((born y2L) (+) (born y1)) (+) (born x) in E
by A241, A258;
( ((born y2L) (+) (born y1)) (+) (born xL) in ((born y2) (+) (born y1)) (+) (born xL) & ((born y2) (+) (born y1)) (+) (born xL) in ((born y2) (+) (born y1)) (+) (born x) )
by A254, SURREALO:1, A264, ORDINAL7:94;
then A267:
((born y2L) (+) (born y1)) (+) (born xL) in ((born y1) (+) (born y2)) (+) (born x)
by ORDINAL1:10;
per cases
( y1 < y2L or y1 == y2L )
by A244;
suppose A268:
y1 < y2L
;
xLy2 + xy1 < xLy1 + xy2
((born x) (+) (born y1)) (+) (born y2L) in E
by A266, ORDINAL7:68;
then A269:
xLy2L + xy1 <= xLy1 + xy2L
by A246, A159, A249, A268, A261, A247, A248, A259;
A270:
(xLy2L + xy1) + (xLy2 + xy2L) < (xLy1 + xy2L) + (xy2 + xLy2L)
by A257, A269, Th44;
A271:
(xLy2L + xy1) + (xLy2 + xy2L) =
xLy2L
+ (xy1 + (xLy2 + xy2L))
by Th37
.=
xLy2L
+ ((xy1 + xLy2) + xy2L)
by Th37
.=
(xLy2L + xy2L) + (xLy2 + xy1)
by Th37
;
(xLy1 + xy2L) + (xy2 + xLy2L) =
xy2L
+ (xLy1 + (xy2 + xLy2L))
by Th37
.=
xy2L
+ ((xLy1 + xy2) + xLy2L)
by Th37
.=
(xLy2L + xy2L) + (xLy1 + xy2)
by Th37
;
hence
xLy2 + xy1 < xLy1 + xy2
by A270, A271, Th43;
verum
end;
suppose A272:
y1 == y2L
;
xLy2 + xy1 < xLy1 + xy2
A273:
xy2L == xy1
by A241, A258, A265, A159, A247, A259, A272, A260;
A274:
xLy2L == xLy1
by A261, A263, A262, A247, A272, A267, A159, A241, A258;
A275:
xy2 + xLy2L <= xLy1 + xy2
by A274, Th32;
A276:
xLy2 + xy1 <= xLy2 + xy2L
by A273, Th32;
xLy2 + xy1 < xy2 + xLy2L
by A257, A276, SURREALO:4;
hence
xLy2 + xy1 < xLy1 + xy2
by A275, SURREALO:4;
verum
end;
end;
end;
for xR being Surreal st xR in R_ x holds
S4[D,x,xR,y1,y2]
proof
let xR be
Surreal;
( xR in R_ x implies S4[D,x,xR,y1,y2] )
assume A277:
xR in R_ x
;
S4[D,x,xR,y1,y2]
let xy2, xRy1, xy1, xRy2 be
Surreal;
( (born x) (+) (born y1) c= D & (born xR) (+) (born y1) c= D & (born x) (+) (born y2) c= D & (born xR) (+) (born y2) c= D & xy1 = x * y1 & xy2 = x * y2 & xRy1 = xR * y1 & xRy2 = xR * y2 & x < xR & y1 < y2 implies xy2 + xRy1 < xy1 + xRy2 )
assume that A278:
( (born x) (+) (born y1) c= D & (born xR) (+) (born y1) c= D & (born x) (+) (born y2) c= D & (born xR) (+) (born y2) c= D )
and A279:
( xy1 = x * y1 & xy2 = x * y2 & xRy1 = xR * y1 & xRy2 = xR * y2 )
and A280:
( x < xR & y1 < y2 )
;
xy2 + xRy1 < xy1 + xRy2
A281:
xy2 = [((comp ((L_ x),x,y2,(L_ y2))) \/ (comp ((R_ x),x,y2,(R_ y2)))),((comp ((L_ x),x,y2,(R_ y2))) \/ (comp ((R_ x),x,y2,(L_ y2))))]
by A279, Th50;
A282:
( L_ xy2 << {xy2} & {xy2} << R_ xy2 & xy2 in {xy2} )
by SURREALO:11, TARSKI:def 1;
A283:
y2L in (L_ y2) \/ (R_ y2)
by A244, XBOOLE_0:def 3;
A284:
(born x) (+) (born y2L) in (born x) (+) (born y2)
by A283, SURREALO:1, ORDINAL7:94;
reconsider xy2L = x
* y2L as
Surreal by A2, A284, A278;
A285:
xR in (L_ x) \/ (R_ x)
by A277, XBOOLE_0:def 3;
A286:
(born xR) (+) (born y2L) in (born x) (+) (born y2L)
by A285, SURREALO:1, ORDINAL7:94;
then A287:
(born xR) (+) (born y2L) in D
by A278, A284, ORDINAL1:10;
then reconsider xRy2L = xR
* y2L as
Surreal by A2;
(xRy2 +' xy2L) +' (-' xRy2L) in comp ((R_ x),x,y2,(L_ y2))
by A277, A244, A279, Def14;
then
(xRy2 +' xy2L) +' (-' xRy2L) in R_ xy2
by A281, XBOOLE_0:def 3;
then A288:
xy2 < (xRy2 + xy2L) - xRy2L
by A282;
then A289:
xy2 + xRy2L < xRy2 + xy2L
by Th42;
A290:
((born y1) (+) (born y2)) (+) (born x) = ((born x) (+) (born y1)) (+) (born y2)
by ORDINAL7:68;
A291:
(born y2L) (+) (born x) c= D
by A284, A278, ORDINAL1:def 2;
A292:
( y2L * x = xy2L & y1 * x = xy1 )
by A284, A278, A279, A3, ORDINAL1:def 2;
A293:
(born y2L) (+) (born xR) c= D
by A286, A278, A284, ORDINAL1:10, ORDINAL1:def 2;
A294:
y2L * xR = xRy2L
by A3, A287, ORDINAL1:def 2;
A295:
y1 * xR = xRy1
by A278, A279, A3;
A296:
(born y2L) (+) (born y1) in (born y1) (+) (born y2)
by A283, SURREALO:1, ORDINAL7:94;
then A297:
((born y2L) (+) (born y1)) (+) (born x) in ((born y1) (+) (born y2)) (+) (born x)
by ORDINAL7:94;
then A298:
((born y2L) (+) (born y1)) (+) (born x) in E
by A241, A290;
( ((born y2L) (+) (born y1)) (+) (born xR) in ((born y2) (+) (born y1)) (+) (born xR) & ((born y2) (+) (born y1)) (+) (born xR) in ((born y2) (+) (born y1)) (+) (born x) )
by A285, SURREALO:1, A296, ORDINAL7:94;
then A299:
((born y2L) (+) (born y1)) (+) (born xR) in ((born y1) (+) (born y2)) (+) (born x)
by ORDINAL1:10;
per cases
( y1 < y2L or y1 == y2L )
by A244;
suppose A300:
y1 < y2L
;
xy2 + xRy1 < xy1 + xRy2
((born x) (+) (born y1)) (+) (born y2L) in E
by A298, ORDINAL7:68;
then A301:
xy2L + xRy1 < xy1 + xRy2L
by A277, A159, A280, A300, A293, A278, A279, A291;
xy2 + xRy2L <= xRy2 + xy2L
by Th42, A288;
then A302:
(xy2 + xRy2L) + (xy2L + xRy1) < (xRy2 + xy2L) + (xy1 + xRy2L)
by A301, Th44;
A303:
(xy2 + xRy2L) + (xy2L + xRy1) =
xy2
+ (xRy2L + (xy2L + xRy1))
by Th37
.=
xy2
+ ((xRy2L + xy2L) + xRy1)
by Th37
.=
(xy2 + xRy1) + (xRy2L + xy2L)
by Th37
;
(xRy2 + xy2L) + (xy1 + xRy2L) =
xy2L
+ (xRy2 + (xy1 + xRy2L))
by Th37
.=
xy2L
+ ((xRy2 + xy1) + xRy2L)
by Th37
.=
(xy1 + xRy2) + (xRy2L + xy2L)
by Th37
;
hence
xy2 + xRy1 < xy1 + xRy2
by A303, A302, Th43;
verum
end;
suppose A304:
y1 == y2L
;
xy2 + xRy1 < xy1 + xRy2
A305:
xy1 == xy2L
by A159, A297, A241, A290, A278, A291, A304, A292;
A306:
xRy1 == xRy2L
by A293, A295, A294, A278, A304, A299, A159, A241, A290;
A307:
xy2 + xRy1 <= xy2 + xRy2L
by A306, Th32;
A308:
xRy2 + xy2L <= xy1 + xRy2
by A305, Th32;
xy2 + xRy1 < xRy2 + xy2L
by A289, A307, SURREALO:4;
hence
xy2 + xRy1 < xy1 + xRy2
by A308, SURREALO:4;
verum
end;
end;
end;
hence
( ( for x being Surreal st x in L_ x holds
S4[D,x,x,y1,y2] ) & ( for x being Surreal st x in R_ x holds
S4[D,x,x,y1,y2] ) )
by A245;
verum
end;
suppose
ex y1R being Surreal st
( y1R in R_ y1 & y1 < y1R & y1R <= y2 )
;
( ( for x being Surreal st x in L_ x holds
S4[D,x,x,y1,y2] ) & ( for x being Surreal st x in R_ x holds
S4[D,x,x,y1,y2] ) )
then consider y1R being
Surreal such that A309:
( y1R in R_ y1 & y1 < y1R & y1R <= y2 )
;
A310:
for xL being Surreal st xL in L_ x holds
S4[D,xL,x,y1,y2]
proof
let xL be
Surreal;
( xL in L_ x implies S4[D,xL,x,y1,y2] )
assume A311:
xL in L_ x
;
S4[D,xL,x,y1,y2]
let xLy2, xy1, xLy1, xy2 be
Surreal;
( (born xL) (+) (born y1) c= D & (born x) (+) (born y1) c= D & (born xL) (+) (born y2) c= D & (born x) (+) (born y2) c= D & xLy1 = xL * y1 & xLy2 = xL * y2 & xy1 = x * y1 & xy2 = x * y2 & xL < x & y1 < y2 implies xLy2 + xy1 < xLy1 + xy2 )
assume that A312:
( (born xL) (+) (born y1) c= D & (born x) (+) (born y1) c= D & (born xL) (+) (born y2) c= D & (born x) (+) (born y2) c= D )
and A313:
( xLy1 = xL * y1 & xLy2 = xL * y2 & xy1 = x * y1 & xy2 = x * y2 )
and A314:
( xL < x & y1 < y2 )
;
xLy2 + xy1 < xLy1 + xy2
A315:
xy1 = [((comp ((L_ x),x,y1,(L_ y1))) \/ (comp ((R_ x),x,y1,(R_ y1)))),((comp ((L_ x),x,y1,(R_ y1))) \/ (comp ((R_ x),x,y1,(L_ y1))))]
by A313, Th50;
A316:
( L_ xy1 << {xy1} & {xy1} << R_ xy1 & xy1 in {xy1} )
by SURREALO:11, TARSKI:def 1;
A317:
y1R in (L_ y1) \/ (R_ y1)
by A309, XBOOLE_0:def 3;
A318:
(born x) (+) (born y1R) in (born x) (+) (born y1)
by A317, SURREALO:1, ORDINAL7:94;
reconsider xy1R = x
* y1R as
Surreal by A2, A312, A318;
A319:
xL in (L_ x) \/ (R_ x)
by A311, XBOOLE_0:def 3;
then A320:
(born xL) (+) (born y1R) in (born x) (+) (born y1R)
by SURREALO:1, ORDINAL7:94;
then A321:
(born xL) (+) (born y1R) in (born x) (+) (born y1)
by A318, ORDINAL1:10;
A322:
(born xL) (+) (born y1R) in D
by A320, A318, ORDINAL1:10, A312;
reconsider xLy1R = xL
* y1R as
Surreal by A321, A2, A312;
(xLy1 +' xy1R) +' (-' xLy1R) in comp ((L_ x),x,y1,(R_ y1))
by A311, A309, A313, Def14;
then
(xLy1 +' xy1R) +' (-' xLy1R) in R_ xy1
by A315, XBOOLE_0:def 3;
then A323:
xy1 < (xLy1 + xy1R) - xLy1R
by A316;
then A324:
xy1 + xLy1R < xLy1 + xy1R
by Th42;
A325:
((born y1) (+) (born y2)) (+) (born x) = ((born x) (+) (born y1)) (+) (born y2)
by ORDINAL7:68;
A326:
(born y1R) (+) (born x) c= D
by A318, A312, ORDINAL1:def 2;
A327:
( y1R * x = xy1R & y2 * x = xy2 )
by A318, A312, ORDINAL1:def 2, A313, A3;
A328:
(born y1R) (+) (born xL) c= D
by A320, A318, ORDINAL1:10, A312, ORDINAL1:def 2;
A329:
y1R * xL = xLy1R
by A3, A322, ORDINAL1:def 2;
A330:
y2 * xL = xLy2
by A312, A313, A3;
A331:
(born y1R) (+) (born y2) in (born y1) (+) (born y2)
by A317, SURREALO:1, ORDINAL7:94;
then A332:
((born y1R) (+) (born y2)) (+) (born x) in ((born y1) (+) (born y2)) (+) (born x)
by ORDINAL7:94;
then A333:
((born y1R) (+) (born y2)) (+) (born x) in E
by A241, A325;
( ((born y1R) (+) (born y2)) (+) (born xL) in ((born y1) (+) (born y2)) (+) (born xL) & ((born y1) (+) (born y2)) (+) (born xL) in ((born y1) (+) (born y2)) (+) (born x) )
by A319, SURREALO:1, A331, ORDINAL7:94;
then A334:
((born y1R) (+) (born y2)) (+) (born xL) in ((born y1) (+) (born y2)) (+) (born x)
by ORDINAL1:10;
per cases
( y1R < y2 or y1R == y2 )
by A309;
suppose A335:
y1R < y2
;
xLy2 + xy1 < xLy1 + xy2
((born x) (+) (born y1R)) (+) (born y2) in E
by A333, ORDINAL7:68;
then A336:
xLy2 + xy1R < xLy1R + xy2
by A159, A311, A314, A335, A328, A312, A313, A326;
xy1 + xLy1R <= xLy1 + xy1R
by A323, Th42;
then A337:
(xy1 + xLy1R) + (xLy2 + xy1R) < (xLy1 + xy1R) + (xLy1R + xy2)
by A336, Th44;
A338:
(xy1 + xLy1R) + (xLy2 + xy1R) =
xy1
+ (xLy1R + (xLy2 + xy1R))
by Th37
.=
xy1
+ (xLy2 + (xLy1R + xy1R))
by Th37
.=
(xy1 + xLy2) + (xLy1R + xy1R)
by Th37
;
(xLy1 + xy1R) + (xLy1R + xy2) =
xLy1
+ (xy1R + (xLy1R + xy2))
by Th37
.=
xLy1
+ ((xy1R + xLy1R) + xy2)
by Th37
.=
(xLy1 + xy2) + (xy1R + xLy1R)
by Th37
;
hence
xLy2 + xy1 < xLy1 + xy2
by A337, A338, Th43;
verum
end;
suppose A339:
y1R == y2
;
xLy2 + xy1 < xLy1 + xy2
A340:
xy1R == xy2
by A332, A241, A325, A159, A312, A326, A339, A327;
A341:
xLy1R == xLy2
by A328, A330, A329, A312, A339, A334, A159, A241, A325;
A342:
xy1 + xLy2 <= xy1 + xLy1R
by A341, Th32;
A343:
xLy1 + xy1R <= xLy1 + xy2
by A340, Th32;
xy1 + xLy2 < xLy1 + xy1R
by A324, A342, SURREALO:4;
hence
xLy2 + xy1 < xLy1 + xy2
by A343, SURREALO:4;
verum
end;
end;
end;
for xR being Surreal st xR in R_ x holds
S4[D,x,xR,y1,y2]
proof
let xR be
Surreal;
( xR in R_ x implies S4[D,x,xR,y1,y2] )
assume A344:
xR in R_ x
;
S4[D,x,xR,y1,y2]
let xy2, xRy1, xy1, xRy2 be
Surreal;
( (born x) (+) (born y1) c= D & (born xR) (+) (born y1) c= D & (born x) (+) (born y2) c= D & (born xR) (+) (born y2) c= D & xy1 = x * y1 & xy2 = x * y2 & xRy1 = xR * y1 & xRy2 = xR * y2 & x < xR & y1 < y2 implies xy2 + xRy1 < xy1 + xRy2 )
assume that A345:
( (born x) (+) (born y1) c= D & (born xR) (+) (born y1) c= D & (born x) (+) (born y2) c= D & (born xR) (+) (born y2) c= D )
and A346:
( xy1 = x * y1 & xy2 = x * y2 & xRy1 = xR * y1 & xRy2 = xR * y2 )
and A347:
( x < xR & y1 < y2 )
;
xy2 + xRy1 < xy1 + xRy2
A348:
xy1 = [((comp ((L_ x),x,y1,(L_ y1))) \/ (comp ((R_ x),x,y1,(R_ y1)))),((comp ((L_ x),x,y1,(R_ y1))) \/ (comp ((R_ x),x,y1,(L_ y1))))]
by A346, Th50;
A349:
( L_ xy1 << {xy1} & {xy1} << R_ xy1 & xy1 in {xy1} )
by SURREALO:11, TARSKI:def 1;
A350:
y1R in (L_ y1) \/ (R_ y1)
by A309, XBOOLE_0:def 3;
A351:
(born x) (+) (born y1R) in (born x) (+) (born y1)
by SURREALO:1, A350, ORDINAL7:94;
then reconsider xy1R = x
* y1R as
Surreal by A2, A345;
A352:
xR in (L_ x) \/ (R_ x)
by A344, XBOOLE_0:def 3;
A353:
(born xR) (+) (born y1R) in (born x) (+) (born y1R)
by A352, SURREALO:1, ORDINAL7:94;
then A354:
(born xR) (+) (born y1R) in D
by A345, A351, ORDINAL1:10;
then reconsider xRy1R = xR
* y1R as
Surreal by A2;
(xRy1 +' xy1R) +' (-' xRy1R) in comp ((R_ x),x,y1,(R_ y1))
by A344, A309, A346, Def14;
then
(xRy1 +' xy1R) +' (-' xRy1R) in L_ xy1
by A348, XBOOLE_0:def 3;
then A355:
(xRy1 + xy1R) - xRy1R < xy1
by A349;
then A356:
xRy1 + xy1R < xy1 + xRy1R
by Th41;
A357:
((born y1) (+) (born y2)) (+) (born x) = ((born x) (+) (born y1)) (+) (born y2)
by ORDINAL7:68;
A358:
(born y1R) (+) (born x) c= D
by A351, A345, ORDINAL1:def 2;
A359:
( y1R * x = xy1R & y2 * x = xy2 )
by A345, A346, A3, A351, ORDINAL1:def 2;
A360:
(born y1R) (+) (born xR) c= D
by A353, A345, A351, ORDINAL1:10, ORDINAL1:def 2;
A361:
y1R * xR = xRy1R
by A3, A354, ORDINAL1:def 2;
A362:
y2 * xR = xRy2
by A345, A346, A3;
A363:
(born y1R) (+) (born y2) in (born y1) (+) (born y2)
by A350, SURREALO:1, ORDINAL7:94;
then A364:
((born y1R) (+) (born y2)) (+) (born x) in ((born y1) (+) (born y2)) (+) (born x)
by ORDINAL7:94;
then A365:
((born y1R) (+) (born y2)) (+) (born x) in E
by A241, A357;
( ((born y1R) (+) (born y2)) (+) (born xR) in ((born y1) (+) (born y2)) (+) (born xR) & ((born y1) (+) (born y2)) (+) (born xR) in ((born y1) (+) (born y2)) (+) (born x) )
by A352, SURREALO:1, A363, ORDINAL7:94;
then A366:
((born y1R) (+) (born y2)) (+) (born xR) in ((born y1) (+) (born y2)) (+) (born x)
by ORDINAL1:10;
per cases
( y1R < y2 or y1R == y2 )
by A309;
suppose A367:
y1R < y2
;
xy2 + xRy1 < xy1 + xRy2
((born x) (+) (born y1R)) (+) (born y2) in E
by A365, ORDINAL7:68;
then A368:
xy2 + xRy1R < xy1R + xRy2
by A344, A159, A347, A367, A360, A345, A346, A358;
xRy1 + xy1R <= xy1 + xRy1R
by A355, Th41;
then A369:
(xRy1 + xy1R) + (xy2 + xRy1R) < (xy1 + xRy1R) + (xy1R + xRy2)
by A368, Th44;
A370:
(xRy1 + xy1R) + (xy2 + xRy1R) =
xRy1
+ (xy1R + (xRy1R + xy2))
by Th37
.=
xRy1
+ ((xy1R + xRy1R) + xy2)
by Th37
.=
(xy1R + xRy1R) + (xy2 + xRy1)
by Th37
;
(xy1 + xRy1R) + (xy1R + xRy2) =
xy1
+ (xRy1R + (xy1R + xRy2))
by Th37
.=
xy1
+ ((xRy1R + xy1R) + xRy2)
by Th37
.=
(xy1 + xRy2) + (xRy1R + xy1R)
by Th37
;
hence
xy2 + xRy1 < xy1 + xRy2
by A370, A369, Th43;
verum
end;
suppose A371:
y1R == y2
;
xy2 + xRy1 < xy1 + xRy2
A372:
xy1R == xy2
by A159, A364, A241, A357, A345, A358, A371, A359;
A373:
xRy1R == xRy2
by A360, A362, A361, A345, A371, A366, A159, A241, A357;
A374:
xy1 + xRy1R <= xy1 + xRy2
by A373, Th32;
A375:
xy2 + xRy1 <= xy1R + xRy1
by A372, Th32;
xRy1 + xy1R < xy1 + xRy2
by A356, A374, SURREALO:4;
hence
xy2 + xRy1 < xy1 + xRy2
by A375, SURREALO:4;
verum
end;
end;
end;
hence
( ( for x being Surreal st x in L_ x holds
S4[D,x,x,y1,y2] ) & ( for x being Surreal st x in R_ x holds
S4[D,x,x,y1,y2] ) )
by A310;
verum
end;
end;
end;
A376:
for E being Ordinal holds S11[E]
from ORDINAL1:sch 2(A158);
thus
for x1, x2, y being Surreal holds S3[D,x1,x2,y]
S9[D]
defpred S
12[
Ordinal]
means for x1, x2, y1, y2 being
Surreal st
(born x1) (+) (born x2) c= $1 holds
S
4[D,x1,x2,y1,y2];
A377:
for E being Ordinal st ( for C being Ordinal st C in E holds
S12[C] ) holds
S12[E]
proof
let E be
Ordinal;
( ( for C being Ordinal st C in E holds
S12[C] ) implies S12[E] )
assume A378:
for C being Ordinal st C in E holds
S12[C]
;
S12[E]
let x1, x2, y1, y2 be
Surreal;
( (born x1) (+) (born x2) c= E implies S4[D,x1,x2,y1,y2] )
assume A379:
(born x1) (+) (born x2) c= E
;
S4[D,x1,x2,y1,y2]
let x1y2, x2y1, x1y1, x2y2 be
Surreal;
( (born x1) (+) (born y1) c= D & (born x2) (+) (born y1) c= D & (born x1) (+) (born y2) c= D & (born x2) (+) (born y2) c= D & x1y1 = x1 * y1 & x1y2 = x1 * y2 & x2y1 = x2 * y1 & x2y2 = x2 * y2 & x1 < x2 & y1 < y2 implies x1y2 + x2y1 < x1y1 + x2y2 )
assume that A380:
( (born x1) (+) (born y1) c= D & (born x2) (+) (born y1) c= D & (born x1) (+) (born y2) c= D & (born x2) (+) (born y2) c= D )
and A381:
( x1y1 = x1 * y1 & x1y2 = x1 * y2 & x2y1 = x2 * y1 & x2y2 = x2 * y2 & x1 < x2 & y1 < y2 )
;
x1y2 + x2y1 < x1y1 + x2y2
per cases
( ex x1R being Surreal st
( x1R in R_ x1 & x1 < x1R & x1R <= x2 ) or ex x2L being Surreal st
( x2L in L_ x2 & x1 <= x2L & x2L < x2 ) )
by A381, SURREALO:13;
suppose
ex x1R being Surreal st
( x1R in R_ x1 & x1 < x1R & x1R <= x2 )
;
x1y2 + x2y1 < x1y1 + x2y2
then consider x1R being
Surreal such that A382:
( x1R in R_ x1 & x1 < x1R & x1R <= x2 )
;
x1R in (L_ x1) \/ (R_ x1)
by A382, XBOOLE_0:def 3;
then A383:
( (born x1R) (+) (born x2) in (born x1) (+) (born x2) & (born x1R) (+) (born y1) in (born x1) (+) (born y1) & (born x1R) (+) (born y2) in (born x1) (+) (born y2) )
by SURREALO:1, ORDINAL7:94;
then reconsider x1Ry1 = x1R
* y1, x1Ry2 = x1R
* y2 as
Surreal by A2, A380;
A384:
( (born x1R) (+) (born y1) c= D & (born x1R) (+) (born y2) c= D )
by A383, A380, ORDINAL1:def 2;
per cases
( x1R == x2 or x1R < x2 )
by A382;
suppose A385:
x1R == x2
;
x1y2 + x2y1 < x1y1 + x2y2
((born x1R) (+) (born x2)) (+) (born y1) c= ((born x1R) (+) (born x2)) (+) (born y1)
;
then A386:
x1Ry1 == x2y1
by A376, A385, A384, A380, A381;
((born x1R) (+) (born x2)) (+) (born y2) c= ((born x1R) (+) (born x2)) (+) (born y2)
;
then A387:
x1Ry2 == x2y2
by A376, A385, A384, A380, A381;
((born x1) (+) (born y1)) (+) (born y2) c= ((born x1) (+) (born y1)) (+) (born y2)
;
then A388:
x1y2 + x1Ry1 < x1y1 + x1Ry2
by A376, A382, A380, A381, A384;
A389:
x1y1 + x1Ry2 <= x1y1 + x2y2
by A387, Th32;
x1y2 + x2y1 <= x1y2 + x1Ry1
by A386, Th32;
then
x1y2 + x2y1 < x1y1 + x1Ry2
by A388, SURREALO:4;
hence
x1y2 + x2y1 < x1y1 + x2y2
by SURREALO:4, A389;
verum
end;
suppose
x1R < x2
;
x1y2 + x2y1 < x1y1 + x2y2
then A390:
x1Ry2 + x2y1 < x1Ry1 + x2y2
by A384, A383, A378, A379, A380, A381;
((born x1) (+) (born y1)) (+) (born y2) c= ((born x1) (+) (born y1)) (+) (born y2)
;
then
x1y2 + x1Ry1 <= x1y1 + x1Ry2
by A376, A384, A382, A380, A381;
then A391:
(x1Ry2 + x2y1) + (x1y2 + x1Ry1) < (x1Ry1 + x2y2) + (x1y1 + x1Ry2)
by A390, Th44;
A392:
(x1Ry2 + x2y1) + (x1y2 + x1Ry1) =
x1Ry2
+ (x2y1 + (x1y2 + x1Ry1))
by Th37
.=
x1Ry2
+ ((x2y1 + x1y2) + x1Ry1)
by Th37
.=
(x1Ry2 + x1Ry1) + (x1y2 + x2y1)
by Th37
;
(x1Ry1 + x2y2) + (x1y1 + x1Ry2) =
x1Ry1
+ (x2y2 + (x1y1 + x1Ry2))
by Th37
.=
x1Ry1
+ ((x2y2 + x1y1) + x1Ry2)
by Th37
.=
(x1Ry1 + x1Ry2) + (x2y2 + x1y1)
by Th37
;
hence
x1y2 + x2y1 < x1y1 + x2y2
by A391, A392, Th43;
verum
end;
end;
end;
suppose
ex x2L being Surreal st
( x2L in L_ x2 & x1 <= x2L & x2L < x2 )
;
x1y2 + x2y1 < x1y1 + x2y2
then consider x2L being
Surreal such that A393:
( x2L in L_ x2 & x1 <= x2L & x2L < x2 )
;
x2L in (L_ x2) \/ (R_ x2)
by A393, XBOOLE_0:def 3;
then A394:
( (born x2L) (+) (born x1) in (born x1) (+) (born x2) & (born x2L) (+) (born y1) in (born x2) (+) (born y1) & (born x2L) (+) (born y2) in (born x2) (+) (born y2) )
by SURREALO:1, ORDINAL7:94;
then reconsider x2Ly1 = x2L
* y1, x2Ly2 = x2L
* y2 as
Surreal by A2, A380;
A395:
( (born x2L) (+) (born y1) c= D & (born x2L) (+) (born y2) c= D )
by A394, A380, ORDINAL1:def 2;
per cases
( x1 == x2L or x1 < x2L )
by A393;
suppose A396:
x1 == x2L
;
x1y2 + x2y1 < x1y1 + x2y2
((born x1) (+) (born x2L)) (+) (born y1) c= ((born x1) (+) (born x2L)) (+) (born y1)
;
then A397:
x1y1 == x2Ly1
by A376, A396, A395, A380, A381;
((born x1) (+) (born x2L)) (+) (born y2) c= ((born x1) (+) (born x2L)) (+) (born y2)
;
then A398:
x1y2 == x2Ly2
by A376, A396, A395, A380, A381;
((born x2) (+) (born y1)) (+) (born y2) c= ((born x2) (+) (born y1)) (+) (born y2)
;
then A399:
x2Ly2 + x2y1 < x2Ly1 + x2y2
by A376, A393, A380, A381, A395;
A400:
x2Ly1 + x2y2 <= x1y1 + x2y2
by A397, Th32;
x1y2 + x2y1 <= x2Ly2 + x2y1
by A398, Th32;
then
x1y2 + x2y1 < x2Ly1 + x2y2
by A399, SURREALO:4;
hence
x1y2 + x2y1 < x1y1 + x2y2
by A400, SURREALO:4;
verum
end;
suppose
x1 < x2L
;
x1y2 + x2y1 < x1y1 + x2y2
then A401:
x1y2 + x2Ly1 < x1y1 + x2Ly2
by A395, A394, A378, A379, A380, A381;
((born x2) (+) (born y1)) (+) (born y2) c= ((born x2) (+) (born y1)) (+) (born y2)
;
then
x2Ly2 + x2y1 <= x2Ly1 + x2y2
by A376, A395, A393, A380, A381;
then A402:
(x2Ly2 + x2y1) + (x1y2 + x2Ly1) < (x2Ly1 + x2y2) + (x1y1 + x2Ly2)
by A401, Th44;
A403:
(x2Ly2 + x2y1) + (x1y2 + x2Ly1) =
x2Ly2
+ (x2y1 + (x1y2 + x2Ly1))
by Th37
.=
x2Ly2
+ ((x2y1 + x1y2) + x2Ly1)
by Th37
.=
(x1y2 + x2y1) + (x2Ly2 + x2Ly1)
by Th37
;
(x2Ly1 + x2y2) + (x1y1 + x2Ly2) =
x2Ly1
+ (x2y2 + (x1y1 + x2Ly2))
by Th37
.=
x2Ly1
+ ((x2y2 + x1y1) + x2Ly2)
by Th37
.=
(x1y1 + x2y2) + (x2Ly2 + x2Ly1)
by Th37
;
hence
x1y2 + x2y1 < x1y1 + x2y2
by A402, A403, Th43;
verum
end;
end;
end;
end;
end;
A404:
for E being Ordinal holds S12[E]
from ORDINAL1:sch 2(A377);
let x1, x2, y1, y2 be
Surreal;
S4[D,x1,x2,y1,y2]
(born x1) (+) (born x2) c= (born x1) (+) (born x2)
;
hence
S4[D,x1,x2,y1,y2]
by A404;
verum
end;
A405:
for E being Ordinal holds S10[E]
from ORDINAL1:sch 2(A1);
thus
for x, y being Surreal holds x * y is Surreal
by A405;
( ( for x, y being Surreal holds x * y = y * x ) & ( for x1, x2, y, x1y, x2y being Surreal st x1 == x2 & x1y = x1 * y & x2y = x2 * y holds
x1y == x2y ) & ( for x1, x2, y1, y2, x1y2, x2y1, x1y1, x2y2 being Surreal st x1y1 = x1 * y1 & x1y2 = x1 * y2 & x2y1 = x2 * y1 & x2y2 = x2 * y2 & x1 < x2 & y1 < y2 holds
x1y2 + x2y1 < x1y1 + x2y2 ) )
thus
for x, y being Surreal holds x * y = y * x
by A405;
( ( for x1, x2, y, x1y, x2y being Surreal st x1 == x2 & x1y = x1 * y & x2y = x2 * y holds
x1y == x2y ) & ( for x1, x2, y1, y2, x1y2, x2y1, x1y1, x2y2 being Surreal st x1y1 = x1 * y1 & x1y2 = x1 * y2 & x2y1 = x2 * y1 & x2y2 = x2 * y2 & x1 < x2 & y1 < y2 holds
x1y2 + x2y1 < x1y1 + x2y2 ) )
thus
for x1, x2, y, x1y, x2y being Surreal st x1 == x2 & x1y = x1 * y & x2y = x2 * y holds
x1y == x2y
for x1, x2, y1, y2, x1y2, x2y1, x1y1, x2y2 being Surreal st x1y1 = x1 * y1 & x1y2 = x1 * y2 & x2y1 = x2 * y1 & x2y2 = x2 * y2 & x1 < x2 & y1 < y2 holds
x1y2 + x2y1 < x1y1 + x2y2
let x1, x2, y1, y2, x1y2, x2y1, x1y1, x2y2 be
Surreal;
( x1y1 = x1 * y1 & x1y2 = x1 * y2 & x2y1 = x2 * y1 & x2y2 = x2 * y2 & x1 < x2 & y1 < y2 implies x1y2 + x2y1 < x1y1 + x2y2 )
assume A407:
( x1y1 = x1 * y1 & x1y2 = x1 * y2 & x2y1 = x2 * y1 & x2y2 = x2 * y2 & x1 < x2 & y1 < y2 )
;
x1y2 + x2y1 < x1y1 + x2y2
set B11 =
(born x1) (+) (born y1);
set B12 =
(born x1) (+) (born y2);
set B21 =
(born x2) (+) (born y1);
set B22 =
(born x2) (+) (born y2);
set B1 =
((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2));
set B2 =
((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2));
set B =
(((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2)));
( (born x1) (+) (born y1) c= ((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2)) & (born x1) (+) (born y2) c= ((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2)) & (born x2) (+) (born y1) c= ((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2)) & (born x2) (+) (born y2) c= ((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2)) & ((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2)) c= (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2))) & ((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2)) c= (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2))) )
by XBOOLE_1:7;
then
( (born x1) (+) (born y1) c= (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2))) & (born x1) (+) (born y2) c= (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2))) & (born x2) (+) (born y1) c= (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2))) & (born x2) (+) (born y2) c= (((born x1) (+) (born y1)) \/ ((born x1) (+) (born y2))) \/ (((born x2) (+) (born y1)) \/ ((born x2) (+) (born y2))) )
by XBOOLE_1:1;
hence
x1y2 + x2y1 < x1y1 + x2y2
by A405, A407;
verum