:: Inverse Element for Surreal Number
:: by Karol P\kak
::
:: Received October 22, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

definition

let x, y be object ;
assume A1: ( x is surreal & y is surreal ) ;

func x *' y -> Surreal means :Def1: :: SURREALI:def 1
for x1, y1 being Surreal st x1 = x & y1 = y holds
it = x1 * y1;

existence
ex b₁ being Surreal st
for x1, y1 being Surreal st x1 = x & y1 = y holds
b₁ = x1 * y1

proof end;

uniqueness
for b₁, b₂ being Surreal st ( for x1, y1 being Surreal st x1 = x & y1 = y holds
b₁ = x1 * y1 ) & ( for x1, y1 being Surreal st x1 = x & y1 = y holds
b₂ = x1 * y1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines *' SURREALI:def 1 :
for x, y being object st x is surreal & y is surreal holds
for b₃ being Surreal holds
( b₃ = x *' y iff for x1, y1 being Surreal st x1 = x & y1 = y holds
b₃ = x1 * y1 );

definition

let lamb, x be object ;
let X be set ;
let Inv be Function;

func divs (lamb,x,X,Inv) -> set means :Def2: :: SURREALI:def 2
for o being object holds
( o in it iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) );

existence
ex b₁ being set st
for o being object holds
( o in b₁ iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for o being object holds
( o in b₁ iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) ) & ( for o being object holds
( o in b₂ iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines divs SURREALI:def 2 :
for lamb, x being object
for X being set
for Inv being Function
for b₅ being set holds
( b₅ = divs (lamb,x,X,Inv) iff for o being object holds
( o in b₅ iff ex xL being object st
( xL in X & xL <> 0_No & o = (1_No +' ((xL +' (-' x)) *' lamb)) *' (Inv . xL) ) ) );

definition

let Lamb be set ;
let x be object ;
let X be set ;
let Inv be Function;

func divset (Lamb,x,X,Inv) -> set means :Def3: :: SURREALI:def 3
for o being object holds
( o in it iff ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) );

existence
ex b₁ being set st
for o being object holds
( o in b₁ iff ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for o being object holds
( o in b₁ iff ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) ) ) & ( for o being object holds
( o in b₂ iff ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines divset SURREALI:def 3 :
for Lamb being set
for x being object
for X being set
for Inv being Function
for b₅ being set holds
( b₅ = divset (Lamb,x,X,Inv) iff for o being object holds
( o in b₅ iff ex lamb being object st
( lamb in Lamb & o in divs (lamb,x,X,Inv) ) ) );

definition

let x be object ;
let Inv be Function;

func transitions_of (x,Inv) -> Function means :Def4: :: SURREALI:def 4
( dom it = NAT & it . 0 = 1_No & ( for k being Nat holds
( it . k is pair & (it . (k + 1)) `1 = ((L_ (it . k)) \/ (divset ((L_ (it . k)),x,(R_ x),Inv))) \/ (divset ((R_ (it . k)),x,(L_ x),Inv)) & (it . (k + 1)) `2 = ((R_ (it . k)) \/ (divset ((L_ (it . k)),x,(L_ x),Inv))) \/ (divset ((R_ (it . k)),x,(R_ x),Inv)) ) ) );

existence
ex b₁ being Function st
( dom b₁ = NAT & b₁ . 0 = 1_No & ( for k being Nat holds
( b₁ . k is pair & (b₁ . (k + 1)) `1 = ((L_ (b<sub>1</sub> . k)) \/ (divset ((L_ (b<sub>1</sub> . k)),x,(R_ x),Inv))) \/ (divset ((R_ (b<sub>1</sub> . k)),x,(L_ x),Inv)) & (b<sub>1</sub> . (k + 1)) `2 = ((R_ (b₁ . k)) \/ (divset ((L_ (b₁ . k)),x,(L_ x),Inv))) \/ (divset ((R_ (b₁ . k)),x,(R_ x),Inv)) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = NAT & b₁ . 0 = 1_No & ( for k being Nat holds
( b₁ . k is pair & (b₁ . (k + 1)) `1 = ((L_ (b<sub>1</sub> . k)) \/ (divset ((L_ (b<sub>1</sub> . k)),x,(R_ x),Inv))) \/ (divset ((R_ (b<sub>1</sub> . k)),x,(L_ x),Inv)) & (b<sub>1</sub> . (k + 1)) `2 = ((R_ (b₁ . k)) \/ (divset ((L_ (b₁ . k)),x,(L_ x),Inv))) \/ (divset ((R_ (b₁ . k)),x,(R_ x),Inv)) ) ) & dom b₂ = NAT & b₂ . 0 = 1_No & ( for k being Nat holds
( b₂ . k is pair & (b₂ . (k + 1)) `1 = ((L_ (b<sub>2</sub> . k)) \/ (divset ((L_ (b<sub>2</sub> . k)),x,(R_ x),Inv))) \/ (divset ((R_ (b<sub>2</sub> . k)),x,(L_ x),Inv)) & (b<sub>2</sub> . (k + 1)) `2 = ((R_ (b₂ . k)) \/ (divset ((L_ (b₂ . k)),x,(L_ x),Inv))) \/ (divset ((R_ (b₂ . k)),x,(R_ x),Inv)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines transitions_of SURREALI:def 4 :
for x being object
for Inv, b₃ being Function holds
( b₃ = transitions_of (x,Inv) iff ( dom b₃ = NAT & b₃ . 0 = 1_No & ( for k being Nat holds
( b₃ . k is pair & (b₃ . (k + 1)) `1 = ((L_ (b<sub>3</sub> . k)) \/ (divset ((L_ (b<sub>3</sub> . k)),x,(R_ x),Inv))) \/ (divset ((R_ (b<sub>3</sub> . k)),x,(L_ x),Inv)) & (b<sub>3</sub> . (k + 1)) `2 = ((R_ (b₃ . k)) \/ (divset ((L_ (b₃ . k)),x,(L_ x),Inv))) \/ (divset ((R_ (b₃ . k)),x,(R_ x),Inv)) ) ) ) );

definition

let x be object ;
let Inv be Function;

func divL (x,Inv) -> Function means :Def5: :: SURREALI:def 5
( dom it = NAT & ( for k being Nat holds it . k = ((transitions_of (x,Inv)) . k) `1 ) );

existence
ex b₁ being Function st
( dom b₁ = NAT & ( for k being Nat holds b₁ . k = ((transitions_of (x,Inv)) . k) `1 ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = NAT & ( for k being Nat holds b₁ . k = ((transitions_of (x,Inv)) . k) `1 ) & dom b<sub>2</sub> = NAT & ( for k being Nat holds b<sub>2</sub> . k = ((transitions_of (x,Inv)) . k) `1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines divL SURREALI:def 5 :
for x being object
for Inv, b₃ being Function holds
( b₃ = divL (x,Inv) iff ( dom b₃ = NAT & ( for k being Nat holds b₃ . k = ((transitions_of (x,Inv)) . k) `1 ) ) );

definition

let x be object ;
let Inv be Function;

func divR (x,Inv) -> Function means :Def6: :: SURREALI:def 6
( dom it = NAT & ( for k being Nat holds it . k = ((transitions_of (x,Inv)) . k) `2 ) );

existence
ex b₁ being Function st
( dom b₁ = NAT & ( for k being Nat holds b₁ . k = ((transitions_of (x,Inv)) . k) `2 ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = NAT & ( for k being Nat holds b₁ . k = ((transitions_of (x,Inv)) . k) `2 ) & dom b<sub>2</sub> = NAT & ( for k being Nat holds b<sub>2</sub> . k = ((transitions_of (x,Inv)) . k) `2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines divR SURREALI:def 6 :
for x being object
for Inv, b₃ being Function holds
( b₃ = divR (x,Inv) iff ( dom b₃ = NAT & ( for k being Nat holds b₃ . k = ((transitions_of (x,Inv)) . k) `2 ) ) );

registration

let a, b be Surreal;
let x, y be object ;

identify a * b with x *' y when a = x, b = y;

compatibility
( a = x & b = y implies a * b = x *' y ) by Def1;

end;

theorem Th1: :: SURREALI:1

for o being object
for Inv being Function holds
( (divL (o,Inv)) . 0 = {0_No} & (divR (o,Inv)) . 0 = {} )

proof end;

theorem :: SURREALI:2

for n, m being Nat
for o being object
for Inv being Function st n <= m holds
( (divL (o,Inv)) . n c= (divL (o,Inv)) . m & (divR (o,Inv)) . n c= (divR (o,Inv)) . m )

proof end;

definition

let X be set ;
let f be Function;

attr f is X -surreal-valued means :: SURREALI:def 7
for o being object st o in X holds
f . o is Surreal;

end;

:: deftheorem defines -surreal-valued SURREALI:def 7 :
for X being set
for f being Function holds
( f is X -surreal-valued iff for o being object st o in X holds
f . o is Surreal );

theorem :: SURREALI:3

for X, Y being set
for Inv being Function st Inv is Y -surreal-valued & X c= Y holds
Inv is X -surreal-valued ;

theorem Th4: :: SURREALI:4

for x, y being Surreal
for X being set
for Inv being Function holds divs (y,x,X,Inv) is surreal-membered

proof end;

theorem Th5: :: SURREALI:5

for x being Surreal
for X, Y being set
for Inv being Function st Y is surreal-membered & X is surreal-membered & Inv is X -surreal-valued holds
divset (Y,x,X,Inv) is surreal-membered

proof end;

theorem Th6: :: SURREALI:6

for n being Nat
for o being object
for Inv being Function holds
( (divL (o,Inv)) . (n + 1) = (((divL (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(R_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(L_ o),Inv)) & (divR (o,Inv)) . (n + 1) = (((divR (o,Inv)) . n) \/ (divset (((divL (o,Inv)) . n),o,(L_ o),Inv))) \/ (divset (((divR (o,Inv)) . n),o,(R_ o),Inv)) )

proof end;

theorem Th7: :: SURREALI:7

for o being object
for x being Surreal
for X being set
for Inv being Function holds divs (o,x,X,Inv) = divs (o,x,(X \ {0_No}),Inv)

proof end;

theorem Th8: :: SURREALI:8

for x being Surreal
for X, Y being set
for Inv being Function holds divset (Y,x,X,Inv) = divset (Y,x,(X \ {0_No}),Inv)

proof end;

theorem Th9: :: SURREALI:9

for n being Nat
for x being Surreal
for Inv being Function st Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued holds
( (divL (x,Inv)) . n is surreal-membered & (divR (x,Inv)) . n is surreal-membered )

proof end;

theorem Th10: :: SURREALI:10

for x being Surreal
for Inv being Function st Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued holds
( Union (divL (x,Inv)) is surreal-membered & Union (divR (x,Inv)) is surreal-membered )

proof end;

theorem Th11: :: SURREALI:11

for x being Surreal
for X, Y, Z being set
for Inv being Function st Y c= Z holds
divset (Y,x,X,Inv) c= divset (Z,x,X,Inv)

proof end;

theorem Th12: :: SURREALI:12

for x being Surreal
for Inv being Function holds Union (divL (x,Inv)) = ({0_No} \/ (divset ((Union (divL (x,Inv))),x,(R_ x),Inv))) \/ (divset ((Union (divR (x,Inv))),x,(L_ x),Inv))

proof end;

theorem Th13: :: SURREALI:13

for x being Surreal
for Inv being Function holds Union (divR (x,Inv)) = (divset ((Union (divL (x,Inv))),x,(L_ x),Inv)) \/ (divset ((Union (divR (x,Inv))),x,(R_ x),Inv))

proof end;

theorem Th14: :: SURREALI:14

for a, b being object
for X, Z being set
for I1, I2 being Function st X \ {0_No} c= Z & I1 | Z = I2 | Z holds
divs (a,b,X,I1) = divs (a,b,X,I2)

proof end;

theorem Th15: :: SURREALI:15

for o being object
for X, Y, Z being set
for I1, I2 being Function st X \ {0_No} c= Z & I1 | Z = I2 | Z holds
divset (Y,o,X,I1) = divset (Y,o,X,I2)

proof end;

theorem Th16: :: SURREALI:16

for Z being set
for I1, I2 being Function
for x being object st ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z holds
transitions_of (x,I1) = transitions_of (x,I2)

proof end;

theorem Th17: :: SURREALI:17

for Z being set
for I1, I2 being Function
for x being object st ((L_ x) \/ (R_ x)) \ {0_No} c= Z & I1 | Z = I2 | Z holds
( divL (x,I1) = divL (x,I2) & divR (x,I1) = divR (x,I2) )

proof end;

definition

let x be Surreal;

attr x is positive means :Def8: :: SURREALI:def 8
0_No < x;

end;

:: deftheorem Def8 defines positive SURREALI:def 8 :
for x being Surreal holds
( x is positive iff 0_No < x );

registration

cluster 1_No -> positive ;

coherence
1_No is positive

proof end;

end;

registration

cluster non empty pair surreal positive for set ;

existence
ex b₁ being Surreal st b₁ is positive

proof end;

end;

registration

let x, y be positive Surreal;

cluster x + y -> positive ;

coherence
x + y is positive

proof end;

cluster x * y -> positive ;

coherence
x * y is positive

proof end;

end;

Lm1: for x being Surreal st 0_No < x holds
ex y being Surreal st
( y == x & ( for z being Surreal holds
( z in L_ y iff ( z = 0_No or ( z in L_ x & 0_No < z ) ) ) ) & ( for z being Surreal holds
( z in R_ y iff ( z in R_ x & 0_No < z ) ) ) )

proof end;

definition

let x be object ;
assume A1: x is positive Surreal ;

func ||.x.|| -> positive Surreal means :Def9: :: SURREALI:def 9
for y being Surreal holds
( ( not y in L_ it or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ it ) & ( y in R_ it implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ it ) );

existence
ex b₁ being positive Surreal st
for y being Surreal holds
( ( not y in L_ b₁ or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ b₁ ) & ( y in R_ b₁ implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ b₁ ) )

proof end;

uniqueness
for b₁, b₂ being positive Surreal st ( for y being Surreal holds
( ( not y in L_ b₁ or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ b₁ ) & ( y in R_ b₁ implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ b₁ ) ) ) & ( for y being Surreal holds
( ( not y in L_ b₂ or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ b₂ ) & ( y in R_ b₂ implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ b₂ ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines ||. SURREALI:def 9 :
for x being object st x is positive Surreal holds
for b₂ being positive Surreal holds
( b₂ = ||.x.|| iff for y being Surreal holds
( ( not y in L_ b₂ or y = 0_No or ( y in L_ x & y is positive ) ) & ( ( y = 0_No or ( y in L_ x & y is positive ) ) implies y in L_ b₂ ) & ( y in R_ b₂ implies ( y in R_ x & y is positive ) ) & ( y in R_ x & y is positive implies y in R_ b₂ ) ) );

theorem Th18: :: SURREALI:18

for x being Surreal st x is positive holds
x == ||.x.||

proof end;

theorem :: SURREALI:19

for x being Surreal st x is positive holds
||.||.x.||.|| = ||.x.||

proof end;

theorem Th20: :: SURREALI:20

for x being Surreal st x is positive holds
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x)

proof end;

theorem Th21: :: SURREALI:21

for x, y being Surreal st x is positive & y in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} holds
y is positive

proof end;

theorem Th22: :: SURREALI:22

for x being Surreal st x is positive holds
born ||.x.|| c= born x

proof end;

definition

let A be Ordinal;

func Positives A -> Subset of (Day A) means :Def10: :: SURREALI:def 10
for x being Surreal holds
( x in it iff ( x in Day A & 0_No < x ) );

existence
ex b₁ being Subset of (Day A) st
for x being Surreal holds
( x in b₁ iff ( x in Day A & 0_No < x ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (Day A) st ( for x being Surreal holds
( x in b₁ iff ( x in Day A & 0_No < x ) ) ) & ( for x being Surreal holds
( x in b₂ iff ( x in Day A & 0_No < x ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines Positives SURREALI:def 10 :
for A being Ordinal
for b₂ being Subset of (Day A) holds
( b₂ = Positives A iff for x being Surreal holds
( x in b₂ iff ( x in Day A & 0_No < x ) ) );

theorem Th23: :: SURREALI:23

for A, B being Ordinal st A c= B holds
Positives A c= Positives B

proof end;

theorem Th24: :: SURREALI:24

for x being Surreal st x is positive holds
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= Positives (born x)

proof end;

definition

let A be Ordinal;

func No_inverse_op A -> ManySortedSet of Positives A means :Def11: :: SURREALI:def 11
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 Positives B st
( S . B = SB & ( for x being object st x in Positives B holds
SB . x = [(Union (divL (||.x.||,(union (rng (S | B)))))),(Union (divR (||.x.||,(union (rng (S | B))))))] ) ) ) );

existence
ex b₁ being ManySortedSet of Positives A ex S being c=-monotone Function-yielding Sequence st
( dom S = succ A & b₁ = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for x being object st x in Positives B holds
SB . x = [(Union (divL (||.x.||,(union (rng (S | B)))))),(Union (divR (||.x.||,(union (rng (S | B))))))] ) ) ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of Positives A st ex S being c=-monotone Function-yielding Sequence st
( dom S = succ A & b₁ = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for x being object st x in Positives B holds
SB . x = [(Union (divL (||.x.||,(union (rng (S | B)))))),(Union (divR (||.x.||,(union (rng (S | B))))))] ) ) ) ) & ex S being c=-monotone Function-yielding Sequence st
( dom S = succ A & b₂ = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for x being object st x in Positives B holds
SB . x = [(Union (divL (||.x.||,(union (rng (S | B)))))),(Union (divR (||.x.||,(union (rng (S | B))))))] ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines No_inverse_op SURREALI:def 11 :
for A being Ordinal
for b₂ being ManySortedSet of Positives A holds
( b₂ = No_inverse_op A iff ex S being c=-monotone Function-yielding Sequence st
( dom S = succ A & b₂ = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for x being object st x in Positives B holds
SB . x = [(Union (divL (||.x.||,(union (rng (S | B)))))),(Union (divR (||.x.||,(union (rng (S | B))))))] ) ) ) ) );

theorem Th25: :: SURREALI:25

for S being c=-monotone Function-yielding Sequence st ( for B being Ordinal st B in dom S holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for o being object st o in Positives B holds
SB . o = [(Union (divL (||.o.||,(union (rng (S | B)))))),(Union (divR (||.o.||,(union (rng (S | B))))))] ) ) ) holds
for A being Ordinal st A in dom S holds
No_inverse_op A = S . A

proof end;

definition

let x be Surreal;

func inv x -> object equals :: SURREALI:def 12
(No_inverse_op (born x)) . x;

coherence
(No_inverse_op (born x)) . x is object ;

end;

:: deftheorem defines inv SURREALI:def 12 :
for x being Surreal holds inv x = (No_inverse_op (born x)) . x;

definition

let x be Surreal;

func No_inverses_on x -> Function means :Def13: :: SURREALI:def 13
( dom it = ((L_ x) \/ (R_ x)) \ {0_No} & ( for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
it . y = inv y ) );

existence
ex b₁ being Function st
( dom b₁ = ((L_ x) \/ (R_ x)) \ {0_No} & ( for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
b₁ . y = inv y ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = ((L_ x) \/ (R_ x)) \ {0_No} & ( for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
b₁ . y = inv y ) & dom b₂ = ((L_ x) \/ (R_ x)) \ {0_No} & ( for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
b₂ . y = inv y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines No_inverses_on SURREALI:def 13 :
for x being Surreal
for b₂ being Function holds
( b₂ = No_inverses_on x iff ( dom b₂ = ((L_ x) \/ (R_ x)) \ {0_No} & ( for y being Surreal st y in ((L_ x) \/ (R_ x)) \ {0_No} holds
b₂ . y = inv y ) ) );

theorem Th26: :: SURREALI:26

for x being Surreal
for Inv being Function st x is positive & No_inverses_on ||.x.|| c= Inv holds
inv x = [(Union (divL (||.x.||,Inv))),(Union (divR (||.x.||,Inv)))]

proof end;

theorem Th27: :: SURREALI:27

for y being Surreal
for f being Function st dom f = NAT & y in Union f holds
ex n being Nat st
( y in f . n & ( for m being Nat st y in f . m holds
n <= m ) )

proof end;

theorem Th28: :: SURREALI:28

for x, y, x1, x1R, y1, y1R being Surreal st 0_No < x1 & x1 * x1R == 1_No & 0_No < y1 & y1 * y1R == 1_No & x * y1 < y * x1 holds
x * x1R < y * y1R

proof end;

theorem Th29: :: SURREALI:29

for x, x1, x2, y1, y2 being Surreal holds
( ((1_No + ((x2 - x) * y2)) * x1) + (- ((1_No + ((x1 - x) * y1)) * x2)) == ((x1 - x2) * (1_No - (x * y1))) + (((y1 - y2) * x1) * (x - x2)) & ((1_No + ((x2 - x) * y2)) * x1) - ((1_No + ((x1 - x) * y1)) * x2) == ((x1 - x2) * (1_No - (x * y2))) + (((y2 - y1) * x2) * (x1 - x)) )

proof end;

theorem Th30: :: SURREALI:30

for x, y, x1, y1, Ix1 being Surreal st x1 * Ix1 == 1_No holds
((x1 * y) + (x * y1)) - (x1 * y1) == 1_No + (x1 * (y - ((1_No + ((x1 - x) * y1)) * Ix1)))

proof end;

Lm2: for x being Surreal st x is positive holds
( inv x is surreal & ( for y being Surreal st y = inv x holds
x * y == 1_No ) )

proof end;

registration

let x be positive Surreal;

cluster inv x -> surreal ;

coherence
inv x is surreal by Lm2;

end;

theorem :: SURREALI:31

for x being Surreal st x is positive holds
inv x is Surreal ;

theorem :: SURREALI:32

for x, y being Surreal st x is positive & y = inv x holds
x * y == 1_No by Lm2;

definition

let x be Surreal;
assume A1: not x == 0_No ;

func x " -> Surreal means :Def14: :: SURREALI:def 14
it = inv x if x is positive
otherwise - it = inv (- x);

existence
( ( x is positive implies ex b₁ being Surreal st b₁ = inv x ) & ( not x is positive implies ex b₁ being Surreal st - b₁ = inv (- x) ) )

proof end;

uniqueness
for b₁, b₂ being Surreal holds
( ( x is positive & b₁ = inv x & b₂ = inv x implies b₁ = b₂ ) & ( not x is positive & - b₁ = inv (- x) & - b₂ = inv (- x) implies b₁ = b₂ ) )

proof end;

correctness
consistency
for b₁ being Surreal holds verum;
;

end;

:: deftheorem Def14 defines " SURREALI:def 14 :
for x being Surreal st not x == 0_No holds
for b₂ being Surreal holds
( ( x is positive implies ( b₂ = x " iff b₂ = inv x ) ) & ( not x is positive implies ( b₂ = x " iff - b₂ = inv (- x) ) ) );

theorem Th33: :: SURREALI:33

for x being Surreal st not x == 0_No holds
x * (x ") == 1_No

proof end;

definition

let X, Y be set ;
let x be Surreal;

func divset (X,x,Y) -> set means :Def15: :: SURREALI:def 15
for o being object holds
( o in it iff ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) );

existence
ex b₁ being set st
for o being object holds
( o in b₁ iff ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for o being object holds
( o in b₁ iff ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) ) ) & ( for o being object holds
( o in b₂ iff ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines divset SURREALI:def 15 :
for X, Y being set
for x being Surreal
for b₄ being set holds
( b₄ = divset (X,x,Y) iff for o being object holds
( o in b₄ iff ex x1, y1 being Surreal st
( 0_No < x1 & x1 in X & y1 in Y & o = (1_No + ((x1 - x) * y1)) * (x1 ") ) ) );

registration

let X, Y be set ;
let x be Surreal;

cluster divset (X,x,Y) -> surreal-membered ;

coherence
divset (X,x,Y) is surreal-membered

proof end;

end;

theorem Th34: :: SURREALI:34

for x being Surreal
for X, nX being set
for Y being surreal-membered set st x is positive & ( ( X = L_ x & nX = L_ ||.x.|| ) or ( X = R_ x & nX = R_ ||.x.|| ) ) holds
divset (X,||.x.||,Y) = divset (Y,||.x.||,nX,(No_inverses_on ||.x.||))

proof end;

theorem Th35: :: SURREALI:35

for x, y being Surreal
for X, Y being set st x == y holds
divset (X,x,Y) <=_ divset (X,y,Y)

proof end;

theorem Th36: :: SURREALI:36

for x being Surreal st x is positive holds
x " = [(({0_No} \/ (divset ((R_ x),||.x.||,(L_ (x "))))) \/ (divset ((L_ x),||.x.||,(R_ (x "))))),((divset ((L_ x),||.x.||,(L_ (x ")))) \/ (divset ((R_ x),||.x.||,(R_ (x ")))))]

proof end;

theorem Th37: :: SURREALI:37

for X1, X2, Y1, Y2 being surreal-membered set st X2 <=_ X1 & Y2 <=_ Y1 & [X1,Y1] is surreal holds
[X2,Y2] is surreal

proof end;

theorem :: SURREALI:38

for x being Surreal st x is positive holds
[(({0_No} \/ (divset ((R_ x),x,(L_ (x "))))) \/ (divset ((L_ x),x,(R_ (x "))))),((divset ((L_ x),x,(L_ (x ")))) \/ (divset ((R_ x),x,(R_ (x ")))))] is Surreal

proof end;

theorem :: SURREALI:39

for x, y being Surreal st x is positive & y = [(({0_No} \/ (divset ((R_ x),x,(L_ (x "))))) \/ (divset ((L_ x),x,(R_ (x "))))),((divset ((L_ x),x,(L_ (x ")))) \/ (divset ((R_ x),x,(R_ (x ")))))] holds
x " == y

proof end;

theorem Th40: :: SURREALI:40

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

proof end;

registration

let x be positive Surreal;

cluster x " -> positive ;

coherence
x " is positive

proof end;

end;

theorem Lm3: :: SURREALI:41

for x, y being Surreal holds
( x * y == 0_No iff ( x == 0_No or y == 0_No ) ) by SURREALR:72, SURREALR:74;

theorem Th41: :: SURREALI:42

for x, y being Surreal st not x == 0_No & x * y == 1_No holds
y == x "

proof end;

theorem :: SURREALI:43

for x, y being Surreal st not 0_No == x & x == y holds
x " == y "

proof end;

theorem :: SURREALI:44

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

proof end;

theorem :: SURREALI:45

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

proof end;