SURREALS

:: SURREALS semantic presentation

definition

let lamb be object ;
let X, Y be set ;

func sqrt (lamb,X,Y) -> surreal-membered set means :Def1: :: SURREALS:def 1
for o being object holds
( o in it iff ex x, y being Surreal st
( x in X & y in Y & not x + y == 0_No & o = (lamb +' (x * y)) * ((x + y) ") ) );

existence

proof

defpred S₁[ object , object ] means ( $1 is Surreal & $2 is Surreal & $1 in X & $2 in Y & not $1 +' $2 == 0_No );
set S = { ((lamb +' (x1 *' y1)) * ((x1 +' y1) ")) where x1 is Element of X, y1 is Element of Y : S₁[x1,y1] } ;
{ ((lamb +' (x1 *' y1)) * ((x1 +' y1) ")) where x1 is Element of X, y1 is Element of Y : S₁[x1,y1] } is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis:
assume o in { ((lamb +' (x1 *' y1)) * ((x1 +' y1) ")) where x1 is Element of X, y1 is Element of Y : S₁[x1,y1] } ; :: thesis:
then ex x1 being Element of X ex y1 being Element of Y st
( o = (lamb +' (x1 *' y1)) * ((x1 +' y1) ") & S₁[x1,y1] ) ;
hence o is surreal ; :: thesis:

end;

then reconsider S = { ((lamb +' (x1 *' y1)) * ((x1 +' y1) ")) where x1 is Element of X, y1 is Element of Y : S₁[x1,y1] } as surreal-membered set ;
take S ; :: thesis:
let o be object ; :: thesis:
thus ( o in S implies ex x1, y1 being Surreal st
( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") ) ) :: thesis:

proof

assume o in S ; :: thesis:
then consider x1 being Element of X, y1 being Element of Y such that
A1: ( o = (lamb +' (x1 *' y1)) * ((x1 +' y1) ") & S₁[x1,y1] ) ;
reconsider x1 = x1, y1 = y1 as Surreal by A1;
take x1 ; :: thesis:
take y1 ; :: thesis:
thus ( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") ) by A1; :: thesis:

end;

thus ( ex x, y being Surreal st
( x in X & y in Y & not x + y == 0_No & o = (lamb +' (x * y)) * ((x + y) ") ) implies o in S ) ; :: thesis:

end;

uniqueness

proof

let D1, D2 be surreal-membered set ; :: thesis:
assume that
A2: for o being object holds
( o in D1 iff ex x1, y1 being Surreal st
( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") ) ) and
A3: for o being object holds
( o in D2 iff ex x1, y1 being Surreal st
( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") ) ) ; :: thesis:

now :: thesis:

let o be object ; :: thesis:
( o in D1 iff ex x1, y1 being Surreal st
( x1 in X & y1 in Y & not x1 + y1 == 0_No & o = (lamb +' (x1 * y1)) * ((x1 + y1) ") ) ) by A2;
hence ( o in D1 iff o in D2 ) by A3; :: thesis:

end;

hence D1 = D2 by TARSKI:2; :: thesis:

end;

:: deftheorem Def1 defines sqrt SURREALS:def 1 :

definition

let x0 be pair object ;
let x be object ;

func transitions_of (x0,x) -> Function means :Def2: :: SURREALS:def 2
( dom it = NAT & it . 0 = x0 & ( for n being Nat holds
( it . n is pair & (it . (n + 1)) `1 = (L_ (it . n)) \/ (sqrt (x,(L_ (it . n)),(R_ (it . n)))) & (it . (n + 1)) `2 = ((R_ (it . n)) \/ (sqrt (x,(L_ (it . n)),(L_ (it . n))))) \/ (sqrt (x,(R_ (it . n)),(R_ (it . n)))) ) ) );

existence

proof

deffunc H₁( object , object ) -> object = [((L_ $2) \/ (sqrt (x,(L_ $2),(R_ $2)))),(((R_ $2) \/ (sqrt (x,(L_ $2),(L_ $2)))) \/ (sqrt (x,(R_ $2),(R_ $2))))];
consider f being Function such that
A1: ( dom f = NAT & f . 0 = x0 & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) from NAT_1:sch 11();
take f ; :: thesis:
thus ( dom f = omega & f . 0 = x0 ) by A1; :: thesis:
let k be Nat; :: thesis:
thus f . k is pair :: thesis:

proof

per cases ;

suppose k = 0 ; :: thesis:

hence f . k is pair by A1; :: thesis:

end;

suppose k > 0 ; :: thesis:

then reconsider k1 = k - 1 as Nat by NAT_1:20;
f . (k1 + 1) = H₁(k1,f . k1) by A1;
hence f . k is pair ; :: thesis:

end;

f . (k + 1) = H₁(k,f . k) by A1;
hence ( (f . (k + 1)) `1 = (L_ (f . k)) \/ (sqrt (x,(L_ (f . k)),(R_ (f . k)))) & (f . (k + 1)) `2 = ((R_ (f . k)) \/ (sqrt (x,(L_ (f . k)),(L_ (f . k))))) \/ (sqrt (x,(R_ (f . k)),(R_ (f . k)))) ) ; :: thesis:

end;

uniqueness

proof

let T1, T2 be Function; :: thesis:
assume that
A2: ( dom T1 = omega & T1 . 0 = x0 ) and
A3: for k being Nat holds
( T1 . k is pair & (T1 . (k + 1)) `1 = (L_ (T1 . k)) \/ (sqrt (x,(L_ (T1 . k)),(R_ (T1 . k)))) & (T1 . (k + 1)) `2 = ((R_ (T1 . k)) \/ (sqrt (x,(L_ (T1 . k)),(L_ (T1 . k))))) \/ (sqrt (x,(R_ (T1 . k)),(R_ (T1 . k)))) ) and
A4: ( dom T2 = omega & T2 . 0 = x0 ) and
A5: for k being Nat holds
( T2 . k is pair & (T2 . (k + 1)) `1 = (L_ (T2 . k)) \/ (sqrt (x,(L_ (T2 . k)),(R_ (T2 . k)))) & (T2 . (k + 1)) `2 = ((R_ (T2 . k)) \/ (sqrt (x,(L_ (T2 . k)),(L_ (T2 . k))))) \/ (sqrt (x,(R_ (T2 . k)),(R_ (T2 . k)))) ) ; :: thesis:
defpred S₁[ Nat] means T1 . $1 = T2 . $1;
A6: S₁[ 0 ] by A2, A4;
A7: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A8: S₁[n] ; :: thesis:
A9: ( T1 . (n + 1) is pair & T2 . (n + 1) is pair ) by A3, A5;
R_ (T1 . (n + 1)) = ((R_ (T1 . n)) \/ (sqrt (x,(L_ (T1 . n)),(L_ (T1 . n))))) \/ (sqrt (x,(R_ (T1 . n)),(R_ (T1 . n)))) by A3;
then A10: (T1 . (n + 1)) `2 = R_ (T2 . (n + 1)) by A5, A8;
L_ (T1 . (n + 1)) = (L_ (T1 . n)) \/ (sqrt (x,(L_ (T1 . n)),(R_ (T1 . n)))) by A3;
then (T1 . (n + 1)) `1 = (T2 . (n + 1)) `1 by A5, A8;
hence S₁[n + 1] by A9, A10, XTUPLE_0:2; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A7);
then for o being object st o in dom T1 holds
T1 . o = T2 . o by A2;
hence T1 = T2 by A2, A4, FUNCT_1:2; :: thesis:

end;

:: deftheorem Def2 defines transitions_of SURREALS:def 2 :

definition

let x0 be pair object ;
let x be object ;

func sqrtL (x0,x) -> Function means :Def3: :: SURREALS:def 3
( dom it = NAT & ( for k being Nat holds it . k = ((transitions_of (x0,x)) . k) `1 ) );

existence

proof

deffunc H₁( object ) -> object = ((transitions_of (x0,x)) . $1) `1 ;
consider f being Function such that
A1: dom f = NAT and
A2: for x being object st x in NAT holds
f . x = H₁(x) from FUNCT_1:sch 3();
take f ; :: thesis:
thus ( dom f = NAT & ( for k being Nat holds f . k = ((transitions_of (x0,x)) . k) `1 ) ) by A1, A2, ORDINAL1:def 12; :: thesis:

end;

uniqueness

proof

let D1, D2 be Function; :: thesis:
assume that
A3: ( dom D1 = NAT & ( for k being Nat holds D1 . k = ((transitions_of (x0,x)) . k) `1 ) ) and
A4: ( dom D2 = NAT & ( for k being Nat holds D2 . k = ((transitions_of (x0,x)) . k) `1 ) ) ; :: thesis:
for o being object st o in dom D1 holds
D1 . o = D2 . o

proof

let o be object ; :: thesis:
assume o in dom D1 ; :: thesis:
then reconsider a = o as Nat by A3;
thus D1 . o = ((transitions_of (x0,x)) . a) `1 by A3
.= D2 . o by A4 ; :: thesis:

end;

hence D1 = D2 by A3, A4, FUNCT_1:2; :: thesis:

end;

:: deftheorem Def3 defines sqrtL SURREALS:def 3 :

definition

let x0 be pair object ;
let x be object ;

func sqrtR (x0,x) -> Function means :Def4: :: SURREALS:def 4
( dom it = NAT & ( for k being Nat holds it . k = ((transitions_of (x0,x)) . k) `2 ) );

existence

proof

deffunc H₁( object ) -> object = ((transitions_of (x0,x)) . $1) `2 ;
consider f being Function such that
A1: dom f = NAT and
A2: for x being object st x in NAT holds
f . x = H₁(x) from FUNCT_1:sch 3();
take f ; :: thesis:
thus ( dom f = NAT & ( for k being Nat holds f . k = ((transitions_of (x0,x)) . k) `2 ) ) by A1, A2, ORDINAL1:def 12; :: thesis:

end;

uniqueness

proof

let D1, D2 be Function; :: thesis:
assume that
A3: ( dom D1 = NAT & ( for k being Nat holds D1 . k = ((transitions_of (x0,x)) . k) `2 ) ) and
A4: ( dom D2 = NAT & ( for k being Nat holds D2 . k = ((transitions_of (x0,x)) . k) `2 ) ) ; :: thesis:
for o being object st o in dom D1 holds
D1 . o = D2 . o

proof

let o be object ; :: thesis:
assume o in dom D1 ; :: thesis:
then reconsider a = o as Nat by A3;
thus D1 . o = ((transitions_of (x0,x)) . a) `2 by A3
.= D2 . o by A4 ; :: thesis:

end;

hence D1 = D2 by A3, A4, FUNCT_1:2; :: thesis:

end;

:: deftheorem Def4 defines sqrtR SURREALS:def 4 :

theorem Th1: :: SURREALS:1

for o being object
for p being pair object holds
( (sqrtL (p,o)) . 0 = L_ p & (sqrtR (p,o)) . 0 = R_ p )

proof

let o be object ; :: thesis:
let p be pair object ; :: thesis:
( (sqrtL (p,o)) . 0 = L_ ((transitions_of (p,o)) . 0) & (sqrtR (p,o)) . 0 = R_ ((transitions_of (p,o)) . 0) ) by Def3, Def4;
hence ( (sqrtL (p,o)) . 0 = L_ p & (sqrtR (p,o)) . 0 = R_ p ) by Def2; :: thesis:

end;

theorem Th2: :: SURREALS:2

for n, m being Nat
for o being object
for p being pair object st n <= m holds
( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . m & (sqrtR (p,o)) . n c= (sqrtR (p,o)) . m )

proof

let n, m be Nat; :: thesis:
let o be object ; :: thesis:
let p be pair object ; :: thesis:
defpred S₁[ Nat] means ( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . (n + $1) & (sqrtR (p,o)) . n c= (sqrtR (p,o)) . (n + $1) );
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

set T = transitions_of (p,o);
let k be Nat; :: thesis:
assume A3: S₁[k] ; :: thesis:
set nk = n + k;
A4: ( (sqrtL (p,o)) . ((n + k) + 1) = ((transitions_of (p,o)) . ((n + k) + 1)) `1 & (sqrtR (p,o)) . ((n + k) + 1) = ((transitions_of (p,o)) . ((n + k) + 1)) `2 ) by Def3, Def4;
A5: ( (sqrtL (p,o)) . (n + k) = L_ ((transitions_of (p,o)) . (n + k)) & (sqrtR (p,o)) . (n + k) = R_ ((transitions_of (p,o)) . (n + k)) ) by Def3, Def4;
( ((transitions_of (p,o)) . ((n + k) + 1)) `1 = (L_ ((transitions_of (p,o)) . (n + k))) \/ (sqrt (o,(L_ ((transitions_of (p,o)) . (n + k))),(R_ ((transitions_of (p,o)) . (n + k))))) & ((transitions_of (p,o)) . ((n + k) + 1)) `2 = ((R_ ((transitions_of (p,o)) . (n + k))) \/ (sqrt (o,(L_ ((transitions_of (p,o)) . (n + k))),(L_ ((transitions_of (p,o)) . (n + k)))))) \/ (sqrt (o,(R_ ((transitions_of (p,o)) . (n + k))),(R_ ((transitions_of (p,o)) . (n + k))))) ) by Def2;
then ( ((transitions_of (p,o)) . ((n + k) + 1)) `1 = (L_ ((transitions_of (p,o)) . (n + k))) \/ (sqrt (o,(L_ ((transitions_of (p,o)) . (n + k))),(R_ ((transitions_of (p,o)) . (n + k))))) & ((transitions_of (p,o)) . ((n + k) + 1)) `2 = (R_ ((transitions_of (p,o)) . (n + k))) \/ ((sqrt (o,(L_ ((transitions_of (p,o)) . (n + k))),(L_ ((transitions_of (p,o)) . (n + k))))) \/ (sqrt (o,(R_ ((transitions_of (p,o)) . (n + k))),(R_ ((transitions_of (p,o)) . (n + k)))))) ) by XBOOLE_1:4;
then ( L_ ((transitions_of (p,o)) . (n + k)) c= L_ ((transitions_of (p,o)) . ((n + k) + 1)) & R_ ((transitions_of (p,o)) . (n + k)) c= R_ ((transitions_of (p,o)) . ((n + k) + 1)) ) by XBOOLE_1:7;
hence S₁[k + 1] by A4, A5, A3, XBOOLE_1:1; :: thesis:

end;

A6: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
assume n <= m ; :: thesis:
then reconsider mn = m - n as Nat by NAT_1:21;
m = n + mn ;
hence ( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . m & (sqrtR (p,o)) . n c= (sqrtR (p,o)) . m ) by A6; :: thesis:

end;

theorem Th3: :: SURREALS:3

for n being Nat
for o being object
for p being pair object holds
( (sqrtL (p,o)) . (n + 1) = ((sqrtL (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n))) & (sqrtR (p,o)) . (n + 1) = (((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)))) \/ (sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n))) )

proof

let n be Nat; :: thesis:
let o be object ; :: thesis:
let p be pair object ; :: thesis:
set T = transitions_of (p,o);
A1: ( (sqrtL (p,o)) . (n + 1) = ((transitions_of (p,o)) . (n + 1)) `1 & (sqrtR (p,o)) . (n + 1) = ((transitions_of (p,o)) . (n + 1)) `2 ) by Def3, Def4;
( (sqrtL (p,o)) . n = ((transitions_of (p,o)) . n) `1 & (sqrtR (p,o)) . n = ((transitions_of (p,o)) . n) `2 ) by Def3, Def4;
hence ( (sqrtL (p,o)) . (n + 1) = ((sqrtL (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n))) & (sqrtR (p,o)) . (n + 1) = (((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)))) \/ (sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n))) ) by Def2, A1; :: thesis:

end;

theorem Th4: :: SURREALS:4

for n being Nat
for o being object
for p being pair object st L_ p is surreal-membered & R_ p is surreal-membered holds
( (sqrtL (p,o)) . n is surreal-membered & (sqrtR (p,o)) . n is surreal-membered )

proof

let n be Nat; :: thesis:
let o be object ; :: thesis:
let p be pair object ; :: thesis:
assume A1: ( L_ p is surreal-membered & R_ p is surreal-membered ) ; :: thesis:
defpred S₁[ Nat] means ( (sqrtL (p,o)) . $1 is surreal-membered & (sqrtR (p,o)) . $1 is surreal-membered );
A2: S₁[ 0 ] by A1, Th1;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A4: S₁[n] ; :: thesis:
( (sqrtL (p,o)) . (n + 1) = ((sqrtL (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n))) & (sqrtR (p,o)) . (n + 1) = (((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)))) \/ (sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n))) ) by Th3;
hence S₁[n + 1] by A4; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence ( (sqrtL (p,o)) . n is surreal-membered & (sqrtR (p,o)) . n is surreal-membered ) ; :: thesis:

end;

theorem Th5: :: SURREALS:5

for o being object
for p being pair object st L_ p is surreal-membered & R_ p is surreal-membered holds
( Union (sqrtL (p,o)) is surreal-membered & Union (sqrtR (p,o)) is surreal-membered )

proof

let o be object ; :: thesis:
let p be pair object ; :: thesis:
assume A1: ( L_ p is surreal-membered & R_ p is surreal-membered ) ; :: thesis:
thus Union (sqrtL (p,o)) is surreal-membered :: thesis:

proof

let a be object ; :: according to SURREAL0:def 16 :: thesis:
assume a in Union (sqrtL (p,o)) ; :: thesis:
then consider n being object such that
A2: ( n in dom (sqrtL (p,o)) & a in (sqrtL (p,o)) . n ) by CARD_5:2;
dom (sqrtL (p,o)) = NAT by Def3;
then reconsider n = n as Nat by A2;
(sqrtL (p,o)) . n is surreal-membered by A1, Th4;
hence a is surreal by A2; :: thesis:

end;

let a be object ; :: according to SURREAL0:def 16 :: thesis:
assume a in Union (sqrtR (p,o)) ; :: thesis:
then consider n being object such that
A3: ( n in dom (sqrtR (p,o)) & a in (sqrtR (p,o)) . n ) by CARD_5:2;
dom (sqrtR (p,o)) = NAT by Def4;
then reconsider n = n as Nat by A3;
(sqrtR (p,o)) . n is surreal-membered by A1, Th4;
hence a is surreal by A3; :: thesis:

end;

theorem Th6: :: SURREALS:6

for o being object
for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds
sqrt (o,X1,Y1) c= sqrt (o,X2,Y2)

proof

let o be object ; :: thesis:
let X1, X2, Y1, Y2 be set ; :: thesis:
assume A1: ( X1 c= X2 & Y1 c= Y2 ) ; :: thesis:
let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in sqrt (o,X1,Y1) ; :: thesis:
then ex x1, y1 being Surreal st
( x1 in X1 & y1 in Y1 & not x1 + y1 == 0_No & a = (o +' (x1 * y1)) * ((x1 + y1) ") ) by Def1;
hence a in sqrt (o,X2,Y2) by A1, Def1; :: thesis:

end;

theorem :: SURREALS:7

for o being object
for p being pair object holds Union (sqrtL (p,o)) = (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))))

proof

let o be object ; :: thesis:
let p be pair object ; :: thesis:
defpred S₁[ Nat] means (sqrtL (p,o)) . $1 c= (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))));
(sqrtL (p,o)) . 0 = L_ p by Th1;
then A1: S₁[ 0 ] by XBOOLE_1:7;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A3: S₁[n] ; :: thesis:
let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A4: a in (sqrtL (p,o)) . (n + 1) ; :: thesis:
(sqrtL (p,o)) . (n + 1) = ((sqrtL (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n))) by Th3;

per cases by XBOOLE_0:def 3, A4;

suppose a in (sqrtL (p,o)) . n ; :: thesis:

hence a in (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) by A3; :: thesis:

end;

suppose A5: a in sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n)) ; :: thesis:

( (sqrtL (p,o)) . n c= Union (sqrtL (p,o)) & (sqrtR (p,o)) . n c= Union (sqrtR (p,o)) ) by ABCMIZ_1:1;
then sqrt (o,((sqrtL (p,o)) . n),((sqrtR (p,o)) . n)) c= sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))) by Th6;
hence a in (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) by A5, XBOOLE_0:def 3; :: thesis:

end;

A6: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
thus Union (sqrtL (p,o)) c= (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in Union (sqrtL (p,o)) ; :: thesis:
then consider n being object such that
A7: ( n in dom (sqrtL (p,o)) & a in (sqrtL (p,o)) . n ) by CARD_5:2;
n in NAT by A7, Def3;
then reconsider n = n as Nat ;
(sqrtL (p,o)) . n c= (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) by A6;
hence a in (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) by A7; :: thesis:

end;

A8: sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))) c= Union (sqrtL (p,o))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o)))) ; :: thesis:
then consider x1, y1 being Surreal such that
A9: ( x1 in Union (sqrtL (p,o)) & y1 in Union (sqrtR (p,o)) & not x1 + y1 == 0_No & a = (o +' (x1 * y1)) * ((x1 + y1) ") ) by Def1;
consider n being object such that
A10: ( n in dom (sqrtL (p,o)) & x1 in (sqrtL (p,o)) . n ) by A9, CARD_5:2;
consider m being object such that
A11: ( m in dom (sqrtR (p,o)) & y1 in (sqrtR (p,o)) . m ) by A9, CARD_5:2;
( n in NAT & m in NAT ) by A11, A10, Def3, Def4;
then reconsider n = n, m = m as Nat ;
set nm = n + m;
( m <= n + m & n <= n + m ) by NAT_1:11;
then ( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . (n + m) & (sqrtR (p,o)) . m c= (sqrtR (p,o)) . (n + m) ) by Th2;
then A12: a in sqrt (o,((sqrtL (p,o)) . (n + m)),((sqrtR (p,o)) . (n + m))) by A9, A10, A11, Def1;
(sqrtL (p,o)) . ((n + m) + 1) = ((sqrtL (p,o)) . (n + m)) \/ (sqrt (o,((sqrtL (p,o)) . (n + m)),((sqrtR (p,o)) . (n + m)))) by Th3;
then A13: a in (sqrtL (p,o)) . ((n + m) + 1) by A12, XBOOLE_0:def 3;
(n + m) + 1 in NAT ;
then (n + m) + 1 in dom (sqrtL (p,o)) by Def3;
hence a in Union (sqrtL (p,o)) by A13, CARD_5:2; :: thesis:

end;

L_ p = (sqrtL (p,o)) . 0 by Th1;
then L_ p c= Union (sqrtL (p,o)) by ABCMIZ_1:1;
hence (L_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtR (p,o))))) c= Union (sqrtL (p,o)) by A8, XBOOLE_1:8; :: thesis:

end;

theorem :: SURREALS:8

for o being object
for p being pair object holds Union (sqrtR (p,o)) = ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))))

proof

let o be object ; :: thesis:
let p be pair object ; :: thesis:
defpred S₁[ Nat] means (sqrtR (p,o)) . $1 c= ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))));
(sqrtR (p,o)) . 0 = R_ p by Th1;
then A1: S₁[ 0 ] by XBOOLE_1:7, XBOOLE_1:10;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A3: S₁[n] ; :: thesis:
let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A4: a in (sqrtR (p,o)) . (n + 1) ; :: thesis:
(sqrtR (p,o)) . (n + 1) = (((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)))) \/ (sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n))) by Th3;
then ( a in ((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n))) or a in sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n)) ) by XBOOLE_0:def 3, A4;

per cases by XBOOLE_0:def 3;

suppose a in (sqrtR (p,o)) . n ; :: thesis:

hence a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) by A3; :: thesis:

end;

suppose A5: a in sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)) ; :: thesis:

(sqrtL (p,o)) . n c= Union (sqrtL (p,o)) by ABCMIZ_1:1;
then sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)) c= sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))) by Th6;
then a in (R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o))))) by A5, XBOOLE_0:def 3;
hence a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) by XBOOLE_0:def 3; :: thesis:

end;

suppose A6: a in sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n)) ; :: thesis:

(sqrtR (p,o)) . n c= Union (sqrtR (p,o)) by ABCMIZ_1:1;
then sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n)) c= sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))) by Th6;
hence a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) by A6, XBOOLE_0:def 3; :: thesis:

end;

A7: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
thus Union (sqrtR (p,o)) c= ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in Union (sqrtR (p,o)) ; :: thesis:
then consider n being object such that
A8: ( n in dom (sqrtR (p,o)) & a in (sqrtR (p,o)) . n ) by CARD_5:2;
n in NAT by A8, Def4;
then reconsider n = n as Nat ;
(sqrtR (p,o)) . n c= ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) by A7;
hence a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) by A8; :: thesis:

end;

A9: sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))) c= Union (sqrtR (p,o))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))) ; :: thesis:
then consider x1, y1 being Surreal such that
A10: ( x1 in Union (sqrtL (p,o)) & y1 in Union (sqrtL (p,o)) & not x1 + y1 == 0_No & a = (o +' (x1 * y1)) * ((x1 + y1) ") ) by Def1;
consider n being object such that
A11: ( n in dom (sqrtL (p,o)) & x1 in (sqrtL (p,o)) . n ) by A10, CARD_5:2;
consider m being object such that
A12: ( m in dom (sqrtL (p,o)) & y1 in (sqrtL (p,o)) . m ) by A10, CARD_5:2;
( n in NAT & m in NAT ) by A12, A11, Def3;
then reconsider n = n, m = m as Nat ;
set nm = n + m;
( m <= n + m & n <= n + m ) by NAT_1:11;
then ( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . (n + m) & (sqrtL (p,o)) . m c= (sqrtL (p,o)) . (n + m) ) by Th2;
then a in sqrt (o,((sqrtL (p,o)) . (n + m)),((sqrtL (p,o)) . (n + m))) by A10, A11, A12, Def1;
then A13: a in ((sqrtR (p,o)) . (n + m)) \/ (sqrt (o,((sqrtL (p,o)) . (n + m)),((sqrtL (p,o)) . (n + m)))) by XBOOLE_0:def 3;
(sqrtR (p,o)) . ((n + m) + 1) = (((sqrtR (p,o)) . (n + m)) \/ (sqrt (o,((sqrtL (p,o)) . (n + m)),((sqrtL (p,o)) . (n + m))))) \/ (sqrt (o,((sqrtR (p,o)) . (n + m)),((sqrtR (p,o)) . (n + m)))) by Th3;
then A14: a in (sqrtR (p,o)) . ((n + m) + 1) by A13, XBOOLE_0:def 3;
(n + m) + 1 in NAT ;
then (n + m) + 1 in dom (sqrtR (p,o)) by Def4;
hence a in Union (sqrtR (p,o)) by A14, CARD_5:2; :: thesis:

end;

A15: sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))) c= Union (sqrtR (p,o))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))) ; :: thesis:
then consider x1, y1 being Surreal such that
A16: ( x1 in Union (sqrtR (p,o)) & y1 in Union (sqrtR (p,o)) & not x1 + y1 == 0_No & a = (o +' (x1 * y1)) * ((x1 + y1) ") ) by Def1;
consider n being object such that
A17: ( n in dom (sqrtR (p,o)) & x1 in (sqrtR (p,o)) . n ) by A16, CARD_5:2;
consider m being object such that
A18: ( m in dom (sqrtR (p,o)) & y1 in (sqrtR (p,o)) . m ) by A16, CARD_5:2;
( n in NAT & m in NAT ) by A18, A17, Def4;
then reconsider n = n, m = m as Nat ;
set nm = n + m;
( m <= n + m & n <= n + m ) by NAT_1:11;
then ( (sqrtR (p,o)) . n c= (sqrtR (p,o)) . (n + m) & (sqrtR (p,o)) . m c= (sqrtR (p,o)) . (n + m) ) by Th2;
then A19: a in sqrt (o,((sqrtR (p,o)) . (n + m)),((sqrtR (p,o)) . (n + m))) by A16, A17, A18, Def1;
(sqrtR (p,o)) . ((n + m) + 1) = (((sqrtR (p,o)) . (n + m)) \/ (sqrt (o,((sqrtL (p,o)) . (n + m)),((sqrtL (p,o)) . (n + m))))) \/ (sqrt (o,((sqrtR (p,o)) . (n + m)),((sqrtR (p,o)) . (n + m)))) by Th3;
then A20: a in (sqrtR (p,o)) . ((n + m) + 1) by A19, XBOOLE_0:def 3;
(n + m) + 1 in NAT ;
then (n + m) + 1 in dom (sqrtR (p,o)) by Def4;
hence a in Union (sqrtR (p,o)) by A20, CARD_5:2; :: thesis:

end;

R_ p = (sqrtR (p,o)) . 0 by Th1;
then R_ p c= Union (sqrtR (p,o)) by ABCMIZ_1:1;
then (R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o))))) c= Union (sqrtR (p,o)) by A9, XBOOLE_1:8;
hence ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) c= Union (sqrtR (p,o)) by XBOOLE_1:8, A15; :: thesis:

end;

definition

let x be object ;

func NonNegativePart x -> pair set means :Def5: :: SURREALS:def 5
for o being object holds
( ( o in L_ it implies ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) ) & ( ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) implies o in L_ it ) & ( o in R_ it implies ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) ) & ( ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) implies o in R_ it ) );

existence

proof

set L = { l where l is Element of L_ x : ( l in L_ x & l is surreal & ( for ll being Surreal st ll = l holds
0_No <= ll ) ) } ;
set R = { r where r is Element of R_ x : ( r in R_ x & r is surreal & ( for rr being Surreal st rr = r holds
0_No <= rr ) ) } ;
reconsider IT = [ { l where l is Element of L_ x : ( l in L_ x & l is surreal & ( for ll being Surreal st ll = l holds
0_No <= ll ) ) } , { r where r is Element of R_ x : ( r in R_ x & r is surreal & ( for rr being Surreal st rr = r holds
0_No <= rr ) ) } ] as pair set by TARSKI:1;
take IT ; :: thesis:
let o be object ; :: thesis:
thus ( o in L_ IT implies ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) ) :: thesis:

proof

assume o in L_ IT ; :: thesis:
then consider l being Element of L_ x such that
A1: ( o = l & l in L_ x & l is surreal & ( for ll being Surreal st ll = l holds
0_No <= ll ) ) ;
reconsider l = l as Surreal by A1;
take l ; :: thesis:
thus ( o = l & l in L_ x & 0_No <= l ) by A1; :: thesis:

end;

thus ( ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) implies o in L_ IT ) :: thesis:

proof

given l being Surreal such that A2: ( o = l & l in L_ x & 0_No <= l ) ; :: thesis:
for ll being Surreal st ll = l holds
0_No <= ll by A2;
hence o in L_ IT by A2; :: thesis:

end;

thus ( o in R_ IT implies ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) ) :: thesis:

proof

assume o in R_ IT ; :: thesis:
then consider r being Element of R_ x such that
A3: ( o = r & r in R_ x & r is surreal & ( for rr being Surreal st rr = r holds
0_No <= rr ) ) ;
reconsider r = r as Surreal by A3;
take r ; :: thesis:
thus ( o = r & r in R_ x & 0_No <= r ) by A3; :: thesis:

end;

given r being Surreal such that A4: ( o = r & r in R_ x & 0_No <= r ) ; :: thesis:
for rr being Surreal st rr = r holds
0_No <= rr by A4;
hence o in R_ IT by A4; :: thesis:

end;

uniqueness

proof

let s1, s2 be pair set ; :: thesis:
assume that
A5: for o being object holds
( ( o in L_ s1 implies ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) ) & ( ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) implies o in L_ s1 ) & ( o in R_ s1 implies ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) ) & ( ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) implies o in R_ s1 ) ) and
A6: for o being object holds
( ( o in L_ s2 implies ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) ) & ( ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) implies o in L_ s2 ) & ( o in R_ s2 implies ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) ) & ( ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) implies o in R_ s2 ) ) ; :: thesis:

now :: thesis:

let o be object ; :: thesis:
( o in R_ s1 iff ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) ) by A5;
hence ( o in R_ s1 iff o in R_ s2 ) by A6; :: thesis:

end;

then A7: R_ s1 = R_ s2 by TARSKI:2;

now :: thesis:

let o be object ; :: thesis:
( o in L_ s1 iff ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) ) by A5;
hence ( o in L_ s1 iff o in L_ s2 ) by A6; :: thesis:

end;

then L_ s1 = L_ s2 by TARSKI:2;
hence s1 = s2 by A7, XTUPLE_0:2; :: thesis:

end;

:: deftheorem Def5 defines NonNegativePart SURREALS:def 5 :

registration

let x be object ;

cluster (NonNegativePart x) `1 -> surreal-membered for set ;

coherence

proof

now :: thesis:

let o be object ; :: thesis:
assume o in L_ (NonNegativePart x) ; :: thesis:
then ex l being Surreal st
( o = l & l in L_ x & 0_No <= l ) by Def5;
hence o is surreal ; :: thesis:

end;

hence for b₁ being set st b₁ = L_ (NonNegativePart x) holds
b₁ is surreal-membered ; :: thesis:

end;

cluster (NonNegativePart x) `2 -> surreal-membered for set ;

coherence

proof

now :: thesis:

let o be object ; :: thesis:
assume o in R_ (NonNegativePart x) ; :: thesis:
then ex r being Surreal st
( o = r & r in R_ x & 0_No <= r ) by Def5;
hence o is surreal ; :: thesis:

end;

hence for b₁ being set st b₁ = R_ (NonNegativePart x) holds
b₁ is surreal-membered ; :: thesis:

end;

theorem Th9: :: SURREALS:9

for o being object holds
( L_ (NonNegativePart o) c= L_ o & R_ (NonNegativePart o) c= R_ o )

proof

let o be object ; :: thesis:
thus L_ (NonNegativePart o) c= L_ o :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in L_ (NonNegativePart o) ; :: thesis:
then ex l being Surreal st
( a = l & l in L_ o & 0_No <= l ) by Def5;
hence a in L_ o ; :: thesis:

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in R_ (NonNegativePart o) ; :: thesis:
then ex r being Surreal st
( a = r & r in R_ o & 0_No <= r ) by Def5;
hence a in R_ o ; :: thesis:

end;

registration

let x be Surreal;

cluster NonNegativePart x -> pair surreal ;

coherence

proof

set NN = NonNegativePart x;
consider M being Ordinal such that
A1: for o being object st o in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
L_ (NonNegativePart x) << R_ (NonNegativePart x)

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A2: ( l in L_ (NonNegativePart x) & r in R_ (NonNegativePart x) ) ; :: thesis:
A3: ( L_ (NonNegativePart x) c= L_ x & R_ (NonNegativePart x) c= R_ x ) by Th9;
L_ x << R_ x by SURREAL0:45;
hence not r <= l by A3, A2; :: thesis:

end;

then [(L_ (NonNegativePart x)),(R_ (NonNegativePart x))] in Day M by A1, SURREAL0:46;
hence NonNegativePart x is surreal ; :: thesis:

end;

theorem Th10: :: SURREALS:10

for o being object
for x being Surreal holds
( ( x in L_ (NonNegativePart o) implies ( x in L_ o & 0_No <= x ) ) & ( x in L_ o & 0_No <= x implies x in L_ (NonNegativePart o) ) & ( x in R_ (NonNegativePart o) implies ( x in R_ o & 0_No <= x ) ) & ( x in R_ o & 0_No <= x implies x in R_ (NonNegativePart o) ) )

proof

let o be object ; :: thesis:
let x be Surreal; :: thesis:
A1: ( x in L_ (NonNegativePart o) implies ( x in L_ o & 0_No <= x ) )

proof

assume x in L_ (NonNegativePart o) ; :: thesis:
then ex l being Surreal st
( x = l & l in L_ o & 0_No <= l ) by Def5;
hence ( x in L_ o & 0_No <= x ) ; :: thesis:

end;

( x in R_ (NonNegativePart o) implies ( x in R_ o & 0_No <= x ) )

proof

assume x in R_ (NonNegativePart o) ; :: thesis:
then ex l being Surreal st
( x = l & l in R_ o & 0_No <= l ) by Def5;
hence ( x in R_ o & 0_No <= x ) ; :: thesis:

end;

hence ( ( x in L_ (NonNegativePart o) implies ( x in L_ o & 0_No <= x ) ) & ( x in L_ o & 0_No <= x implies x in L_ (NonNegativePart o) ) & ( x in R_ (NonNegativePart o) implies ( x in R_ o & 0_No <= x ) ) & ( x in R_ o & 0_No <= x implies x in R_ (NonNegativePart o) ) ) by A1, Def5; :: thesis:

end;

theorem Th11: :: SURREALS:11

for x being Surreal holds born (NonNegativePart x) c= born x

proof

let x be Surreal; :: thesis:
set NN = NonNegativePart x;
for o being object st o in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) holds
ex O being Ordinal st
( O in born x & o in Day O )

proof

let o be object ; :: thesis:
assume A1: o in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) ; :: thesis:
reconsider o = o as Surreal by A1, SURREAL0:def 16;
( ( o in L_ (NonNegativePart x) & L_ (NonNegativePart x) c= L_ x ) or ( o in R_ (NonNegativePart x) & R_ (NonNegativePart x) c= R_ x ) ) by A1, Th9, XBOOLE_0:def 3;
then o in (L_ x) \/ (R_ x) by XBOOLE_0:def 3;
then ( born o in born x & o in Day (born o) ) by SURREALO:1, SURREAL0:def 18;
hence ex O being Ordinal st
( O in born x & o in Day O ) ; :: thesis:

end;

then [(L_ (NonNegativePart x)),(R_ (NonNegativePart x))] in Day (born x) by SURREAL0:45, SURREAL0:46;
hence born (NonNegativePart x) c= born x by SURREAL0:def 18; :: thesis:

end;

theorem Th12: :: SURREALS:12

for x being Surreal st 0_No <= x holds
0_No <= NonNegativePart x

proof

let x be Surreal; :: thesis:
set NN = NonNegativePart x;
assume A1: 0_No <= x ; :: thesis:
A2: L_ 0_No << {(NonNegativePart x)} ;
{0_No} << R_ (NonNegativePart x)

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A3: ( l in {0_No} & r in R_ (NonNegativePart x) ) ; :: thesis:
consider R being Surreal such that
A4: ( R = r & R in R_ x & 0_No <= R ) by A3, Def5;
( x in {x} & {x} << R_ x ) by TARSKI:def 1, SURREALO:11;
then 0_No < R by A4, A1, SURREALO:4;
hence l < r by A3, A4, TARSKI:def 1; :: thesis:

end;

hence 0_No <= NonNegativePart x by A2, SURREAL0:43; :: thesis:

end;

theorem :: SURREALS:13

for x being Surreal st 0_No <= x holds
NonNegativePart x == x

proof

let x be Surreal; :: thesis:
set NN = NonNegativePart x;
assume A1: 0_No <= x ; :: thesis:
then A2: 0_No <= NonNegativePart x by Th12;
A3: L_ (NonNegativePart x) << {x}

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A4: ( l in L_ (NonNegativePart x) & r in {x} ) ; :: thesis:
( L_ (NonNegativePart x) c= L_ x & L_ x << {x} ) by Th9, SURREALO:11;
hence not r <= l by A4; :: thesis:

end;

A5: {(NonNegativePart x)} << R_ x

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A6: ( l in {(NonNegativePart x)} & r in R_ x ) ; :: thesis:
( x in {x} & {x} << R_ x ) by TARSKI:def 1, SURREALO:11;
then 0_No <= r by A6, A1, SURREALO:4;
then A7: r in R_ (NonNegativePart x) by A6, Def5;
assume r <= l ; :: thesis:
then r <= NonNegativePart x by A6, TARSKI:def 1;
then ( r in {r} & {r} << R_ (NonNegativePart x) ) by TARSKI:def 1, SURREAL0:43;
hence contradiction by A7, SURREALO:3; :: thesis:

end;

A8: L_ x << {(NonNegativePart x)}

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A9: ( l in L_ x & r in {(NonNegativePart x)} ) ; :: thesis:
assume A10: r <= l ; :: thesis:
then NonNegativePart x <= l by A9, TARSKI:def 1;
then 0_No <= l by A2, SURREALO:4;
then A11: l in L_ (NonNegativePart x) by A9, Def5;
L_ (NonNegativePart x) << {(NonNegativePart x)} by SURREALO:11;
hence contradiction by A10, A9, A11; :: thesis:

end;

{x} << R_ (NonNegativePart x)

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A12: ( l in {x} & r in R_ (NonNegativePart x) ) ; :: thesis:
( R_ (NonNegativePart x) c= R_ x & {x} << R_ x ) by Th9, SURREALO:11;
hence not r <= l by A12; :: thesis:

end;

hence NonNegativePart x == x by A5, A8, A3, SURREAL0:43; :: thesis:

end;

definition

let A be Ordinal;

func No_sqrt_op A -> ManySortedSet of Day A means :Def6: :: SURREALS:def 6
ex S being c=-monotone Function-yielding Sequence st
( dom S = succ A & it = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [(Union (sqrtL ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x))),(Union (sqrtR ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x)))] ) ) ) );

existence

proof

deffunc H₁( Ordinal) -> Element of K10((Games $1)) = Day $1;
A1: for A, B being Ordinal st A c= B holds
H₁(A) c= H₁(B) by SURREAL0:35;
deffunc H₂( object , c=-monotone Function-yielding Sequence) -> object = [(Union (sqrtL ([((union (rng $2)) .: (L_ (NonNegativePart $1))),((union (rng $2)) .: (R_ (NonNegativePart $1)))],$1))),(Union (sqrtR ([((union (rng $2)) .: (L_ (NonNegativePart $1))),((union (rng $2)) .: (R_ (NonNegativePart $1)))],$1)))];
A2: for S being c=-monotone Function-yielding Sequence st ( for A being Ordinal st A in dom S holds
dom (S . A) = H₁(A) ) holds
for A being Ordinal
for o being object st o in dom (S . A) holds
H₂(o,S | A) = H₂(o,S)

proof

let S be c=-monotone Function-yielding Sequence; :: thesis:
assume A3: for A being Ordinal st A in dom S holds
dom (S . A) = H₁(A) ; :: thesis:
let A be Ordinal; :: thesis:
let o be object ; :: thesis:
assume A4: o in dom (S . A) ; :: thesis:
S . A <> {} by A4;
then A5: A in dom S by FUNCT_1:def 2;
then A6: dom (S . A) = H₁(A) by A3;
then reconsider x = o as Surreal by A4;
set Nx = NonNegativePart x;
A7: born x c= A by SURREAL0:def 18, A6, A4;
born (NonNegativePart x) c= born x by Th11;
then A8: born (NonNegativePart x) c= A by A7, XBOOLE_1:1;
A9: for a being object st a in L_ (NonNegativePart x) holds
ex B being Ordinal st
( a in dom (S . B) & B in A )

proof

let a be object ; :: thesis:
assume A10: a in L_ (NonNegativePart x) ; :: thesis:
reconsider a = a as Surreal by A10, SURREAL0:def 16;
set b = born a;
a in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by XBOOLE_0:def 3, A10;
then A11: born a in born (NonNegativePart x) by SURREALO:1;
A12: a in Day (born a) by SURREAL0:def 18;
dom (S . (born a)) = H₁( born a) by A3, A11, A8, A5, ORDINAL1:10;
hence ex B being Ordinal st
( a in dom (S . B) & B in A ) by A12, A11, A8; :: thesis:

end;

A13: for a being object st a in R_ (NonNegativePart x) holds
ex B being Ordinal st
( a in dom (S . B) & B in A )

proof

let a be object ; :: thesis:
assume A14: a in R_ (NonNegativePart x) ; :: thesis:
reconsider a = a as Surreal by A14, SURREAL0:def 16;
set b = born a;
a in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by XBOOLE_0:def 3, A14;
then A15: born a in born (NonNegativePart x) by SURREALO:1;
A16: a in Day (born a) by SURREAL0:def 18;
dom (S . (born a)) = H₁( born a) by A3, A15, A8, A5, ORDINAL1:10;
hence ex B being Ordinal st
( a in dom (S . B) & B in A ) by A15, A8, A16; :: thesis:

end;

A17: (union (rng S)) .: (L_ (NonNegativePart x)) = (union (rng (S | A))) .: (L_ (NonNegativePart x)) by A9, SURREALR:3;
(union (rng S)) .: (R_ (NonNegativePart x)) = (union (rng (S | A))) .: (R_ (NonNegativePart x)) by A13, SURREALR:3;
hence H₂(o,S | A) = H₂(o,S) by A17; :: thesis:

end;

consider S being c=-monotone Function-yielding Sequence such that
A18: dom S = succ A and
A19: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S . B = SB & ( for o being object st o in H₁(B) holds
SB . o = H₂(o,S | B) ) ) from SURREALR:sch 1(A2, A1);
consider SA being ManySortedSet of H₁(A) such that
A20: ( S . A = SA & ( for o being object st o in H₁(A) holds
SA . o = H₂(o,S | A) ) ) by A19, ORDINAL1:6;
take SA ; :: thesis:
take S ; :: thesis:
thus ( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [(Union (sqrtL ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x))),(Union (sqrtR ([((union (rng (S | B))) .: (L_ (NonNegativePart x))),((union (rng (S | B))) .: (R_ (NonNegativePart x)))],x)))] ) ) ) ) by A18, A20, A19; :: thesis:

end;

uniqueness

proof

let dA1, dA2 be ManySortedSet of Day A; :: thesis:
deffunc H₁( Ordinal) -> Element of K10((Games $1)) = Day $1;
deffunc H₂( object , c=-monotone Function-yielding Sequence) -> object = [(Union (sqrtL ([((union (rng $2)) .: (L_ (NonNegativePart $1))),((union (rng $2)) .: (R_ (NonNegativePart $1)))],$1))),(Union (sqrtR ([((union (rng $2)) .: (L_ (NonNegativePart $1))),((union (rng $2)) .: (R_ (NonNegativePart $1)))],$1)))];
given S1 being c=-monotone Function-yielding Sequence such that A21: ( dom S1 = succ A & dA1 = S1 . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S1 . B = SB & ( for x being object st x in Day B holds
SB . x = H₂(x,S1 | B) ) ) ) ) ; :: thesis:
given S2 being c=-monotone Function-yielding Sequence such that A22: ( dom S2 = succ A & dA2 = S2 . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S2 . B = SB & ( for x being object st x in Day B holds
SB . x = H₂(x,S2 | B) ) ) ) ) ; :: thesis:
A23: ( succ A c= dom S1 & succ A c= dom S2 ) by A21, A22;
A24: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S1 . B = SB & ( for o being object st o in H₁(B) holds
SB . o = H₂(o,S1 | B) ) ) by A21;
A25: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S2 . B = SB & ( for o being object st o in H₁(B) holds
SB . o = H₂(o,S2 | B) ) ) by A22;
S1 | (succ A) = S2 | (succ A) from SURREALR:sch 2(A23, A24, A25);
then S1 | (succ A) = S2 by A22;
hence dA1 = dA2 by A21, A22; :: thesis:

end;

:: deftheorem Def6 defines No_sqrt_op SURREALS:def 6 :

theorem Th14: :: SURREALS:14

for S being c=-monotone Function-yielding Sequence st ( for B being Ordinal st B in dom S holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for o being object st o in Day B holds
SB . o = [(Union (sqrtL ([((union (rng (S | B))) .: (L_ (NonNegativePart o))),((union (rng (S | B))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | B))) .: (L_ (NonNegativePart o))),((union (rng (S | B))) .: (R_ (NonNegativePart o)))],o)))] ) ) ) holds
for A being Ordinal st A in dom S holds
No_sqrt_op A = S . A

proof

deffunc H₁( Ordinal) -> Element of K10((Games $1)) = Day $1;
deffunc H₂( object , c=-monotone Function-yielding Sequence) -> object = [(Union (sqrtL ([((union (rng $2)) .: (L_ (NonNegativePart $1))),((union (rng $2)) .: (R_ (NonNegativePart $1)))],$1))),(Union (sqrtR ([((union (rng $2)) .: (L_ (NonNegativePart $1))),((union (rng $2)) .: (R_ (NonNegativePart $1)))],$1)))];
let S1 be c=-monotone Function-yielding Sequence; :: thesis:
assume A1: for B being Ordinal st B in dom S1 holds
ex SB being ManySortedSet of H₁(B) st
( S1 . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S1 | B) ) ) ; :: thesis:
let A be Ordinal; :: thesis:
assume A2: A in dom S1 ; :: thesis:
A3: succ A c= dom S1 by A2, ORDINAL1:21;
consider S2 being c=-monotone Function-yielding Sequence such that
A4: ( dom S2 = succ A & S2 . A = No_sqrt_op A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S2 . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S2 | B) ) ) ) ) by Def6;
A5: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S1 . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S1 | B) ) ) by A1, A3;
A6: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H₁(B) st
( S2 . B = SB & ( for x being object st x in H₁(B) holds
SB . x = H₂(x,S2 | B) ) ) by A4;
A7: ( succ A c= dom S1 & succ A c= dom S2 ) by A2, ORDINAL1:21, A4;
A8: S1 | (succ A) = S2 | (succ A) from SURREALR:sch 2(A7, A5, A6);
A in succ A by ORDINAL1:8;
hence No_sqrt_op A = S1 . A by A4, A8, FUNCT_1:49; :: thesis:

end;

definition

let o be object ;
assume A1: o is Surreal ;

func sqrt o -> set means :Def7: :: SURREALS:def 7
for x being Surreal st x = o holds
it = (No_sqrt_op (born x)) . x;

existence

proof

reconsider x = o as Surreal by A1;
take (No_sqrt_op (born x)) . x ; :: thesis:
thus for x being Surreal st x = o holds
(No_sqrt_op (born x)) . x = (No_sqrt_op (born x)) . x ; :: thesis:

end;

uniqueness

proof

let s1, s2 be set ; :: thesis:
assume that
A2: for x being Surreal st x = o holds
s1 = (No_sqrt_op (born x)) . x and
A3: for x being Surreal st x = o holds
s2 = (No_sqrt_op (born x)) . x ; :: thesis:
reconsider x = o as Surreal by A1;
s1 = (No_sqrt_op (born x)) . x by A2;
hence s1 = s2 by A3; :: thesis:

end;

:: deftheorem Def7 defines sqrt SURREALS:def 7 :

definition

let x be Surreal;

:: original: sqrt
redefine func sqrt x -> set equals :: SURREALS:def 8
(No_sqrt_op (born x)) . x;

coherence ;
compatibility by Def7;

end;

:: deftheorem defines sqrt SURREALS:def 8 :

definition

let x be object ;

func sqrt_0 x -> pair set means :Def9: :: SURREALS:def 9
for o being object holds
( ( o in L_ it implies ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) ) & ( ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) implies o in L_ it ) & ( o in R_ it implies ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) ) & ( ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) implies o in R_ it ) );

existence

proof

set NN = NonNegativePart x;
set L = { (sqrt l) where l is Element of L_ (NonNegativePart x) : l in L_ (NonNegativePart x) } ;
set R = { (sqrt r) where r is Element of R_ (NonNegativePart x) : r in R_ (NonNegativePart x) } ;
reconsider IT = [ { (sqrt l) where l is Element of L_ (NonNegativePart x) : l in L_ (NonNegativePart x) } , { (sqrt r) where r is Element of R_ (NonNegativePart x) : r in R_ (NonNegativePart x) } ] as pair set by TARSKI:1;
take IT ; :: thesis:
let o be object ; :: thesis:
thus ( o in L_ IT implies ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) ) :: thesis:

proof

assume o in L_ IT ; :: thesis:
then consider l being Element of L_ (NonNegativePart x) such that
A1: ( o = sqrt l & l in L_ (NonNegativePart x) ) ;
reconsider l = l as Surreal by A1, SURREAL0:def 16;
take l ; :: thesis:
thus ( o = sqrt l & l in L_ (NonNegativePart x) ) by A1; :: thesis:

end;

thus ( ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) implies o in L_ IT ) ; :: thesis:
thus ( o in R_ IT implies ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) ) :: thesis:

proof

assume o in R_ IT ; :: thesis:
then consider r being Element of R_ (NonNegativePart x) such that
A2: ( o = sqrt r & r in R_ (NonNegativePart x) ) ;
reconsider r = r as Surreal by A2, SURREAL0:def 16;
take r ; :: thesis:
thus ( o = sqrt r & r in R_ (NonNegativePart x) ) by A2; :: thesis:

end;

thus ( ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) implies o in R_ IT ) ; :: thesis:

end;

uniqueness

proof

set NN = NonNegativePart x;
let s1, s2 be pair set ; :: thesis:
assume that
A3: for o being object holds
( ( o in L_ s1 implies ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) ) & ( ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) implies o in L_ s1 ) & ( o in R_ s1 implies ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) ) & ( ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) implies o in R_ s1 ) ) and
A4: for o being object holds
( ( o in L_ s2 implies ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) ) & ( ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) implies o in L_ s2 ) & ( o in R_ s2 implies ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) ) & ( ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) implies o in R_ s2 ) ) ; :: thesis:

now :: thesis:

let o be object ; :: thesis:
( o in R_ s1 iff ex r being Surreal st
( o = sqrt r & r in R_ (NonNegativePart x) ) ) by A3;
hence ( o in R_ s1 iff o in R_ s2 ) by A4; :: thesis:

end;

then A5: R_ s1 = R_ s2 by TARSKI:2;

now :: thesis:

let o be object ; :: thesis:
( o in L_ s1 iff ex l being Surreal st
( o = sqrt l & l in L_ (NonNegativePart x) ) ) by A3;
hence ( o in L_ s1 iff o in L_ s2 ) by A4; :: thesis:

end;

then L_ s1 = L_ s2 by TARSKI:2;
hence s1 = s2 by A5, XTUPLE_0:2; :: thesis:

end;

:: deftheorem Def9 defines sqrt_0 SURREALS:def 9 :

theorem Th15: :: SURREALS:15

for x being Surreal holds sqrt x = [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))]

proof

let x be Surreal; :: thesis:
set A = born x;
set Nx = NonNegativePart x;
consider S being c=-monotone Function-yielding Sequence such that
A1: ( dom S = succ (born x) & No_sqrt_op (born x) = S . (born x) ) and
A2: for B being Ordinal st B in succ (born x) holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for o being object st o in Day B holds
SB . o = [(Union (sqrtL ([((union (rng (S | B))) .: (L_ (NonNegativePart o))),((union (rng (S | B))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | B))) .: (L_ (NonNegativePart o))),((union (rng (S | B))) .: (R_ (NonNegativePart o)))],o)))] ) ) by Def6;
set UA = union (rng (S | (born x)));
consider SB being ManySortedSet of Day (born x) such that
A3: S . (born x) = SB and
A4: for o being object st o in Day (born x) holds
SB . o = [(Union (sqrtL ([((union (rng (S | (born x)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born x)))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | (born x)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born x)))) .: (R_ (NonNegativePart o)))],o)))] by A2, ORDINAL1:6;
x in Day (born x) by SURREAL0:def 18;
then A5: sqrt x = [(Union (sqrtL ([((union (rng (S | (born x)))) .: (L_ (NonNegativePart x))),((union (rng (S | (born x)))) .: (R_ (NonNegativePart x)))],x))),(Union (sqrtR ([((union (rng (S | (born x)))) .: (L_ (NonNegativePart x))),((union (rng (S | (born x)))) .: (R_ (NonNegativePart x)))],x)))] by A4, A1, A3;
A6: (union (rng (S | (born x)))) .: (L_ (NonNegativePart x)) c= L_ (sqrt_0 x)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: y in (union (rng (S | (born x)))) .: (L_ (NonNegativePart x)) ; :: thesis:
consider o being object such that
A8: ( o in dom (union (rng (S | (born x)))) & o in L_ (NonNegativePart x) & (union (rng (S | (born x)))) . o = y ) by A7, FUNCT_1:def 6;
reconsider o = o as Surreal by SURREAL0:def 16, A8;
set b = born o;
A9: o in L_ x by Th10, A8;
A10: o in Day (born o) by SURREAL0:def 18;
A11: o in (L_ x) \/ (R_ x) by A9, XBOOLE_0:def 3;
then A12: born o in born x by SURREALO:1;
A13: born o in succ (born x) by A11, SURREALO:1, ORDINAL1:8;
then ex SB being ManySortedSet of Day (born o) st
( S . (born o) = SB & ( for o being object st o in Day (born o) holds
SB . o = [(Union (sqrtL ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o)))] ) ) by A2;
then A14: o in dom (S . (born o)) by A10, PARTFUN1:def 2;
then A15: (union (rng (S | (born x)))) . o = (union (rng S)) . o by A12, SURREALR:5;
A16: No_sqrt_op (born o) = S . (born o) by A1, A2, Th14, A13;
y = sqrt o by A8, A15, A13, A1, A14, SURREALR:2, A16;
hence y in L_ (sqrt_0 x) by Def9, A8; :: thesis:

end;

A17: L_ (sqrt_0 x) c= (union (rng (S | (born x)))) .: (L_ (NonNegativePart x))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in L_ (sqrt_0 x) ; :: thesis:
then consider o being Surreal such that
A18: ( y = sqrt o & o in L_ (NonNegativePart x) ) by Def9;
set b = born o;
A19: o in L_ x by Th10, A18;
A20: o in Day (born o) by SURREAL0:def 18;
A21: o in (L_ x) \/ (R_ x) by A19, XBOOLE_0:def 3;
then A22: born o in born x by SURREALO:1;
A23: born o in succ (born x) by SURREALO:1, A21, ORDINAL1:8;
then ex SB being ManySortedSet of Day (born o) st
( S . (born o) = SB & ( for o being object st o in Day (born o) holds
SB . o = [(Union (sqrtL ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o)))] ) ) by A2;
then A24: o in dom (S . (born o)) by A20, PARTFUN1:def 2;
then A25: (union (rng (S | (born x)))) . o = (union (rng S)) . o by A22, SURREALR:5;
A26: born o in dom S by SURREALO:1, A21, ORDINAL1:8, A1;
A27: No_sqrt_op (born o) = S . (born o) by A1, A2, Th14, A23;
A28: y = (union (rng S)) . o by A18, A24, A26, SURREALR:2, A27;
o in dom (union (rng (S | (born x)))) by SURREALR:5, A22, A24;
hence y in (union (rng (S | (born x)))) .: (L_ (NonNegativePart x)) by A18, A28, A25, FUNCT_1:def 6; :: thesis:

end;

A29: (union (rng (S | (born x)))) .: (R_ (NonNegativePart x)) c= R_ (sqrt_0 x)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A30: y in (union (rng (S | (born x)))) .: (R_ (NonNegativePart x)) ; :: thesis:
consider o being object such that
A31: ( o in dom (union (rng (S | (born x)))) & o in R_ (NonNegativePart x) & (union (rng (S | (born x)))) . o = y ) by A30, FUNCT_1:def 6;
reconsider o = o as Surreal by A31, SURREAL0:def 16;
set b = born o;
A32: o in R_ x by Th10, A31;
A33: o in Day (born o) by SURREAL0:def 18;
A34: o in (L_ x) \/ (R_ x) by A32, XBOOLE_0:def 3;
then A35: born o in born x by SURREALO:1;
A36: born o in succ (born x) by A34, SURREALO:1, ORDINAL1:8;
then ex SB being ManySortedSet of Day (born o) st
( S . (born o) = SB & ( for o being object st o in Day (born o) holds
SB . o = [(Union (sqrtL ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o)))] ) ) by A2;
then A37: o in dom (S . (born o)) by A33, PARTFUN1:def 2;
A38: born o in dom S by A34, SURREALO:1, ORDINAL1:8, A1;
A39: No_sqrt_op (born o) = S . (born o) by A1, A2, Th14, A36;
(S . (born o)) . o = (union (rng S)) . o by A37, A38, SURREALR:2;
then y = sqrt o by A39, A31, A37, A35, SURREALR:5;
hence y in R_ (sqrt_0 x) by Def9, A31; :: thesis:

end;

A40: R_ (sqrt_0 x) c= (union (rng (S | (born x)))) .: (R_ (NonNegativePart x))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in R_ (sqrt_0 x) ; :: thesis:
then consider o being Surreal such that
A41: ( y = sqrt o & o in R_ (NonNegativePart x) ) by Def9;
set b = born o;
A42: o in R_ x by Th10, A41;
A43: o in Day (born o) by SURREAL0:def 18;
A44: o in (L_ x) \/ (R_ x) by A42, XBOOLE_0:def 3;
then A45: born o in born x by SURREALO:1;
A46: born o in succ (born x) by A44, ORDINAL1:8, SURREALO:1;
then ex SB being ManySortedSet of Day (born o) st
( S . (born o) = SB & ( for o being object st o in Day (born o) holds
SB . o = [(Union (sqrtL ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o))),(Union (sqrtR ([((union (rng (S | (born o)))) .: (L_ (NonNegativePart o))),((union (rng (S | (born o)))) .: (R_ (NonNegativePart o)))],o)))] ) ) by A2;
then A47: o in dom (S . (born o)) by A43, PARTFUN1:def 2;
then A48: (union (rng (S | (born x)))) . o = (union (rng S)) . o by A45, SURREALR:5;
A49: born o in dom S by A44, ORDINAL1:8, SURREALO:1, A1;
A50: No_sqrt_op (born o) = S . (born o) by A1, A2, Th14, A46;
A51: y = (union (rng S)) . o by A41, A47, A49, SURREALR:2, A50;
o in dom (union (rng (S | (born x)))) by SURREALR:5, A45, A47;
hence y in (union (rng (S | (born x)))) .: (R_ (NonNegativePart x)) by A41, A51, A48, FUNCT_1:def 6; :: thesis:

end;

A52: (union (rng (S | (born x)))) .: (L_ (NonNegativePart x)) = L_ (sqrt_0 x) by A6, A17, XBOOLE_0:def 10;
(union (rng (S | (born x)))) .: (R_ (NonNegativePart x)) = R_ (sqrt_0 x) by A29, A40, XBOOLE_0:def 10;
hence sqrt x = [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))] by A5, A52; :: thesis:

end;

theorem :: SURREALS:16

for o being object
for p being pair object st Union (sqrtL (p,o)) = {} holds
L_ p = {}

proof

let o be object ; :: thesis:
let p be pair object ; :: thesis:
assume Union (sqrtL (p,o)) = {} ; :: thesis:
then (sqrtL (p,o)) . 0 c= {} by ABCMIZ_1:1;
hence L_ p = {} by Th1; :: thesis:

end;

theorem Th17: :: SURREALS:17

for x1, x2, y, z being Surreal st not x2 == 0_No & y = x1 * (x2 ") holds
( ( y * y < z implies x1 * x1 < z * (x2 * x2) ) & ( x1 * x1 < z * (x2 * x2) implies y * y < z ) & ( z < y * y implies z * (x2 * x2) < x1 * x1 ) & ( z * (x2 * x2) < x1 * x1 implies z < y * y ) )

proof

let x1, x2, y, z be Surreal; :: thesis:
assume A1: ( not x2 == 0_No & y = x1 * (x2 ") ) ; :: thesis:
x2 * (x2 ") == 1_No by A1, SURREALI:33;
then ( (x2 * (x2 ")) * (x2 * (x2 ")) == 1_No * (x2 * (x2 ")) & 1_No * (x2 * (x2 ")) == 1_No * 1_No & 1_No * 1_No = 1_No ) by SURREALR:54;
then A2: (x2 * (x2 ")) * (x2 * (x2 ")) == 1_No by SURREALO:4;
( ((x2 ") * (x2 ")) * (x2 * x2) == (x2 ") * ((x2 ") * (x2 * x2)) & (x2 ") * ((x2 ") * (x2 * x2)) == (x2 ") * (((x2 ") * x2) * x2) ) by SURREALR:54, SURREALR:69;
then ( ((x2 ") * (x2 ")) * (x2 * x2) == (x2 ") * (((x2 ") * x2) * x2) & (x2 ") * (((x2 ") * x2) * x2) == ((x2 ") * x2) * ((x2 ") * x2) ) by SURREALO:4, SURREALR:69;
then ((x2 ") * (x2 ")) * (x2 * x2) == ((x2 ") * x2) * ((x2 ") * x2) by SURREALO:4;
then A3: ((x2 ") * (x2 ")) * (x2 * x2) == 1_No by A2, SURREALO:4;
( y * y == x1 * ((x2 ") * ((x2 ") * x1)) & x1 * ((x2 ") * ((x2 ") * x1)) == x1 * (x1 * ((x2 ") * (x2 "))) ) by SURREALR:54, SURREALR:69, A1;
then ( y * y == x1 * (x1 * ((x2 ") * (x2 "))) & x1 * (x1 * ((x2 ") * (x2 "))) == (x1 * x1) * ((x2 ") * (x2 ")) ) by SURREALO:4, SURREALR:69;
then y * y == (x1 * x1) * ((x2 ") * (x2 ")) by SURREALO:4;
then ( (y * y) * (x2 * x2) == ((x1 * x1) * ((x2 ") * (x2 "))) * (x2 * x2) & ((x1 * x1) * ((x2 ") * (x2 "))) * (x2 * x2) == (x1 * x1) * (((x2 ") * (x2 ")) * (x2 * x2)) ) by SURREALR:54, SURREALR:69;
then ( (y * y) * (x2 * x2) == (x1 * x1) * (((x2 ") * (x2 ")) * (x2 * x2)) & (x1 * x1) * (((x2 ") * (x2 ")) * (x2 * x2)) == (x1 * x1) * 1_No & (x1 * x1) * 1_No = x1 * x1 ) by A3, SURREALO:4, SURREALR:54;
then A4: (y * y) * (x2 * x2) == x1 * x1 by SURREALO:4;
A5: 0_No < x2 * x2 by A1, SURREALR:72;
thus ( y * y < z implies x1 * x1 < z * (x2 * x2) ) :: thesis:

proof

assume y * y < z ; :: thesis:
then (y * y) * (x2 * x2) < z * (x2 * x2) by A5, SURREALR:70;
hence x1 * x1 < z * (x2 * x2) by A4, SURREALO:4; :: thesis:

end;

A6: 0_No <= x2 * x2 by A1, SURREALR:72;
thus ( x1 * x1 < z * (x2 * x2) implies y * y < z ) :: thesis:

proof

assume x1 * x1 < z * (x2 * x2) ; :: thesis:
then (y * y) * (x2 * x2) < z * (x2 * x2) by A4, SURREALO:4;
hence y * y < z by A6, SURREALR:75; :: thesis:

end;

thus ( z < y * y implies z * (x2 * x2) < x1 * x1 ) :: thesis:

proof

assume z < y * y ; :: thesis:
then z * (x2 * x2) < (y * y) * (x2 * x2) by A5, SURREALR:70;
hence z * (x2 * x2) < x1 * x1 by A4, SURREALO:4; :: thesis:

end;

assume z * (x2 * x2) < x1 * x1 ; :: thesis:
then z * (x2 * x2) < (y * y) * (x2 * x2) by A4, SURREALO:4;
hence z < y * y by A6, SURREALR:75; :: thesis:

end;

Lm1: for x, y, z being Surreal holds z * ((x + y) * (x + y)) == ((z * (x * x)) + (z * (y * y))) + ((z * (x * y)) + (z * (y * x)))

proof

let x, y, z be Surreal; :: thesis:
( z * ((x + y) * (x + y)) == z * (((x * x) + (y * y)) + ((x * y) + (y * x))) & z * (((x * x) + (y * y)) + ((x * y) + (y * x))) == (z * ((x * x) + (y * y))) + (z * ((x * y) + (y * x))) ) by SURREALR:67, SURREALR:54, SURREALR:76;
then A1: z * ((x + y) * (x + y)) == (z * ((x * x) + (y * y))) + (z * ((x * y) + (y * x))) by SURREALO:4;
( z * ((x * x) + (y * y)) == (z * (x * x)) + (z * (y * y)) & z * ((x * y) + (y * x)) == (z * (x * y)) + (z * (y * x)) ) by SURREALR:67;
then (z * ((x * x) + (y * y))) + (z * ((x * y) + (y * x))) == ((z * (x * x)) + (z * (y * y))) + ((z * (x * y)) + (z * (y * x))) by SURREALR:66;
hence z * ((x + y) * (x + y)) == ((z * (x * x)) + (z * (y * y))) + ((z * (x * y)) + (z * (y * x))) by A1, SURREALO:4; :: thesis:

end;

Lm2: for x, y, z being Surreal holds ((x * x) + ((y * z) * (y * z))) - ((x * (y * y)) + (x * (z * z))) == (x - (y * y)) * (x - (z * z))

proof

let x, y, z be Surreal; :: thesis:
( (y * z) * (y * z) == z * (y * (y * z)) & z * (y * (y * z)) == z * ((y * y) * z) ) by SURREALR:54, SURREALR:69;
then ( (y * z) * (y * z) == (z * (y * y)) * z & (z * (y * y)) * z == (z * z) * (y * y) ) by SURREALO:4, SURREALR:69;
then (y * z) * (y * z) == (z * z) * (y * y) by SURREALO:4;
then (x * x) + ((y * z) * (y * z)) == (x * x) + ((z * z) * (y * y)) by SURREALR:66;
then A1: ((x * x) + ((y * z) * (y * z))) - ((x * (y * y)) + (x * (z * z))) == ((x * x) + ((z * z) * (y * y))) - ((x * (y * y)) + (x * (z * z))) by SURREALR:66;
( x * (x - (z * z)) == (x * x) + (x * (- (z * z))) & (- (y * y)) * (x - (z * z)) == ((- (y * y)) * x) + ((- (y * y)) * (- (z * z))) ) by SURREALR:67;
then ( (x + (- (y * y))) * (x - (z * z)) == (x * (x - (z * z))) + ((- (y * y)) * (x - (z * z))) & (x * (x - (z * z))) + ((- (y * y)) * (x - (z * z))) == ((x * x) + (x * (- (z * z)))) + (((- (y * y)) * x) + ((- (y * y)) * (- (z * z)))) ) by SURREALR:67, SURREALR:66;
then A2: (x + (- (y * y))) * (x - (z * z)) == ((x * x) + (x * (- (z * z)))) + (((- (y * y)) * x) + ((- (y * y)) * (- (z * z)))) by SURREALO:4;
( (- (y * y)) * (- (z * z)) = (y * y) * (z * z) & x * (- (z * z)) = - (x * (z * z)) & (- (y * y)) * x = - (x * (y * y)) ) by SURREALR:58;
then ((x * x) + (x * (- (z * z)))) + (((- (y * y)) * x) + ((- (y * y)) * (- (z * z)))) = (((x * x) + (- (x * (z * z)))) + (- ((y * y) * x))) + ((y * y) * (z * z)) by SURREALR:37
.= ((x * x) + ((- (x * (z * z))) + (- ((y * y) * x)))) + ((y * y) * (z * z)) by SURREALR:37
.= ((x * x) + ((y * y) * (z * z))) + ((- (x * (z * z))) + (- ((y * y) * x))) by SURREALR:37
.= ((x * x) + ((y * y) * (z * z))) + (- ((x * (z * z)) + ((y * y) * x))) by SURREALR:40 ;
hence ((x * x) + ((y * z) * (y * z))) - ((x * (y * y)) + (x * (z * z))) == (x - (y * y)) * (x - (z * z)) by A2, A1, SURREALO:4; :: thesis:

end;

theorem Th18: :: SURREALS:18

for o being object
for x being Surreal st x <= 0_No holds
Union (sqrtL ((sqrt_0 x),o)) = {}

proof

let o be object ; :: thesis:
let x be Surreal; :: thesis:
assume A1: x <= 0_No ; :: thesis:
defpred S₁[ Nat] means (sqrtL ((sqrt_0 x),o)) . $1 = {} ;
A2: S₁[ 0 ]

proof

assume (sqrtL ((sqrt_0 x),o)) . 0 <> {} ; :: thesis:
then consider a being object such that
A3: a in (sqrtL ((sqrt_0 x),o)) . 0 by XBOOLE_0:def 1;
a in L_ (sqrt_0 x) by A3, Th1;
then consider l being Surreal such that
A4: ( a = sqrt l & l in L_ (NonNegativePart x) ) by Def9;
A5: ( l in L_ x & 0_No <= l ) by A4, Th10;
( L_ x << {x} & x in {x} ) by TARSKI:def 1, SURREALO:11;
hence contradiction by A5, A1, SURREALO:4; :: thesis:

end;

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

proof

let n be Nat; :: thesis:
assume A7: S₁[n] ; :: thesis:
assume (sqrtL ((sqrt_0 x),o)) . (n + 1) <> {} ; :: thesis:
then consider y being object such that
A8: y in (sqrtL ((sqrt_0 x),o)) . (n + 1) by XBOOLE_0:def 1;
y in ((sqrtL ((sqrt_0 x),o)) . n) \/ (sqrt (o,((sqrtL ((sqrt_0 x),o)) . n),((sqrtR ((sqrt_0 x),o)) . n))) by A8, Th3;

per cases by XBOOLE_0:def 3;

suppose y in (sqrtL ((sqrt_0 x),o)) . n ; :: thesis:

hence contradiction by A7; :: thesis:

end;

suppose y in sqrt (o,((sqrtL ((sqrt_0 x),o)) . n),((sqrtR ((sqrt_0 x),o)) . n)) ; :: thesis:

then ex x1, y1 being Surreal st
( x1 in (sqrtL ((sqrt_0 x),o)) . n & y1 in (sqrtR ((sqrt_0 x),o)) . n & not x1 + y1 == 0_No & y = (o +' (x1 * y1)) * ((x1 + y1) ") ) by Def1;
hence contradiction by A7; :: thesis:

end;

A9: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A6);
assume Union (sqrtL ((sqrt_0 x),o)) <> {} ; :: thesis:
then consider a being object such that
A10: a in Union (sqrtL ((sqrt_0 x),o)) by XBOOLE_0:def 1;
consider n being object such that
A11: ( n in dom (sqrtL ((sqrt_0 x),o)) & a in (sqrtL ((sqrt_0 x),o)) . n ) by A10, CARD_5:2;
dom (sqrtL ((sqrt_0 x),o)) = NAT by Def3;
then reconsider n = n as Nat by A11;
(sqrtL ((sqrt_0 x),o)) . n = {} by A9;
hence contradiction by A11; :: thesis:

end;

theorem Th19: :: SURREALS:19

for x, y being Surreal st 0_No <= x holds
( ( y = sqrt x implies ( 0_No <= y & y * y == x & ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) ) & ( y in L_ (sqrt x) implies ( 0_No <= y & y * y < x ) ) & ( y in R_ (sqrt x) implies ( 0_No < y & x < y * y ) ) & sqrt x is surreal )

proof

let x, y be Surreal; :: thesis:
defpred S₁[ Ordinal] means for x being Surreal st born x = $1 & 0_No <= x holds
( sqrt x is surreal & ( for y being Surreal st y = sqrt x holds
( 0_No <= y & y * y == x & ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) ) & ( for y being Surreal st y in L_ (sqrt x) holds
( 0_No <= y & y * y < x ) ) & ( for y being Surreal st y in R_ (sqrt x) holds
( 0_No < y & x < y * y ) ) );
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis:
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
let x be Surreal; :: thesis:
assume A3: ( born x = D & 0_No <= x ) ; :: thesis:
set S = sqrt x;
set S0 = sqrt_0 x;
A4: sqrt x = [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))] by Th15;
defpred S₂[ Nat] means ( ( for y being Surreal st y in (sqrtL ((sqrt_0 x),x)) . $1 holds
( 0_No <= y & y * y < x ) ) & ( for y being Surreal st y in (sqrtR ((sqrt_0 x),x)) . $1 holds
( 0_No < y & x < y * y ) ) );
set Nx = NonNegativePart x;
A5: S₂[ 0 ]

proof

thus for y being Surreal st y in (sqrtL ((sqrt_0 x),x)) . 0 holds
( 0_No <= y & y * y < x ) :: thesis:

proof

let y be Surreal; :: thesis:
assume A6: y in (sqrtL ((sqrt_0 x),x)) . 0 ; :: thesis:
y in L_ (sqrt_0 x) by A6, Th1;
then consider l being Surreal such that
A7: ( y = sqrt l & l in L_ (NonNegativePart x) ) by Def9;
A8: ( l in L_ x & 0_No <= l ) by Th10, A7;
A9: ( L_ x << {x} & x in {x} ) by SURREALO:11, TARSKI:def 1;
l in (L_ x) \/ (R_ x) by A8, XBOOLE_0:def 3;
then born l in D by A3, SURREALO:1;
then ( 0_No <= y & y * y == l ) by A2, A8, A7;
hence ( 0_No <= y & y * y < x ) by A9, A8, SURREALO:4; :: thesis:

end;

let y be Surreal; :: thesis:
assume A10: y in (sqrtR ((sqrt_0 x),x)) . 0 ; :: thesis:
y in R_ (sqrt_0 x) by A10, Th1;
then consider r being Surreal such that
A11: ( y = sqrt r & r in R_ (NonNegativePart x) ) by Def9;
A12: ( r in R_ x & 0_No <= r ) by A11, Th10;
then r in (L_ x) \/ (R_ x) by XBOOLE_0:def 3;
then A13: born r in D by A3, SURREALO:1;
then A14: ( 0_No <= y & y * y == r ) by A2, A11, A12;
A15: ( x in {x} & {x} << R_ x ) by SURREALO:11, TARSKI:def 1;
then 0_No < r by A3, A12, SURREALO:4;
hence ( 0_No < y & x < y * y ) by A15, A12, A13, A2, A11, A14, SURREALO:4; :: thesis:

end;

A16: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
assume A17: S₂[n] ; :: thesis:
thus for y being Surreal st y in (sqrtL ((sqrt_0 x),x)) . (n + 1) holds
( 0_No <= y & y * y < x ) :: thesis:

proof

let y be Surreal; :: thesis:
assume A18: y in (sqrtL ((sqrt_0 x),x)) . (n + 1) ; :: thesis:
y in ((sqrtL ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n))) by A18, Th3;

per cases by XBOOLE_0:def 3;

suppose y in (sqrtL ((sqrt_0 x),x)) . n ; :: thesis:

hence ( 0_No <= y & y * y < x ) by A17; :: thesis:

end;

suppose y in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ; :: thesis:

then consider L1, R1 being Surreal such that
A19: ( L1 in (sqrtL ((sqrt_0 x),x)) . n & R1 in (sqrtR ((sqrt_0 x),x)) . n & not L1 + R1 == 0_No & y = (x +' (L1 * R1)) * ((L1 + R1) ") ) by Def1;
A20: ( 0_No <= L1 & 0_No <= R1 ) by A19, A17;
then 0_No + 0_No <= L1 + R1 by SURREALR:43;
then A21: 0_No <= (L1 + R1) " by A19, SURREALI:40;
0_No * R1 <= L1 * R1 by A20, SURREALR:75;
then 0_No + 0_No <= x + (L1 * R1) by A3, SURREALR:43;
then A22: 0_No * ((L1 + R1) ") <= (x +' (L1 * R1)) * ((L1 + R1) ") by A21, SURREALR:75;
( L1 * L1 < x & x < R1 * R1 ) by A19, A17;
then ( 0_No < x - (L1 * L1) & x - (R1 * R1) < 0_No ) by SURREALR:45, SURREALR:46;
then A23: (x - (L1 * L1)) * (x - (R1 * R1)) < 0_No by SURREALR:74;
((x * x) + ((L1 * R1) * (L1 * R1))) - ((x * (L1 * L1)) + (x * (R1 * R1))) == (x - (L1 * L1)) * (x - (R1 * R1)) by Lm2;
then ((x * x) + ((L1 * R1) * (L1 * R1))) - ((x * (L1 * L1)) + (x * (R1 * R1))) < 0_No by A23, SURREALO:4;
then A24: (x * x) + ((L1 * R1) * (L1 * R1)) < (x * (L1 * L1)) + (x * (R1 * R1)) by SURREALR:46;
A25: x * ((L1 + R1) * (L1 + R1)) == ((x * (L1 * L1)) + (x * (R1 * R1))) + ((x * (L1 * R1)) + (x * (R1 * L1))) by Lm1;
A26: (x + (L1 * R1)) * (x + (L1 * R1)) == ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) by SURREALR:76;
((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) < ((x * (L1 * L1)) + (x * (R1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) by A24, SURREALR:44;
then ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + (x * (L1 * R1))) < x * ((L1 + R1) * (L1 + R1)) by A25, SURREALO:4;
then (x + (L1 * R1)) * (x + (L1 * R1)) < x * ((L1 + R1) * (L1 + R1)) by A26, SURREALO:4;
hence ( 0_No <= y & y * y < x ) by A22, A19, Th17; :: thesis:

end;

let y be Surreal; :: thesis:
assume A27: y in (sqrtR ((sqrt_0 x),x)) . (n + 1) ; :: thesis:
y in (((sqrtR ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)))) \/ (sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n))) by A27, Th3;
then ( y in ((sqrtR ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n))) or y in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ) by XBOOLE_0:def 3;

per cases by XBOOLE_0:def 3;

suppose y in (sqrtR ((sqrt_0 x),x)) . n ; :: thesis:

hence ( 0_No < y & x < y * y ) by A17; :: thesis:

end;

suppose y in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)) ; :: thesis:

then consider L1, R1 being Surreal such that
A28: ( L1 in (sqrtL ((sqrt_0 x),x)) . n & R1 in (sqrtL ((sqrt_0 x),x)) . n & not L1 + R1 == 0_No & y = (x +' (L1 * R1)) * ((L1 + R1) ") ) by Def1;
A29: ( 0_No <= L1 & 0_No <= R1 ) by A28, A17;
then 0_No + 0_No <= L1 + R1 by SURREALR:43;
then A30: 0_No < (L1 + R1) " by A28, SURREALI:40;
A31: (sqrtL ((sqrt_0 x),x)) . n c= Union (sqrtL ((sqrt_0 x),x)) by ABCMIZ_1:1;
0_No * R1 <= L1 * R1 by A29, SURREALR:75;
then A32: 0_No + 0_No < x + (L1 * R1) by A31, Th18, A28, SURREALR:44;
( 0_No < x - (L1 * L1) & 0_No < x - (R1 * R1) ) by A28, A17, SURREALR:45;
then A33: 0_No < (x - (L1 * L1)) * (x - (R1 * R1)) by SURREALR:72;
((x * x) + ((L1 * R1) * (L1 * R1))) - ((x * (L1 * L1)) + (x * (R1 * R1))) == (x - (L1 * L1)) * (x - (R1 * R1)) by Lm2;
then 0_No < ((x * x) + ((L1 * R1) * (L1 * R1))) - ((x * (L1 * L1)) + (x * (R1 * R1))) by A33, SURREALO:4;
then A34: (x * (L1 * L1)) + (x * (R1 * R1)) < (x * x) + ((L1 * R1) * (L1 * R1)) by SURREALR:45;
A35: x * ((L1 + R1) * (L1 + R1)) == ((x * (L1 * L1)) + (x * (R1 * R1))) + ((x * (L1 * R1)) + (x * (R1 * L1))) by Lm1;
A36: (x + (L1 * R1)) * (x + (L1 * R1)) == ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) by SURREALR:76;
((x * (L1 * L1)) + (x * (R1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) < ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) by A34, SURREALR:44;
then x * ((L1 + R1) * (L1 + R1)) < ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + (x * (L1 * R1))) by A35, SURREALO:4;
then x * ((L1 + R1) * (L1 + R1)) < (x + (L1 * R1)) * (x + (L1 * R1)) by A36, SURREALO:4;
hence ( 0_No < y & x < y * y ) by A32, A28, Th17, A30, SURREALR:72; :: thesis:

end;

suppose y in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ; :: thesis:

then consider L1, R1 being Surreal such that
A37: ( L1 in (sqrtR ((sqrt_0 x),x)) . n & R1 in (sqrtR ((sqrt_0 x),x)) . n & not L1 + R1 == 0_No & y = (x +' (L1 * R1)) * ((L1 + R1) ") ) by Def1;
A38: ( 0_No < L1 & 0_No < R1 ) by A37, A17;
( 0_No < L1 & 0_No <= R1 ) by A37, A17;
then 0_No + 0_No < L1 + R1 by SURREALR:44;
then A39: 0_No < (L1 + R1) " by A37, SURREALI:40;
0_No < L1 * R1 by A38, SURREALR:72;
then A40: 0_No + 0_No < x + (L1 * R1) by A3, SURREALR:44;
( x < L1 * L1 & x < R1 * R1 ) by A37, A17;
then ( x - (L1 * L1) < 0_No & x - (R1 * R1) < 0_No ) by SURREALR:46;
then A41: 0_No < (x - (L1 * L1)) * (x - (R1 * R1)) by SURREALR:72;
((x * x) + ((L1 * R1) * (L1 * R1))) - ((x * (L1 * L1)) + (x * (R1 * R1))) == (x - (L1 * L1)) * (x - (R1 * R1)) by Lm2;
then 0_No < ((x * x) + ((L1 * R1) * (L1 * R1))) - ((x * (L1 * L1)) + (x * (R1 * R1))) by A41, SURREALO:4;
then A42: (x * (L1 * L1)) + (x * (R1 * R1)) < (x * x) + ((L1 * R1) * (L1 * R1)) by SURREALR:45;
A43: x * ((L1 + R1) * (L1 + R1)) == ((x * (L1 * L1)) + (x * (R1 * R1))) + ((x * (L1 * R1)) + (x * (R1 * L1))) by Lm1;
A44: (x + (L1 * R1)) * (x + (L1 * R1)) == ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) by SURREALR:76;
((x * (L1 * L1)) + (x * (R1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) < ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + ((L1 * R1) * x)) by A42, SURREALR:44;
then x * ((L1 + R1) * (L1 + R1)) < ((x * x) + ((L1 * R1) * (L1 * R1))) + ((x * (L1 * R1)) + (x * (L1 * R1))) by A43, SURREALO:4;
then x * ((L1 + R1) * (L1 + R1)) < (x + (L1 * R1)) * (x + (L1 * R1)) by A44, SURREALO:4;
hence ( 0_No < y & x < y * y ) by A40, A37, A39, SURREALR:72, Th17; :: thesis:

end;

A45: for n being Nat holds S₂[n] from NAT_1:sch 2(A5, A16);
A46: for y being Surreal st y in L_ (sqrt x) holds
( 0_No <= y & y * y < x )

proof

let y be Surreal; :: thesis:
assume y in L_ (sqrt x) ; :: thesis:
then consider n being object such that
A47: ( n in dom (sqrtL ((sqrt_0 x),x)) & y in (sqrtL ((sqrt_0 x),x)) . n ) by A4, CARD_5:2;
dom (sqrtL ((sqrt_0 x),x)) = NAT by Def3;
then reconsider n = n as Nat by A47;
S₂[n] by A45;
hence ( 0_No <= y & y * y < x ) by A47; :: thesis:

end;

A48: for y being Surreal st y in R_ (sqrt x) holds
( 0_No < y & x < y * y )

proof

let y be Surreal; :: thesis:
assume y in R_ (sqrt x) ; :: thesis:
then consider n being object such that
A49: ( n in dom (sqrtR ((sqrt_0 x),x)) & y in (sqrtR ((sqrt_0 x),x)) . n ) by A4, CARD_5:2;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def4;
then reconsider n = n as Nat by A49;
S₂[n] by A45;
hence ( 0_No < y & x < y * y ) by A49; :: thesis:

end;

A50: L_ (sqrt_0 x) is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis:
assume o in L_ (sqrt_0 x) ; :: thesis:
then consider l being Surreal such that
A51: ( o = sqrt l & l in L_ (NonNegativePart x) ) by Def9;
A52: ( l in L_ x & 0_No <= l ) by Th10, A51;
then l in (L_ x) \/ (R_ x) by XBOOLE_0:def 3;
then born l in D by A3, SURREALO:1;
hence o is surreal by A51, A52, A2; :: thesis:

end;

R_ (sqrt_0 x) is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis:
assume o in R_ (sqrt_0 x) ; :: thesis:
then consider r being Surreal such that
A53: ( o = sqrt r & r in R_ (NonNegativePart x) ) by Def9;
A54: ( r in R_ x & 0_No <= r ) by Th10, A53;
then r in (L_ x) \/ (R_ x) by XBOOLE_0:def 3;
then born r in D by A3, SURREALO:1;
hence o is surreal by A53, A54, A2; :: thesis:

end;

then ( Union (sqrtL ((sqrt_0 x),x)) is surreal-membered & Union (sqrtR ((sqrt_0 x),x)) is surreal-membered ) by A50, Th5;
then consider M being Ordinal such that
A55: for o being object st o in (Union (sqrtL ((sqrt_0 x),x))) \/ (Union (sqrtR ((sqrt_0 x),x))) holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
Union (sqrtL ((sqrt_0 x),x)) << Union (sqrtR ((sqrt_0 x),x))

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A56: ( l in Union (sqrtL ((sqrt_0 x),x)) & r in Union (sqrtR ((sqrt_0 x),x)) & r <= l ) ; :: thesis:
consider n being object such that
A57: ( n in dom (sqrtL ((sqrt_0 x),x)) & l in (sqrtL ((sqrt_0 x),x)) . n ) by A56, CARD_5:2;
consider k being object such that
A58: ( k in dom (sqrtR ((sqrt_0 x),x)) & r in (sqrtR ((sqrt_0 x),x)) . k ) by A56, CARD_5:2;
( dom (sqrtL ((sqrt_0 x),x)) = NAT & NAT = dom (sqrtR ((sqrt_0 x),x)) ) by Def3, Def4;
then reconsider n = n, k = k as Nat by A57, A58;
A59: ( S₂[n] & S₂[k] ) by A45;
then A60: ( 0_No <= l & l * l < x & 0_No <= r & x < r * r ) by A57, A58;
then ( r * r <= r * l & r * l <= l * l ) by A56, SURREALR:75;
then r * r <= l * l by SURREALO:4;
then x <= l * l by A60, SURREALO:4;
hence contradiction by A57, A59; :: thesis:

end;

then [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))] in Day M by A55, SURREAL0:46;
then reconsider S = sqrt x as Surreal by Th15;
A61: for y being Surreal st y = sqrt x holds
( 0_No <= y & y * y == x )

proof

let y be Surreal; :: thesis:
assume A62: y = sqrt x ; :: thesis:
A63: L_ 0_No << {y} ;
{0_No} << R_ y

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A64: ( l in {0_No} & r in R_ y ) ; :: thesis:
consider n being object such that
A65: ( n in dom (sqrtR ((sqrt_0 x),x)) & r in (sqrtR ((sqrt_0 x),x)) . n ) by CARD_5:2, A4, A62, A64;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def4;
then reconsider n = n as Nat by A65;
r in (sqrtR ((sqrt_0 x),x)) . n by A65;
then 0_No < r by A45;
hence not r <= l by A64, TARSKI:def 1; :: thesis:

end;

hence A66: 0_No <= y by A63, SURREAL0:43; :: thesis:
A67: y * y = [((comp ((L_ y),y,y,(L_ y))) \/ (comp ((R_ y),y,y,(R_ y)))),((comp ((L_ y),y,y,(R_ y))) \/ (comp ((R_ y),y,y,(L_ y))))] by SURREALR:50;
A68: L_ (y * y) << {x}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A69: ( a in L_ (y * y) & b in {x} ) ; :: thesis:

per cases by XBOOLE_0:def 3, A67, A69;

suppose a in comp ((L_ y),y,y,(L_ y)) ; :: thesis:

then consider x1, y1 being Surreal such that
A70: ( a = ((x1 * y) + (y * y1)) - (x1 * y1) & x1 in L_ y & y1 in L_ y ) by SURREALR:def 15;
consider n being object such that
A71: ( n in dom (sqrtL ((sqrt_0 x),x)) & x1 in (sqrtL ((sqrt_0 x),x)) . n ) by A70, A4, A62, CARD_5:2;
dom (sqrtL ((sqrt_0 x),x)) = NAT by Def3;
then reconsider n = n as Nat by A71;
consider m being object such that
A72: ( m in dom (sqrtL ((sqrt_0 x),x)) & y1 in (sqrtL ((sqrt_0 x),x)) . m ) by A70, A4, A62, CARD_5:2;
dom (sqrtL ((sqrt_0 x),x)) = NAT by Def3;
then reconsider n = n, m = m as Nat by A72;
set nm = n + m;
A73: ( n <= n + m & m <= n + m ) by NAT_1:11;
then A74: ( (sqrtL ((sqrt_0 x),x)) . n c= (sqrtL ((sqrt_0 x),x)) . (n + m) & (sqrtL ((sqrt_0 x),x)) . m c= (sqrtL ((sqrt_0 x),x)) . (n + m) ) by Th2;
A75: (sqrtL ((sqrt_0 x),x)) . n c= Union (sqrtL ((sqrt_0 x),x)) by ABCMIZ_1:1;
set X = x + (x1 * y1);
A76: ( 0_No <= x1 & 0_No <= y1 ) by A73, A71, A72, A45;

per cases ;

suppose ( x1 == 0_No & y1 == 0_No ) ; :: thesis:

then ( x1 * y == 0_No * y & y * y1 == y * 0_No & x1 * y1 == 0_No * x1 ) by SURREALR:54;
then ( (x1 * y) + (y * y1) == 0_No + 0_No & - (x1 * y1) == - 0_No ) by SURREALR:65, SURREALR:66;
then a == 0_No + 0_No by A70, SURREALR:66;
then a < x by A75, A71, Th18, SURREALO:4;
hence not b <= a by A69, TARSKI:def 1; :: thesis:

end;

suppose A77: ( not x1 == 0_No or not y1 == 0_No ) ; :: thesis:

then 0_No + 0_No < x1 + y1 by A76, SURREALR:44;
then A78: not x1 + y1 == 0_No ;
then (x + (x1 * y1)) * ((x1 + y1) ") in sqrt (x,((sqrtL ((sqrt_0 x),x)) . (n + m)),((sqrtL ((sqrt_0 x),x)) . (n + m))) by A74, A71, A72, Def1;
then (x + (x1 * y1)) * ((x1 + y1) ") in ((sqrtR ((sqrt_0 x),x)) . (n + m)) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . (n + m)),((sqrtL ((sqrt_0 x),x)) . (n + m)))) by XBOOLE_0:def 3;
then (x + (x1 * y1)) * ((x1 + y1) ") in (((sqrtR ((sqrt_0 x),x)) . (n + m)) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . (n + m)),((sqrtL ((sqrt_0 x),x)) . (n + m))))) \/ (sqrt (x,((sqrtR ((sqrt_0 x),x)) . (n + m)),((sqrtR ((sqrt_0 x),x)) . (n + m)))) by XBOOLE_0:def 3;
then A79: ( (x + (x1 * y1)) * ((x1 + y1) ") in (sqrtR ((sqrt_0 x),x)) . ((n + m) + 1) & (sqrtR ((sqrt_0 x),x)) . ((n + m) + 1) c= Union (sqrtR ((sqrt_0 x),x)) ) by Th3, ABCMIZ_1:1;
A80: ( y in {y} & {y} << R_ y ) by TARSKI:def 1, SURREALO:11;
then A81: y < (x + (x1 * y1)) * ((x1 + y1) ") by A79, A62, A4;
A82: y <= (x + (x1 * y1)) * ((x1 + y1) ") by A80, A79, A62, A4;
A83: (x1 + y1) * ((x1 + y1) ") == 1_No by A78, SURREALI:33;
A84: (x1 * y) + (y * y1) < (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) ")))

proof

per cases by A73, A71, A72, A45, A77;

suppose 0_No < x1 ; :: thesis:

then ( x1 * y < x1 * ((x + (x1 * y1)) * ((x1 + y1) ")) & y1 * y <= y1 * ((x + (x1 * y1)) * ((x1 + y1) ")) ) by A76, A81, A82, SURREALR:70, SURREALR:75;
hence (x1 * y) + (y * y1) < (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) by SURREALR:44; :: thesis:

end;

suppose 0_No < y1 ; :: thesis:

then ( x1 * y <= x1 * ((x + (x1 * y1)) * ((x1 + y1) ")) & y1 * y < y1 * ((x + (x1 * y1)) * ((x1 + y1) ")) ) by A76, A81, A82, SURREALR:70, SURREALR:75;
hence (x1 * y) + (y * y1) < (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) by SURREALR:44; :: thesis:

end;

( (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == (x1 + y1) * ((x + (x1 * y1)) * ((x1 + y1) ")) & (x1 + y1) * ((x + (x1 * y1)) * ((x1 + y1) ")) == ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) ) by SURREALR:67, SURREALR:69;
then ( (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) & ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) == 1_No * (x + (x1 * y1)) ) by A83, SURREALR:54, SURREALO:4;
then (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == 1_No * (x + (x1 * y1)) by SURREALO:4;
then (x1 * y) + (y * y1) < x + (x1 * y1) by A84, SURREALO:4;
then A85: ((x1 * y) + (y * y1)) + (- (x1 * y1)) < (x + (x1 * y1)) + (- (x1 * y1)) by SURREALR:44;
(x1 * y1) - (x1 * y1) == 0_No by SURREALR:39;
then ( (x + (x1 * y1)) + (- (x1 * y1)) = x + ((x1 * y1) + (- (x1 * y1))) & x + ((x1 * y1) + (- (x1 * y1))) == x + 0_No ) by SURREALR:37, SURREALR:66;
then a < x by A70, A85, SURREALO:4;
hence not b <= a by A69, TARSKI:def 1; :: thesis:

end;

suppose a in comp ((R_ y),y,y,(R_ y)) ; :: thesis:

then consider x1, y1 being Surreal such that
A86: ( a = ((x1 * y) + (y * y1)) - (x1 * y1) & x1 in R_ y & y1 in R_ y ) by SURREALR:def 15;
consider n being object such that
A87: ( n in dom (sqrtR ((sqrt_0 x),x)) & x1 in (sqrtR ((sqrt_0 x),x)) . n ) by A86, A4, A62, CARD_5:2;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def4;
then reconsider n = n as Nat by A87;
consider m being object such that
A88: ( m in dom (sqrtR ((sqrt_0 x),x)) & y1 in (sqrtR ((sqrt_0 x),x)) . m ) by A86, A4, A62, CARD_5:2;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def4;
then reconsider n = n, m = m as Nat by A88;
set nm = n + m;
A89: ( n <= n + m & m <= n + m ) by NAT_1:11;
then A90: ( (sqrtR ((sqrt_0 x),x)) . n c= (sqrtR ((sqrt_0 x),x)) . (n + m) & (sqrtR ((sqrt_0 x),x)) . m c= (sqrtR ((sqrt_0 x),x)) . (n + m) ) by Th2;
set X = x + (x1 * y1);
A91: ( 0_No < x1 & 0_No <= y1 ) by A89, A87, A88, A45;
then 0_No + 0_No < x1 + y1 by SURREALR:44;
then A92: not x1 + y1 == 0_No ;
then (x + (x1 * y1)) * ((x1 + y1) ") in sqrt (x,((sqrtR ((sqrt_0 x),x)) . (n + m)),((sqrtR ((sqrt_0 x),x)) . (n + m))) by A87, A88, A90, Def1;
then (x + (x1 * y1)) * ((x1 + y1) ") in (((sqrtR ((sqrt_0 x),x)) . (n + m)) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . (n + m)),((sqrtL ((sqrt_0 x),x)) . (n + m))))) \/ (sqrt (x,((sqrtR ((sqrt_0 x),x)) . (n + m)),((sqrtR ((sqrt_0 x),x)) . (n + m)))) by XBOOLE_0:def 3;
then A93: ( (x + (x1 * y1)) * ((x1 + y1) ") in (sqrtR ((sqrt_0 x),x)) . ((n + m) + 1) & (sqrtR ((sqrt_0 x),x)) . ((n + m) + 1) c= Union (sqrtR ((sqrt_0 x),x)) ) by Th3, ABCMIZ_1:1;
A94: ( y in {y} & {y} << R_ y ) by TARSKI:def 1, SURREALO:11;
then A95: y < (x + (x1 * y1)) * ((x1 + y1) ") by A93, A62, A4;
A96: y <= (x + (x1 * y1)) * ((x1 + y1) ") by A93, A94, A62, A4;
A97: (x1 + y1) * ((x1 + y1) ") == 1_No by A92, SURREALI:33;
( x1 * y < x1 * ((x + (x1 * y1)) * ((x1 + y1) ")) & y1 * y <= y1 * ((x + (x1 * y1)) * ((x1 + y1) ")) ) by A91, A95, A96, SURREALR:70, SURREALR:75;
then A98: (x1 * y) + (y * y1) < (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) by SURREALR:44;
( (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == (x1 + y1) * ((x + (x1 * y1)) * ((x1 + y1) ")) & (x1 + y1) * ((x + (x1 * y1)) * ((x1 + y1) ")) == ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) ) by SURREALR:67, SURREALR:69;
then ( (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) & ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) == 1_No * (x + (x1 * y1)) ) by A97, SURREALR:54, SURREALO:4;
then (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == 1_No * (x + (x1 * y1)) by SURREALO:4;
then (x1 * y) + (y * y1) < x + (x1 * y1) by A98, SURREALO:4;
then A99: ((x1 * y) + (y * y1)) + (- (x1 * y1)) < (x + (x1 * y1)) + (- (x1 * y1)) by SURREALR:44;
(x1 * y1) - (x1 * y1) == 0_No by SURREALR:39;
then ( (x + (x1 * y1)) + (- (x1 * y1)) = x + ((x1 * y1) + (- (x1 * y1))) & x + ((x1 * y1) + (- (x1 * y1))) == x + 0_No ) by SURREALR:37, SURREALR:66;
then a < x by A86, A99, SURREALO:4;
hence not b <= a by A69, TARSKI:def 1; :: thesis:

end;

A100: {(y * y)} << R_ x

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A101: ( a in {(y * y)} & b in R_ x ) ; :: thesis:
A102: ( x in {x} & {x} << R_ x ) by TARSKI:def 1, SURREALO:11;
then A103: 0_No < b by A101, A3, SURREALO:4;
A104: 0_No <= b by A102, A101, A3, SURREALO:4;
b in (L_ x) \/ (R_ x) by A101, XBOOLE_0:def 3;
then A105: born b in born x by SURREALO:1;
then reconsider sb = sqrt b as Surreal by A104, A2, A3;
A106: ( 0_No < sb & sb * sb == b ) by A103, A104, A105, A2, A3;
b in R_ (NonNegativePart x) by A101, A104, Def5;
then A107: ( sb in R_ (sqrt_0 x) & R_ (sqrt_0 x) = (sqrtR ((sqrt_0 x),x)) . 0 & (sqrtR ((sqrt_0 x),x)) . 0 c= Union (sqrtR ((sqrt_0 x),x)) ) by Th1, Def9, ABCMIZ_1:1;
( y in {y} & {y} << R_ y ) by TARSKI:def 1, SURREALO:11;
then ( y < sb & y <= sb ) by A107, A62, A4;
then ( y * y <= sb * y & sb * y < sb * sb ) by A106, A66, SURREALR:75, SURREALR:70;
then y * y < sb * sb by SURREALO:4;
then y * y < b by A106, SURREALO:4;
hence not b <= a by A101, TARSKI:def 1; :: thesis:

end;

A108: L_ x << {(y * y)}

proof

let b, a be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A109: ( b in L_ x & a in {(y * y)} ) ; :: thesis:

per cases ;

suppose A110: b < 0_No ; :: thesis:

0_No * y <= y * y by A66, SURREALR:75;
then b < y * y by A110, SURREALO:4;
hence not a <= b by A109, TARSKI:def 1; :: thesis:

end;

suppose A111: 0_No <= b ; :: thesis:

b in (L_ x) \/ (R_ x) by A109, XBOOLE_0:def 3;
then A112: born b in born x by SURREALO:1;
then reconsider sb = sqrt b as Surreal by A111, A2, A3;
b in L_ (NonNegativePart x) by A109, A111, Def5;
then A113: ( sb in L_ (sqrt_0 x) & L_ (sqrt_0 x) = (sqrtL ((sqrt_0 x),x)) . 0 & (sqrtL ((sqrt_0 x),x)) . 0 c= Union (sqrtL ((sqrt_0 x),x)) ) by Th1, Def9, ABCMIZ_1:1;
A114: ( 0_No <= sb & sb * sb == b ) by A111, A112, A2, A3;
A115: ( y in {y} & L_ y << {y} ) by TARSKI:def 1, SURREALO:11;
then A116: ( sb < y & sb <= y ) by A113, A62, A4;
0_No < y by A114, A113, A62, A4, A115, SURREALO:4;
then ( sb * sb <= sb * y & sb * y < y * y ) by A116, A114, SURREALR:75, SURREALR:70;
then sb * sb < y * y by SURREALO:4;
then b < y * y by A114, SURREALO:4;
hence not a <= b by A109, TARSKI:def 1; :: thesis:

end;

{x} << R_ (y * y)

proof

let b, a be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A117: ( b in {x} & a in R_ (y * y) ) ; :: thesis:
comp ((L_ y),y,y,(R_ y)) = comp ((R_ y),y,y,(L_ y)) by SURREALR:53;
then consider x1, y1 being Surreal such that
A118: ( a = ((x1 * y) + (y * y1)) - (x1 * y1) & x1 in L_ y & y1 in R_ y ) by A67, A117, SURREALR:def 15;
consider n being object such that
A119: ( n in dom (sqrtL ((sqrt_0 x),x)) & x1 in (sqrtL ((sqrt_0 x),x)) . n ) by A118, A4, A62, CARD_5:2;
dom (sqrtL ((sqrt_0 x),x)) = NAT by Def3;
then reconsider n = n as Nat by A119;
consider m being object such that
A120: ( m in dom (sqrtR ((sqrt_0 x),x)) & y1 in (sqrtR ((sqrt_0 x),x)) . m ) by A118, A4, A62, CARD_5:2;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def4;
then reconsider n = n, m = m as Nat by A120;
set nm = n + m;
A121: ( n <= n + m & m <= n + m ) by NAT_1:11;
then A122: ( (sqrtL ((sqrt_0 x),x)) . n c= (sqrtL ((sqrt_0 x),x)) . (n + m) & (sqrtR ((sqrt_0 x),x)) . m c= (sqrtR ((sqrt_0 x),x)) . (n + m) ) by Th2;
set X = x + (x1 * y1);
A123: ( 0_No <= x1 & 0_No < y1 ) by A121, A119, A120, A45;
then 0_No + 0_No < x1 + y1 by SURREALR:44;
then A124: not x1 + y1 == 0_No ;
then (x + (x1 * y1)) * ((x1 + y1) ") in sqrt (x,((sqrtL ((sqrt_0 x),x)) . (n + m)),((sqrtR ((sqrt_0 x),x)) . (n + m))) by A122, A119, A120, Def1;
then (x + (x1 * y1)) * ((x1 + y1) ") in ((sqrtL ((sqrt_0 x),x)) . (n + m)) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . (n + m)),((sqrtR ((sqrt_0 x),x)) . (n + m)))) by XBOOLE_0:def 3;
then A125: ( (x + (x1 * y1)) * ((x1 + y1) ") in (sqrtL ((sqrt_0 x),x)) . ((n + m) + 1) & (sqrtL ((sqrt_0 x),x)) . ((n + m) + 1) c= Union (sqrtL ((sqrt_0 x),x)) ) by Th3, ABCMIZ_1:1;
A126: ( y in {y} & L_ y << {y} ) by TARSKI:def 1, SURREALO:11;
then A127: (x + (x1 * y1)) * ((x1 + y1) ") < y by A125, A62, A4;
A128: (x + (x1 * y1)) * ((x1 + y1) ") <= y by A126, A125, A62, A4;
A129: (x1 + y1) * ((x1 + y1) ") == 1_No by A124, SURREALI:33;
( x1 * ((x + (x1 * y1)) * ((x1 + y1) ")) <= x1 * y & y1 * ((x + (x1 * y1)) * ((x1 + y1) ")) < y1 * y ) by A123, A127, A128, SURREALR:70, SURREALR:75;
then A130: (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) < (x1 * y) + (y * y1) by SURREALR:44;
( (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == (x1 + y1) * ((x + (x1 * y1)) * ((x1 + y1) ")) & (x1 + y1) * ((x + (x1 * y1)) * ((x1 + y1) ")) == ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) ) by SURREALR:67, SURREALR:69;
then ( (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) & ((x1 + y1) * ((x1 + y1) ")) * (x + (x1 * y1)) == 1_No * (x + (x1 * y1)) ) by A129, SURREALR:54, SURREALO:4;
then (x1 * ((x + (x1 * y1)) * ((x1 + y1) "))) + (y1 * ((x + (x1 * y1)) * ((x1 + y1) "))) == 1_No * (x + (x1 * y1)) by SURREALO:4;
then x + (x1 * y1) < (x1 * y) + (y * y1) by A130, SURREALO:4;
then A131: (x + (x1 * y1)) + (- (x1 * y1)) < ((x1 * y) + (y * y1)) + (- (x1 * y1)) by SURREALR:44;
(x1 * y1) - (x1 * y1) == 0_No by SURREALR:39;
then ( (x + (x1 * y1)) + (- (x1 * y1)) = x + ((x1 * y1) + (- (x1 * y1))) & x + ((x1 * y1) + (- (x1 * y1))) == x + 0_No ) by SURREALR:37, SURREALR:66;
then x < a by A118, A131, SURREALO:4;
hence not a <= b by A117, TARSKI:def 1; :: thesis:

end;

hence y * y == x by A68, A100, SURREAL0:43, A108; :: thesis:

end;

A132: for y being Surreal st y = sqrt x holds
( ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) )

proof

let y be Surreal; :: thesis:
assume A133: y = sqrt x ; :: thesis:
thus ( x == 0_No implies y == 0_No ) :: thesis:

proof

assume A134: x == 0_No ; :: thesis:
0_No <= y by A133, A61;
then A135: ( L_ y << {0_No} & {0_No} << R_ y ) by A134, A133, A4, Th18, SURREAL0:43;
for z being Surreal st L_ y << {z} & {z} << R_ y holds
born 0_No c= born z

proof

let z be Surreal; :: thesis:
assume ( L_ y << {z} & {z} << R_ y ) ; :: thesis:
born 0_No = {} by SURREAL0:37;
hence born 0_No c= born z ; :: thesis:

end;

hence y == 0_No by SURREALO:16, A135; :: thesis:

end;

assume A136: ( 0_No < x & y <= 0_No ) ; :: thesis:
then A137: ( y == 0_No & y * y == x ) by A133, A61;
then y * 0_No == y * y by SURREALR:54;
hence contradiction by A136, A137, SURREALO:4; :: thesis:

end;

S is Surreal ;
hence ( sqrt x is surreal & ( for y being Surreal st y = sqrt x holds
( 0_No <= y & y * y == x & ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) ) & ( for y being Surreal st y in L_ (sqrt x) holds
( 0_No <= y & y * y < x ) ) & ( for y being Surreal st y in R_ (sqrt x) holds
( 0_No < y & x < y * y ) ) ) by A46, A48, A61, A132; :: thesis:

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence ( 0_No <= x implies ( ( y = sqrt x implies ( 0_No <= y & y * y == x & ( x == 0_No implies y == 0_No ) & ( 0_No < x implies 0_No < y ) ) ) & ( y in L_ (sqrt x) implies ( 0_No <= y & y * y < x ) ) & ( y in R_ (sqrt x) implies ( 0_No < y & x < y * y ) ) & sqrt x is surreal ) ) ; :: thesis:

end;

theorem Th20: :: SURREALS:20

for x being Surreal st x <= 0_No holds
sqrt x is surreal

proof

let x be Surreal; :: thesis:
assume A1: x <= 0_No ; :: thesis:
A2: L_ (sqrt_0 x) is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis:
assume o in L_ (sqrt_0 x) ; :: thesis:
then consider l being Surreal such that
A3: ( o = sqrt l & l in L_ (NonNegativePart x) ) by Def9;
0_No <= l by A3, Th10;
hence o is surreal by A3, Th19; :: thesis:

end;

R_ (sqrt_0 x) is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis:
assume o in R_ (sqrt_0 x) ; :: thesis:
then consider l being Surreal such that
A4: ( o = sqrt l & l in R_ (NonNegativePart x) ) by Def9;
0_No <= l by A4, Th10;
hence o is surreal by A4, Th19; :: thesis:

end;

then ( Union (sqrtR ((sqrt_0 x),x)) is surreal-membered & Union (sqrtL ((sqrt_0 x),x)) is surreal-membered ) by A2, Th5;
then consider M being Ordinal such that
A5: for o being object st o in (Union (sqrtL ((sqrt_0 x),x))) \/ (Union (sqrtR ((sqrt_0 x),x))) holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
Union (sqrtL ((sqrt_0 x),x)) << Union (sqrtR ((sqrt_0 x),x)) by A1, Th18;
then [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))] in Day M by A5, SURREAL0:46;
hence sqrt x is surreal by Th15; :: thesis:

end;

registration

let x be Surreal;

cluster sqrt x -> surreal ;

coherence

proof

( x <= 0_No or 0_No <= x ) ;
hence sqrt x is surreal by Th19, Th20; :: thesis:

end;

registration

let x be Surreal;

cluster sqrt_0 x -> pair surreal ;

coherence

proof

set S0 = sqrt_0 x;
A1: sqrt_0 x = [(L_ (sqrt_0 x)),(R_ (sqrt_0 x))] ;
A2: sqrt x = [(L_ (sqrt x)),(R_ (sqrt x))] ;
A3: sqrt x = [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))] by Th15;
A4: ( L_ (sqrt_0 x) = (sqrtL ((sqrt_0 x),x)) . 0 & (sqrtL ((sqrt_0 x),x)) . 0 c= Union (sqrtL ((sqrt_0 x),x)) & R_ (sqrt_0 x) = (sqrtR ((sqrt_0 x),x)) . 0 & (sqrtR ((sqrt_0 x),x)) . 0 c= Union (sqrtR ((sqrt_0 x),x)) ) by Th1, ABCMIZ_1:1;
then ( L_ (sqrt_0 x) c= L_ (sqrt x) & R_ (sqrt_0 x) c= R_ (sqrt x) ) by A3;
then A5: ( L_ (sqrt_0 x) is surreal-membered & R_ (sqrt_0 x) is surreal-membered ) by SURREAL0:def 16;
( L_ (sqrt_0 x) <=_ L_ (sqrt x) & R_ (sqrt_0 x) <=_ R_ (sqrt x) ) by A4, A3;
hence sqrt_0 x is surreal by A5, A1, A2, SURREALI:37; :: thesis:

end;

theorem Th21: :: SURREALS:21

for x being Surreal st 0_No <= x holds
( 0_No <= sqrt x & (sqrt x) * (sqrt x) == x ) by Th19;

theorem :: SURREALS:22

for x being Surreal st 0_No == x holds
sqrt x == 0_No by Th19;

theorem :: SURREALS:23

for x, y being Surreal st 0_No <= x holds
( ( y in L_ (sqrt x) implies ( 0_No <= y & y * y < x ) ) & ( y in R_ (sqrt x) implies ( 0_No < y & x < y * y ) ) ) by Th19;

theorem :: SURREALS:24

for x being Surreal st x < 0_No & ( for y being Surreal st y in R_ x holds
y < 0_No ) holds
sqrt x = 0_No

proof

let x be Surreal; :: thesis:
assume that
A1: x < 0_No and
A2: for y being Surreal st y in R_ x holds
y < 0_No ; :: thesis:
defpred S₁[ Nat] means (sqrtR ((sqrt_0 x),x)) . $1 = {} ;
A3: S₁[ 0 ]

proof

assume (sqrtR ((sqrt_0 x),x)) . 0 <> {} ; :: thesis:
then consider a being object such that
A4: a in (sqrtR ((sqrt_0 x),x)) . 0 by XBOOLE_0:def 1;
a in R_ (sqrt_0 x) by A4, Th1;
then consider r being Surreal such that
A5: ( a = sqrt r & r in R_ (NonNegativePart x) ) by Def9;
( r in R_ x & 0_No <= r ) by A5, Th10;
hence contradiction by A2; :: thesis:

end;

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

proof

let n be Nat; :: thesis:
assume A7: S₁[n] ; :: thesis:
assume (sqrtR ((sqrt_0 x),x)) . (n + 1) <> {} ; :: thesis:
then consider y being object such that
A8: y in (sqrtR ((sqrt_0 x),x)) . (n + 1) by XBOOLE_0:def 1;
y in (((sqrtR ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)))) \/ (sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n))) by A8, Th3;
then ( y in ((sqrtR ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n))) or y in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ) by XBOOLE_0:def 3;

per cases by XBOOLE_0:def 3;

suppose y in (sqrtR ((sqrt_0 x),x)) . n ; :: thesis:

hence contradiction by A7; :: thesis:

end;

suppose y in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)) ; :: thesis:

then consider x1, y1 being Surreal such that
A9: ( x1 in (sqrtL ((sqrt_0 x),x)) . n & y1 in (sqrtL ((sqrt_0 x),x)) . n & not x1 + y1 == 0_No & y = (x +' (x1 * y1)) * ((x1 + y1) ") ) by Def1;
x <= 0_No by A1;
then ( (sqrtL ((sqrt_0 x),x)) . n c= Union (sqrtL ((sqrt_0 x),x)) & Union (sqrtL ((sqrt_0 x),x)) = {} ) by ABCMIZ_1:1, Th18;
hence contradiction by A9; :: thesis:

end;

suppose y in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ; :: thesis:

then ex x1, y1 being Surreal st
( x1 in (sqrtR ((sqrt_0 x),x)) . n & y1 in (sqrtR ((sqrt_0 x),x)) . n & not x1 + y1 == 0_No & y = (x +' (x1 * y1)) * ((x1 + y1) ") ) by Def1;
hence contradiction by A7; :: thesis:

end;

A10: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A6);
A11: Union (sqrtR ((sqrt_0 x),x)) = {}

proof

assume Union (sqrtR ((sqrt_0 x),x)) <> {} ; :: thesis:
then consider a being object such that
A12: a in Union (sqrtR ((sqrt_0 x),x)) by XBOOLE_0:def 1;
consider n being object such that
A13: ( n in dom (sqrtR ((sqrt_0 x),x)) & a in (sqrtR ((sqrt_0 x),x)) . n ) by A12, CARD_5:2;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def4;
then reconsider n = n as Nat by A13;
(sqrtR ((sqrt_0 x),x)) . n = {} by A10;
hence contradiction by A13; :: thesis:

end;

x <= 0_No by A1;
then Union (sqrtL ((sqrt_0 x),x)) = {} by Th18;
hence sqrt x = 0_No by A11, Th15; :: thesis:

end;

theorem Th25: :: SURREALS:25

for x being Surreal st ( for y being Surreal st y in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) holds
y == 0_No ) holds
sqrt x = sqrt_0 x

proof

let x be Surreal; :: thesis:
assume A1: for y being Surreal st y in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) holds
y == 0_No ; :: thesis:
defpred S₁[ Nat] means ( (sqrtL ((sqrt_0 x),x)) . $1 = L_ (sqrt_0 x) & (sqrtR ((sqrt_0 x),x)) . $1 = R_ (sqrt_0 x) );
A2: S₁[ 0 ] by Th1;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A4: S₁[n] ; :: thesis:
set S0 = sqrt_0 x;
set n1 = n + 1;
(sqrtL ((sqrt_0 x),x)) . 0 c= (sqrtL ((sqrt_0 x),x)) . (n + 1) by Th2;
then A5: L_ (sqrt_0 x) c= (sqrtL ((sqrt_0 x),x)) . (n + 1) by Th1;
(sqrtL ((sqrt_0 x),x)) . (n + 1) c= L_ (sqrt_0 x)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: ( o in (sqrtL ((sqrt_0 x),x)) . (n + 1) & not o in L_ (sqrt_0 x) ) ; :: thesis:
o in ((sqrtL ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n))) by A6, Th3;
then o in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) by A4, A6, XBOOLE_0:def 3;
then consider x1, y1 being Surreal such that
A7: ( x1 in (sqrtL ((sqrt_0 x),x)) . n & y1 in (sqrtR ((sqrt_0 x),x)) . n & not x1 + y1 == 0_No & o = (x +' (x1 * y1)) * ((x1 + y1) ") ) by Def1;
consider l being Surreal such that
A8: ( x1 = sqrt l & l in L_ (NonNegativePart x) ) by A4, A7, Def9;
l in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by A8, XBOOLE_0:def 3;
then l == 0_No by A1;
then A9: x1 == 0_No by A8, Th19;
consider r being Surreal such that
A10: ( y1 = sqrt r & r in R_ (NonNegativePart x) ) by A4, A7, Def9;
r in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by A10, XBOOLE_0:def 3;
then r == 0_No by A1;
then y1 == 0_No by A10, Th19;
then x1 + y1 == 0_No + 0_No by A9, SURREALR:66;
hence contradiction by A7; :: thesis:

end;

hence (sqrtL ((sqrt_0 x),x)) . (n + 1) = L_ (sqrt_0 x) by A5, XBOOLE_0:def 10; :: thesis:
(sqrtR ((sqrt_0 x),x)) . 0 c= (sqrtR ((sqrt_0 x),x)) . (n + 1) by Th2;
then A11: R_ (sqrt_0 x) c= (sqrtR ((sqrt_0 x),x)) . (n + 1) by Th1;
(sqrtR ((sqrt_0 x),x)) . (n + 1) c= R_ (sqrt_0 x)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A12: ( o in (sqrtR ((sqrt_0 x),x)) . (n + 1) & not o in R_ (sqrt_0 x) ) ; :: thesis:
o in (((sqrtR ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)))) \/ (sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n))) by A12, Th3;
then ( o in ((sqrtR ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n))) or o in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ) by XBOOLE_0:def 3;

per cases by A4, A12, XBOOLE_0:def 3;

suppose o in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)) ; :: thesis:

then consider x1, y1 being Surreal such that
A13: ( x1 in (sqrtL ((sqrt_0 x),x)) . n & y1 in (sqrtL ((sqrt_0 x),x)) . n & not x1 + y1 == 0_No & o = (x +' (x1 * y1)) * ((x1 + y1) ") ) by Def1;
consider l being Surreal such that
A14: ( x1 = sqrt l & l in L_ (NonNegativePart x) ) by Def9, A4, A13;
l in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by A14, XBOOLE_0:def 3;
then l == 0_No by A1;
then A15: x1 == 0_No by A14, Th19;
consider r being Surreal such that
A16: ( y1 = sqrt r & r in L_ (NonNegativePart x) ) by Def9, A4, A13;
r in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by A16, XBOOLE_0:def 3;
then r == 0_No by A1;
then y1 == 0_No by A16, Th19;
then x1 + y1 == 0_No + 0_No by A15, SURREALR:66;
hence contradiction by A13; :: thesis:

end;

suppose o in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ; :: thesis:

then consider x1, y1 being Surreal such that
A17: ( x1 in (sqrtR ((sqrt_0 x),x)) . n & y1 in (sqrtR ((sqrt_0 x),x)) . n & not x1 + y1 == 0_No & o = (x +' (x1 * y1)) * ((x1 + y1) ") ) by Def1;
consider l being Surreal such that
A18: ( x1 = sqrt l & l in R_ (NonNegativePart x) ) by Def9, A4, A17;
l in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by A18, XBOOLE_0:def 3;
then l == 0_No by A1;
then A19: x1 == 0_No by A18, Th19;
consider r being Surreal such that
A20: ( y1 = sqrt r & r in R_ (NonNegativePart x) ) by Def9, A4, A17;
r in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) by A20, XBOOLE_0:def 3;
then r == 0_No by A1;
then y1 == 0_No by A20, Th19;
then x1 + y1 == 0_No + 0_No by A19, SURREALR:66;
hence contradiction by A17; :: thesis:

end;

hence (sqrtR ((sqrt_0 x),x)) . (n + 1) = R_ (sqrt_0 x) by A11, XBOOLE_0:def 10; :: thesis:

end;

A21: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
A22: sqrt x = [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))] by Th15;
A23: L_ (sqrt x) = L_ (sqrt_0 x)

proof

thus L_ (sqrt x) c= L_ (sqrt_0 x) :: according to XBOOLE_0:def 10 :: thesis:

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in L_ (sqrt x) ; :: thesis:
then consider n being object such that
A24: ( n in dom (sqrtL ((sqrt_0 x),x)) & o in (sqrtL ((sqrt_0 x),x)) . n ) by A22, CARD_5:2;
dom (sqrtL ((sqrt_0 x),x)) = NAT by Def3;
then reconsider n = n as Nat by A24;
(sqrtL ((sqrt_0 x),x)) . n = L_ (sqrt_0 x) by A21;
hence o in L_ (sqrt_0 x) by A24; :: thesis:

end;

thus L_ (sqrt_0 x) c= L_ (sqrt x) by A2, A22, ABCMIZ_1:1; :: thesis:

end;

R_ (sqrt x) = R_ (sqrt_0 x)

proof

thus R_ (sqrt x) c= R_ (sqrt_0 x) :: according to XBOOLE_0:def 10 :: thesis:

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in R_ (sqrt x) ; :: thesis:
then consider n being object such that
A25: ( n in dom (sqrtR ((sqrt_0 x),x)) & o in (sqrtR ((sqrt_0 x),x)) . n ) by A22, CARD_5:2;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def4;
then reconsider n = n as Nat by A25;
(sqrtR ((sqrt_0 x),x)) . n = R_ (sqrt_0 x) by A21;
hence o in R_ (sqrt_0 x) by A25; :: thesis:

end;

thus R_ (sqrt_0 x) c= R_ (sqrt x) by A2, A22, ABCMIZ_1:1; :: thesis:

end;

hence sqrt x = sqrt_0 x by A23, XTUPLE_0:2; :: thesis:

end;

registration

reduce sqrt 0_No with 0_No ;

reducibility

proof

set S0 = sqrt_0 0_No;
A1: L_ (sqrt_0 0_No) = {}

proof

assume L_ (sqrt_0 0_No) <> {} ; :: thesis:
then consider o being object such that
A2: o in L_ (sqrt_0 0_No) by XBOOLE_0:def 1;
consider l being Surreal such that
A3: ( o = sqrt l & l in L_ (NonNegativePart 0_No) ) by A2, Def9;
l in L_ 0_No by A3, Th10;
hence contradiction ; :: thesis:

end;

A4: R_ (sqrt_0 0_No) = {}

proof

assume R_ (sqrt_0 0_No) <> {} ; :: thesis:
then consider o being object such that
A5: o in R_ (sqrt_0 0_No) by XBOOLE_0:def 1;
consider r being Surreal such that
A6: ( o = sqrt r & r in R_ (NonNegativePart 0_No) ) by A5, Def9;
r in R_ 0_No by A6, Th10;
hence contradiction ; :: thesis:

end;

for y being Surreal st y in (L_ (NonNegativePart 0_No)) \/ (R_ (NonNegativePart 0_No)) holds
y == 0_No

proof

let y be Surreal; :: thesis:
assume y in (L_ (NonNegativePart 0_No)) \/ (R_ (NonNegativePart 0_No)) ; :: thesis:
then ( y in L_ (NonNegativePart 0_No) or y in R_ (NonNegativePart 0_No) ) by XBOOLE_0:def 3;
then ( y in L_ 0_No or y in R_ 0_No ) by Th10;
hence y == 0_No ; :: thesis:

end;

hence sqrt 0_No = 0_No by A1, A4, Th25; :: thesis:

end;

reduce sqrt 1_No with 1_No ;

reducibility

proof

set S0 = sqrt_0 1_No;
( 0_No in L_ 1_No & 0_No <= 0_No ) by TARSKI:def 1;
then 0_No in L_ (NonNegativePart 1_No) by Def5;
then A7: sqrt 0_No in L_ (sqrt_0 1_No) by Def9;
L_ (sqrt_0 1_No) c= {0_No}

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in L_ (sqrt_0 1_No) ; :: thesis:
then consider l being Surreal such that
A8: ( o = sqrt l & l in L_ (NonNegativePart 1_No) ) by Def9;
l in L_ 1_No by A8, Th10;
then l = 0_No by TARSKI:def 1;
hence o in {0_No} by A8, TARSKI:def 1; :: thesis:

end;

then A9: L_ (sqrt_0 1_No) = {0_No} by A7, ZFMISC_1:33;
A10: R_ (sqrt_0 1_No) = {}

proof

assume R_ (sqrt_0 1_No) <> {} ; :: thesis:
then consider o being object such that
A11: o in R_ (sqrt_0 1_No) by XBOOLE_0:def 1;
consider r being Surreal such that
A12: ( o = sqrt r & r in R_ (NonNegativePart 1_No) ) by A11, Def9;
r in R_ 1_No by A12, Th10;
hence contradiction ; :: thesis:

end;

for y being Surreal st y in (L_ (NonNegativePart 1_No)) \/ (R_ (NonNegativePart 1_No)) holds
y == 0_No

proof

let y be Surreal; :: thesis:
assume y in (L_ (NonNegativePart 1_No)) \/ (R_ (NonNegativePart 1_No)) ; :: thesis:
then ( y in L_ (NonNegativePart 1_No) or y in R_ (NonNegativePart 1_No) ) by XBOOLE_0:def 3;
then ( y in L_ 1_No or y in R_ 1_No ) by Th10;
hence y == 0_No by TARSKI:def 1; :: thesis:

end;

hence sqrt 1_No = 1_No by A10, A9, Th25; :: thesis:

end;

reduce sqrt (- 1_No) with - 1_No;

reducibility

proof

A13: - 1_No = [(-- (R_ 1_No)),(-- (L_ 1_No))] by SURREALR:7
.= [{},{(- 0_No)}] by SURREALR:21, SURREALR:22 ;
set S0 = sqrt_0 (- 1_No);
0_No in R_ (- 1_No) by A13, TARSKI:def 1;
then 0_No in R_ (NonNegativePart (- 1_No)) by Def5;
then A14: sqrt 0_No in R_ (sqrt_0 (- 1_No)) by Def9;
R_ (sqrt_0 (- 1_No)) c= {0_No}

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in R_ (sqrt_0 (- 1_No)) ; :: thesis:
then consider r being Surreal such that
A15: ( o = sqrt r & r in R_ (NonNegativePart (- 1_No)) ) by Def9;
r in R_ (- 1_No) by A15, Th10;
then r = 0_No by A13, TARSKI:def 1;
hence o in {0_No} by A15, TARSKI:def 1; :: thesis:

end;

then A16: R_ (sqrt_0 (- 1_No)) = {0_No} by A14, ZFMISC_1:33;
A17: L_ (sqrt_0 (- 1_No)) = {}

proof

assume L_ (sqrt_0 (- 1_No)) <> {} ; :: thesis:
then consider o being object such that
A18: o in L_ (sqrt_0 (- 1_No)) by XBOOLE_0:def 1;
consider l being Surreal such that
A19: ( o = sqrt l & l in L_ (NonNegativePart (- 1_No)) ) by A18, Def9;
l in L_ (- 1_No) by A19, Th10;
hence contradiction by A13; :: thesis:

end;

for y being Surreal st y in (L_ (NonNegativePart (- 1_No))) \/ (R_ (NonNegativePart (- 1_No))) holds
y == 0_No

proof

let y be Surreal; :: thesis:
assume y in (L_ (NonNegativePart (- 1_No))) \/ (R_ (NonNegativePart (- 1_No))) ; :: thesis:
then ( y in L_ (NonNegativePart (- 1_No)) or y in R_ (NonNegativePart (- 1_No)) ) by XBOOLE_0:def 3;
then ( y in L_ (- 1_No) or y in R_ (- 1_No) ) by Th10;
hence y == 0_No by A13, TARSKI:def 1; :: thesis:

end;

hence sqrt (- 1_No) = - 1_No by A17, Th25, A13, A16; :: thesis:

end;

theorem :: SURREALS:26

for x, y being Surreal st 0_No <= x & x <= y holds
sqrt x <= sqrt y

proof

let x, y be Surreal; :: thesis:
assume that
A1: ( 0_No <= x & x <= y ) and
A2: sqrt y < sqrt x ; :: thesis:
A3: ( 0_No <= sqrt x & (sqrt x) * (sqrt x) == x ) by A1, Th19;
0_No <= y by A1, SURREALO:4;
then A4: ( 0_No <= sqrt y & (sqrt y) * (sqrt y) == y ) by Th19;
0_No < sqrt x by A4, A2, SURREALO:4;
then (sqrt y) * (sqrt x) < (sqrt x) * (sqrt x) by A2, SURREALR:70;
then A5: (sqrt y) * (sqrt x) < x by A3, SURREALO:4;
sqrt y <= sqrt x by A2;
then (sqrt y) * (sqrt y) <= (sqrt x) * (sqrt y) by A4, SURREALR:75;
then y <= (sqrt x) * (sqrt y) by A4, SURREALO:4;
hence contradiction by A1, A5, SURREALO:4; :: thesis:

end;

theorem Th27: :: SURREALS:27

for x, y being Surreal st 0_No <= x & x < y holds
sqrt x < sqrt y

proof

let x, y be Surreal; :: thesis:
assume that
A1: ( 0_No <= x & x < y ) and
A2: sqrt y <= sqrt x ; :: thesis:
A3: ( 0_No <= sqrt x & (sqrt x) * (sqrt x) == x ) by A1, Th19;
0_No <= y by A1, SURREALO:4;
then A4: ( 0_No <= sqrt y & (sqrt y) * (sqrt y) == y ) by Th19;
(sqrt y) * (sqrt x) <= (sqrt x) * (sqrt x) by A3, A2, SURREALR:75;
then A5: (sqrt y) * (sqrt x) <= x by A3, SURREALO:4;
(sqrt y) * (sqrt y) <= (sqrt x) * (sqrt y) by A2, A4, SURREALR:75;
then y <= (sqrt x) * (sqrt y) by A4, SURREALO:4;
hence contradiction by A1, A5, SURREALO:4; :: thesis:

end;

theorem Th28: :: SURREALS:28

for x, y being Surreal st 0_No <= x & x == y * y & not y == sqrt x holds
y == - (sqrt x)

proof

let x, y be Surreal; :: thesis:
set s = sqrt x;
assume A1: ( 0_No <= x & x == y * y ) ; :: thesis:
then A2: (sqrt x) * (sqrt x) == x by Th19;
( ((sqrt x) + (- y)) * (sqrt x) == ((sqrt x) * (sqrt x)) + ((- y) * (sqrt x)) & ((sqrt x) + (- y)) * y == ((sqrt x) * y) + ((- y) * y) ) by SURREALR:67;
then ( ((sqrt x) + (- y)) * ((sqrt x) + y) == (((sqrt x) + (- y)) * (sqrt x)) + (((sqrt x) + (- y)) * y) & (((sqrt x) + (- y)) * (sqrt x)) + (((sqrt x) + (- y)) * y) == (((sqrt x) * (sqrt x)) + ((- y) * (sqrt x))) + (((sqrt x) * y) + ((- y) * y)) ) by SURREALR:67, SURREALR:66;
then A3: ((sqrt x) + (- y)) * ((sqrt x) + y) == (((sqrt x) * (sqrt x)) + ((- y) * (sqrt x))) + (((sqrt x) * y) + ((- y) * y)) by SURREALO:4;
( ((- y) * (sqrt x)) + ((sqrt x) * y) == (- ((sqrt x) * y)) + ((sqrt x) * y) & (- ((sqrt x) * y)) + ((sqrt x) * y) = ((sqrt x) * y) - ((sqrt x) * y) & ((sqrt x) * y) - ((sqrt x) * y) == 0_No ) by SURREALR:39, SURREALR:58;
then A4: ((- y) * (sqrt x)) + ((sqrt x) * y) == 0_No by SURREALO:4;
A5: ((sqrt x) * (sqrt x)) + ((- y) * y) == ((sqrt x) * (sqrt x)) + (- (y * y)) by SURREALR:58;
A6: - (y * y) == - x by A1, SURREALR:65;
(((sqrt x) * (sqrt x)) + ((- y) * (sqrt x))) + (((sqrt x) * y) + ((- y) * y)) = ((sqrt x) * (sqrt x)) + (((- y) * (sqrt x)) + (((sqrt x) * y) + ((- y) * y))) by SURREALR:37
.= ((sqrt x) * (sqrt x)) + ((((- y) * (sqrt x)) + ((sqrt x) * y)) + ((- y) * y)) by SURREALR:37
.= (((sqrt x) * (sqrt x)) + ((- y) * y)) + (((- y) * (sqrt x)) + ((sqrt x) * y)) by SURREALR:37 ;
then (((sqrt x) * (sqrt x)) + ((- y) * (sqrt x))) + (((sqrt x) * y) + ((- y) * y)) == (((sqrt x) * (sqrt x)) + (- (y * y))) + 0_No by A4, A5, SURREALR:66;
then ( ((sqrt x) + (- y)) * ((sqrt x) + y) == ((sqrt x) * (sqrt x)) + (- (y * y)) & ((sqrt x) * (sqrt x)) + (- (y * y)) == x - x ) by SURREALR:66, A3, A6, SURREALO:4, A2;
then ( ((sqrt x) + (- y)) * ((sqrt x) + y) == x - x & x - x == 0_No ) by SURREALO:4, SURREALR:39;
then ((sqrt x) + (- y)) * ((sqrt x) + y) == 0_No by SURREALO:4;
then ( (sqrt x) - y == 0_No or (sqrt x) - (- y) == 0_No ) by SURREALR:72, SURREALR:74;
then ( sqrt x == y or sqrt x == - y ) by SURREALR:47;
then ( sqrt x == y or - (sqrt x) == - (- y) ) by SURREALR:10;
hence ( y == sqrt x or y == - (sqrt x) ) ; :: thesis:

end;

registration

let x be positive Surreal;

cluster sqrt x -> positive ;

coherence

proof

sqrt 0_No < sqrt x by Th27, SURREALI:def 8;
hence sqrt x is positive ; :: thesis:

end;

theorem Th29: :: SURREALS:29

for x being Surreal st 0_No <= x holds
sqrt (x * x) == x

proof

let x be Surreal; :: thesis:
set S = sqrt (x * x);
assume that
A1: 0_No <= x and
A2: not sqrt (x * x) == x ; :: thesis:
A3: 0_No * x <= x * x by A1, SURREALR:75;
0_No * x <= x * x by A1, SURREALR:75;
then A4: ( x == sqrt (x * x) or x == - (sqrt (x * x)) ) by Th28;
then - 0_No <= - (sqrt (x * x)) by A2, A1, SURREALO:4;
then A5: sqrt (x * x) == 0_No by A3, Th19, SURREALR:10;
then - (sqrt (x * x)) == - 0_No by SURREALR:10;
then x == - 0_No by A4, A2, SURREALO:4;
hence contradiction by A2, A5, SURREALO:4; :: thesis:

end;

theorem :: SURREALS:30

for x being Surreal st 0_No < x holds
(sqrt x) " == sqrt (x ")

proof

let x be Surreal; :: thesis:
assume A1: 0_No < x ; :: thesis:
then reconsider a = x as positive Surreal by SURREALI:def 8;
set S = sqrt a;
set T = sqrt (a ");
A2: ( not sqrt a == 0_No & not sqrt (a ") == 0_No ) by SURREALI:def 8;
A3: 0_No <= a " by SURREALI:def 8;
0_No <= x by A1;
then ( ((sqrt a) * (sqrt a)) * ((sqrt (a ")) * (sqrt (a "))) == a * ((sqrt (a ")) * (sqrt (a "))) & a * ((sqrt (a ")) * (sqrt (a "))) == a * (a ") ) by A3, Th21, SURREALR:54;
then A4: ((sqrt a) * (sqrt a)) * ((sqrt (a ")) * (sqrt (a "))) == a * (a ") by SURREALO:4;
not a == 0_No by A1;
then a * (a ") == 1_No by SURREALI:33;
then A5: ((sqrt a) * (sqrt a)) * ((sqrt (a ")) * (sqrt (a "))) == 1_No by A4, SURREALO:4;
A6: 0_No <= 1_No by SURREALI:def 8;
A7: - 1_No <= - 0_No by SURREALR:10, SURREALI:def 8;
( ((sqrt a) * (sqrt a)) * ((sqrt (a ")) * (sqrt (a "))) == (((sqrt a) * (sqrt a)) * (sqrt (a "))) * (sqrt (a ")) & (((sqrt a) * (sqrt a)) * (sqrt (a "))) * (sqrt (a ")) == ((sqrt a) * ((sqrt a) * (sqrt (a ")))) * (sqrt (a ")) ) by SURREALR:69, SURREALR:54;
then ( ((sqrt a) * (sqrt a)) * ((sqrt (a ")) * (sqrt (a "))) == ((sqrt a) * ((sqrt a) * (sqrt (a ")))) * (sqrt (a ")) & ((sqrt a) * ((sqrt a) * (sqrt (a ")))) * (sqrt (a ")) == ((sqrt a) * (sqrt (a "))) * ((sqrt a) * (sqrt (a "))) ) by SURREALO:4, SURREALR:69;
then ((sqrt a) * (sqrt a)) * ((sqrt (a ")) * (sqrt (a "))) == ((sqrt a) * (sqrt (a "))) * ((sqrt a) * (sqrt (a "))) by SURREALO:4;
then ((sqrt a) * (sqrt (a "))) * ((sqrt a) * (sqrt (a "))) == 1_No by A5, SURREALO:4;
then ( (sqrt a) * (sqrt (a ")) == sqrt 1_No or (sqrt a) * (sqrt (a ")) == - (sqrt 1_No) ) by A6, Th28;
hence (sqrt x) " == sqrt (x ") by A2, A7, SURREALI:def 8, SURREALI:42, SURREALO:4; :: thesis:

end;

theorem Th31: :: SURREALS:31

for x being Surreal st 0_No < x holds
ex y being Surreal st
( - 1_No == y & sqrt y < - x & y = [{},{0_No,(((sqrt ((x * x) + 1_No)) - x) * ((sqrt ((x * x) + 1_No)) - x))}] )

proof

let x be Surreal; :: thesis:
assume A1: 0_No < x ; :: thesis:
reconsider p = x as positive Surreal by A1, SURREALI:def 8;
A2: - 1_No = [(-- (R_ 1_No)),(-- (L_ 1_No))] by SURREALR:7
.= [{},{(- 0_No)}] by SURREALR:21, SURREALR:22 ;
A3: 0_No <= x by A1;
then A4: x * 0_No <= x * x by SURREALR:75;
A5: (x * x) + 0_No < (x * x) + 1_No by SURREALR:44, SURREALI:def 8;
then ( x == sqrt (x * x) & sqrt (x * x) < sqrt ((x * x) + 1_No) ) by A4, Th27, A3, Th29;
then x < sqrt ((x * x) + 1_No) by SURREALO:4;
then 0_No < (sqrt ((x * x) + 1_No)) - x by SURREALR:45;
then reconsider Y = (sqrt ((x * x) + 1_No)) + (- x) as positive Surreal by SURREALI:def 8;
set YY = Y * Y;
{0_No} \/ {(Y * Y)} is surreal-membered ;
then reconsider Y0 = {0_No,(Y * Y)} as surreal-membered set by ENUMSET1:1;
consider M being Ordinal such that
A6: for o being object st o in {} \/ Y0 holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
{} << Y0 ;
then [{},Y0] in Day M by A6, SURREAL0:46;
then reconsider y = [{},Y0] as Surreal ;
take y ; :: thesis:
A7: 0_No <= Y * Y by SURREALI:def 8;
A8: for z being Surreal st z in R_ y holds
0_No <= z by A7, TARSKI:def 2;
A9: - 1_No = [(L_ y),{0_No}] by A2;
0_No in R_ y by TARSKI:def 2;
hence A10: - 1_No == y by A9, A8, SURREALO:24; :: thesis:
(sqrt (Y * Y)) + (sqrt (Y * Y)) is positive ;
then A11: not (sqrt (Y * Y)) + (sqrt (Y * Y)) == 0_No ;
Y * Y in R_ y by TARSKI:def 2;
then Y * Y in R_ (NonNegativePart y) by A7, Def5;
then sqrt (Y * Y) in R_ (sqrt_0 y) by Def9;
then sqrt (Y * Y) in (sqrtR ((sqrt_0 y),y)) . 0 by Th1;
then A12: (y + ((sqrt (Y * Y)) * (sqrt (Y * Y)))) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") in sqrt (y,((sqrtR ((sqrt_0 y),y)) . 0),((sqrtR ((sqrt_0 y),y)) . 0)) by A11, Def1;
sqrt y = [(Union (sqrtL ((sqrt_0 y),y))),(Union (sqrtR ((sqrt_0 y),y)))] by Th15;
then A13: ( {(sqrt y)} << R_ (sqrt y) & R_ (sqrt y) = Union (sqrtR ((sqrt_0 y),y)) & sqrt y in {(sqrt y)} ) by TARSKI:def 1, SURREALO:11;
(sqrtR ((sqrt_0 y),y)) . (0 + 1) = (((sqrtR ((sqrt_0 y),y)) . 0) \/ (sqrt (y,((sqrtL ((sqrt_0 y),y)) . 0),((sqrtL ((sqrt_0 y),y)) . 0)))) \/ (sqrt (y,((sqrtR ((sqrt_0 y),y)) . 0),((sqrtR ((sqrt_0 y),y)) . 0))) by Th3;
then A14: ( (y + ((sqrt (Y * Y)) * (sqrt (Y * Y)))) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") in (sqrtR ((sqrt_0 y),y)) . 1 & (sqrtR ((sqrt_0 y),y)) . 1 c= Union (sqrtR ((sqrt_0 y),y)) ) by ABCMIZ_1:1, XBOOLE_0:def 3, A12;
set TWO = 1_No + 1_No;
A15: ( not 0_No == Y " & not 0_No == Y & not 1_No + 1_No == 0_No ) by SURREALI:def 8;
then A16: ( (Y ") " == Y & Y * (Y ") == 1_No & (1_No + 1_No) * ((1_No + 1_No) ") == 1_No ) by SURREALI:44, SURREALI:33;
0_No <= Y by SURREALI:def 8;
then sqrt (Y * Y) == Y by Th29;
then ( (sqrt (Y * Y)) + (sqrt (Y * Y)) == Y + Y & Y + Y = (1_No * Y) + (1_No * Y) & (1_No * Y) + (1_No * Y) == (1_No + 1_No) * Y ) by SURREALR:66, SURREALR:67;
then (sqrt (Y * Y)) + (sqrt (Y * Y)) == (1_No + 1_No) * Y by SURREALO:4;
then ( ((sqrt (Y * Y)) + (sqrt (Y * Y))) " == ((1_No + 1_No) * Y) " & ((1_No + 1_No) * Y) " == ((1_No + 1_No) ") * (Y ") ) by A11, A15, SURREALI:43, SURREALI:45;
then A17: ((sqrt (Y * Y)) + (sqrt (Y * Y))) " == ((1_No + 1_No) ") * (Y ") by SURREALO:4;
A18: (sqrt (Y * Y)) * (sqrt (Y * Y)) == Y * Y by A7, Th19;
A19: Y * Y == (((sqrt ((x * x) + 1_No)) * (sqrt ((x * x) + 1_No))) + ((- x) * (- x))) + (((sqrt ((x * x) + 1_No)) * (- x)) + ((- x) * (sqrt ((x * x) + 1_No)))) by SURREALR:76;
0_No <= (x * x) + 1_No by A4, A5, SURREALO:4;
then ( (sqrt ((x * x) + 1_No)) * (sqrt ((x * x) + 1_No)) == (x * x) + 1_No & (- x) * (- x) = x * x ) by Th19, SURREALR:58;
then A20: ( ((sqrt ((x * x) + 1_No)) * (sqrt ((x * x) + 1_No))) + ((- x) * (- x)) == ((x * x) + 1_No) + (x * x) & ((x * x) + 1_No) + (x * x) = 1_No + ((x * x) + (x * x)) ) by SURREALR:37, SURREALR:66;
x * x = 1_No * (x * x) ;
then (x * x) + (x * x) == (1_No + 1_No) * (x * x) by SURREALR:67;
then 1_No + ((x * x) + (x * x)) == 1_No + ((1_No + 1_No) * (x * x)) by SURREALR:66;
then A21: ((sqrt ((x * x) + 1_No)) * (sqrt ((x * x) + 1_No))) + ((- x) * (- x)) == 1_No + ((1_No + 1_No) * (x * x)) by A20, SURREALO:4;
1_No * ((sqrt ((x * x) + 1_No)) * (- x)) = (sqrt ((x * x) + 1_No)) * (- x) ;
then ((sqrt ((x * x) + 1_No)) * (- x)) + ((sqrt ((x * x) + 1_No)) * (- x)) == (1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x)) by SURREALR:67;
then (((sqrt ((x * x) + 1_No)) * (sqrt ((x * x) + 1_No))) + ((- x) * (- x))) + (((sqrt ((x * x) + 1_No)) * (- x)) + ((- x) * (sqrt ((x * x) + 1_No)))) == (1_No + ((1_No + 1_No) * (x * x))) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x))) by A21, SURREALR:66;
then Y * Y == (1_No + ((1_No + 1_No) * (x * x))) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x))) by A19, SURREALO:4;
then A22: ( (sqrt (Y * Y)) * (sqrt (Y * Y)) == (1_No + ((1_No + 1_No) * (x * x))) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x))) & (1_No + ((1_No + 1_No) * (x * x))) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x))) = 1_No + (((1_No + 1_No) * (x * x)) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x)))) ) by A18, SURREALO:4, SURREALR:37;
A23: 1_No - 1_No == 0_No by SURREALR:39;
x * x = (- x) * (- x) by SURREALR:58;
then ( ((1_No + 1_No) * (x * x)) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x))) == (1_No + 1_No) * ((x * x) + ((sqrt ((x * x) + 1_No)) * (- x))) & (1_No + 1_No) * ((x * x) + ((sqrt ((x * x) + 1_No)) * (- x))) == (1_No + 1_No) * ((- x) * Y) ) by SURREALR:54, SURREALR:67;
then ((1_No + 1_No) * (x * x)) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x))) == (1_No + 1_No) * ((- x) * Y) by SURREALO:4;
then 1_No + (((1_No + 1_No) * (x * x)) + ((1_No + 1_No) * ((sqrt ((x * x) + 1_No)) * (- x)))) == 1_No + ((1_No + 1_No) * ((- x) * Y)) by SURREALR:66;
then (sqrt (Y * Y)) * (sqrt (Y * Y)) == 1_No + ((1_No + 1_No) * ((- x) * Y)) by A22, SURREALO:4;
then ( y + ((sqrt (Y * Y)) * (sqrt (Y * Y))) == (- 1_No) + (1_No + ((1_No + 1_No) * ((- x) * Y))) & (- 1_No) + (1_No + ((1_No + 1_No) * ((- x) * Y))) = (1_No - 1_No) + ((1_No + 1_No) * ((- x) * Y)) & (1_No - 1_No) + ((1_No + 1_No) * ((- x) * Y)) == 0_No + ((1_No + 1_No) * ((- x) * Y)) ) by A23, A10, SURREALR:66, SURREALR:37;
then y + ((sqrt (Y * Y)) * (sqrt (Y * Y))) == (1_No + 1_No) * ((- x) * Y) by SURREALO:4;
then ( (y + ((sqrt (Y * Y)) * (sqrt (Y * Y)))) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") == ((1_No + 1_No) * ((- x) * Y)) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") & ((1_No + 1_No) * ((- x) * Y)) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") == ((1_No + 1_No) * ((- x) * Y)) * (((1_No + 1_No) ") * (Y ")) ) by A17, SURREALR:54;
then A24: (y + ((sqrt (Y * Y)) * (sqrt (Y * Y)))) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") == ((1_No + 1_No) * ((- x) * Y)) * (((1_No + 1_No) ") * (Y ")) by SURREALO:4;
( ((1_No + 1_No) * ((- x) * Y)) * (((1_No + 1_No) ") * (Y ")) == ((- x) * ((1_No + 1_No) * Y)) * (((1_No + 1_No) ") * (Y ")) & ((- x) * ((1_No + 1_No) * Y)) * (((1_No + 1_No) ") * (Y ")) == (- x) * (((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y "))) ) by SURREALR:69, SURREALR:54;
then A25: ((1_No + 1_No) * ((- x) * Y)) * (((1_No + 1_No) ") * (Y ")) == (- x) * (((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y "))) by SURREALO:4;
( ((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y ")) == (((1_No + 1_No) * Y) * ((1_No + 1_No) ")) * (Y ") & (((1_No + 1_No) * Y) * ((1_No + 1_No) ")) * (Y ") == (Y * ((1_No + 1_No) * ((1_No + 1_No) "))) * (Y ") ) by SURREALR:69, SURREALR:54;
then ( ((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y ")) == (Y * ((1_No + 1_No) * ((1_No + 1_No) "))) * (Y ") & (Y * ((1_No + 1_No) * ((1_No + 1_No) "))) * (Y ") == ((1_No + 1_No) * ((1_No + 1_No) ")) * (Y * (Y ")) ) by SURREALR:69, SURREALO:4;
then ( ((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y ")) == ((1_No + 1_No) * ((1_No + 1_No) ")) * (Y * (Y ")) & ((1_No + 1_No) * ((1_No + 1_No) ")) * (Y * (Y ")) == ((1_No + 1_No) * ((1_No + 1_No) ")) * 1_No ) by A16, SURREALR:54, SURREALO:4;
then ((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y ")) == (1_No + 1_No) * ((1_No + 1_No) ") by SURREALO:4;
then ((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y ")) == 1_No by A16, SURREALO:4;
then (- x) * (((1_No + 1_No) * Y) * (((1_No + 1_No) ") * (Y "))) == (- x) * 1_No by SURREALR:54;
then ((1_No + 1_No) * ((- x) * Y)) * (((1_No + 1_No) ") * (Y ")) == (- x) * 1_No by A25, SURREALO:4;
then (y + ((sqrt (Y * Y)) * (sqrt (Y * Y)))) * (((sqrt (Y * Y)) + (sqrt (Y * Y))) ") == - x by A24, SURREALO:4;
hence ( sqrt y < - x & y = [{},{0_No,(((sqrt ((x * x) + 1_No)) - x) * ((sqrt ((x * x) + 1_No)) - x))}] ) by A14, A13, SURREALO:4; :: thesis:

end;

theorem :: SURREALS:32

ex x, y being Surreal st
( x == y & y < 0_No & sqrt x < sqrt y )

proof

consider y being Surreal such that
A1: ( - 1_No == y & sqrt y < - 1_No & y = [{},{0_No,(((sqrt ((1_No * 1_No) + 1_No)) - 1_No) * ((sqrt ((1_No * 1_No) + 1_No)) - 1_No))}] ) by Th31, SURREALI:def 8;
take y ; :: thesis:
take - 1_No ; :: thesis:
- 1_No < - 0_No by SURREALI:def 8, SURREALR:10;
hence ( y == - 1_No & - 1_No < 0_No & sqrt y < sqrt (- 1_No) ) by A1; :: thesis:

end;