SURREALR: The Ring of {C}onway Numbers in {M}izar

for f being Function-yielding c=-monotone Sequence
for A being Ordinal st A in dom f holds
( dom (f . A) c= dom (union (rng f)) & ( for o being object st o in dom (f . A) holds
(f . A) . o = (union (rng f)) . o ) )

proof end;

theorem Th3: :: SURREALR:3

for f being Function-yielding c=-monotone Sequence
for A being Ordinal
for X being set st ( for o being object st o in X holds
ex B being Ordinal st
( o in dom (f . B) & B in A ) ) holds
(union (rng (f | A))) .: X = (union (rng f)) .: X

proof end;

scheme :: SURREALR:sch 1
MonoFvSExists{ F₁() -> Ordinal, F₂( Ordinal) -> set , F₃( object , Function-yielding c=-monotone Sequence) -> object } :

ex S being Function-yielding c=-monotone Sequence st
( dom S = succ F₁() & ( for A being Ordinal st A in succ F₁() holds
ex SA being ManySortedSet of F₂(A) st
( S . A = SA & ( for o being object st o in F₂(A) holds
SA . o = F₃(o,(S | A)) ) ) ) )

provided

A1: for S being Function-yielding c=-monotone Sequence st ( for A being Ordinal st A in dom S holds
dom (S . A) = F₂(A) ) holds
for A being Ordinal
for o being object st o in dom (S . A) holds
F₃(o,(S | A)) = F₃(o,S) and
A2: for A, B being Ordinal st A c= B holds
F₂(A) c= F₂(B)

proof end;

scheme :: SURREALR:sch 2
MonoFvSUniq{ F₁() -> Ordinal, F₂( Ordinal) -> set , F₃() -> Function-yielding c=-monotone Sequence, F₄() -> Function-yielding c=-monotone Sequence, F₅( object , Function-yielding c=-monotone Sequence) -> object } :

F₃() | F₁() = F₄() | F₁()

provided

A1: ( F₁() c= dom F₃() & F₁() c= dom F₄() ) and
A2: for A being Ordinal st A in F₁() holds
ex SA being ManySortedSet of F₂(A) st
( F₃() . A = SA & ( for o being object st o in F₂(A) holds
SA . o = F₅(o,(F₃() | A)) ) ) and
A3: for A being Ordinal st A in F₁() holds
ex SA being ManySortedSet of F₂(A) st
( F₄() . A = SA & ( for o being object st o in F₂(A) holds
SA . o = F₅(o,(F₄() | A)) ) )

proof end;

definition

let A be Ordinal;

func No_opposite_op A -> ManySortedSet of Day A means :Def2: :: SURREALR:def 2
ex S being Function-yielding c=-monotone 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 o being object st o in Day B holds
SB . o = [((union (rng (S | B))) .: (R_ o)),((union (rng (S | B))) .: (L_ o))] ) ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines No_opposite_op SURREALR:def 2 :

theorem Th4: :: SURREALR:4

for S being Function-yielding c=-monotone 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 (rng (S | B))) .: (R_ o)),((union (rng (S | B))) .: (L_ o))] ) ) ) holds
for A being Ordinal st A in dom S holds
No_opposite_op A = S . A

proof end;

theorem Th5: :: SURREALR:5

for A, B being Ordinal
for o being object
for f being Function-yielding c=-monotone Sequence st o in dom (f . B) & B in A holds
( o in dom (union (rng (f | A))) & (union (rng (f | A))) . o = (union (rng f)) . o )

proof end;

theorem Th6: :: SURREALR:6

for o being object
for f being Function-yielding c=-monotone Sequence
for A, B being Ordinal st o in dom (f . B) & B in A holds
(union (rng (f | A))) . o = (union (rng f)) . o

proof end;

definition

let x be Surreal;

func - x -> set equals :: SURREALR:def 3
(No_opposite_op (born x)) . x;

coherence ;

end;

:: deftheorem defines - SURREALR:def 3 :

definition

let X be set ;

func -- X -> set means :Def4: :: SURREALR:def 4
for o being object holds
( o in it iff ex x being Surreal st
( x in X & o = - x ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines -- SURREALR:def 4 :

theorem Th7: :: SURREALR:7

for x being Surreal holds - x = [(-- (R_ x)),(-- (L_ x))]

proof end;

Lm1: for D being Ordinal holds
( ( for x being Surreal st x in Day D holds
( - x is surreal & - x in Day D & ( for x1 being Surreal st x1 = - x holds
- x1 = x ) ) ) & ( for x, x1, y, y1 being Surreal st x in Day D & y in Day D & x1 = - x & y1 = - y holds
( x <= y iff y1 <= x1 ) ) )

proof end;

registration

let x be Surreal;

cluster - x -> surreal ;

coherence

proof end;

end;

registration

let X be set ;

cluster -- X -> surreal-membered ;

coherence

proof end;

end;

theorem Th8: :: SURREALR:8

for x being Surreal holds
( L_ (- x) = -- (R_ x) & R_ (- x) = -- (L_ x) )

proof end;

Conway Ch.1 Th.4(ii)

theorem Th9: :: SURREALR:9

for x being Surreal holds - (- x) = x

proof end;

registration

let x be Surreal;

reduce - (- x) to x;

reducibility by Th9;

end;

theorem Th10: :: SURREALR:10

for x, y being Surreal holds
( x <= y iff - y <= - x )

proof end;

theorem :: SURREALR:11

for x being Surreal
for D being Ordinal st x in Day D holds
- x in Day D by Lm1;

theorem Th12: :: SURREALR:12

for x being Surreal holds born x = born (- x)

proof end;

theorem Th13: :: SURREALR:13

for x being Surreal holds born_eq x = born_eq (- x)

proof end;

theorem :: SURREALR:14

for x, y being Surreal st x in born_eq_set y holds
- x in born_eq_set (- y)

proof end;

theorem Th15: :: SURREALR:15

for X being surreal-membered set holds -- (-- X) = X

proof end;

theorem Th16: :: SURREALR:16

for X being set holds card (-- X) c= card X

proof end;

theorem :: SURREALR:17

for X being surreal-membered set holds card X = card (-- X)

proof end;

Lm2: for X, Y being surreal-membered set st X <<= Y holds
-- Y <<= -- X

proof end;

theorem :: SURREALR:18

for X, Y being surreal-membered set holds
( X <<= Y iff -- Y <<= -- X )

proof end;

Lm3: for X, Y being surreal-membered set st X << Y holds
-- Y << -- X

proof end;

theorem :: SURREALR:19

for X, Y being surreal-membered set holds
( X << Y iff -- Y << -- X )

proof end;

theorem Th20: :: SURREALR:20

for X1, X2 being set holds -- (X1 \/ X2) = (-- X1) \/ (-- X2)

proof end;

theorem Th21: :: SURREALR:21

for x being Surreal holds {(- x)} = -- {x}

proof end;

theorem Th22: :: SURREALR:22

-- {} = {}

proof end;

theorem Th23: :: SURREALR:23

- 0_No = 0_No

proof end;

registration

reduce - 0_No to 0_No ;

reducibility by Th23;

end;

theorem :: SURREALR:24

for x being Surreal holds
( x == 0_No iff - x == 0_No ) by Th23, Th10;

definition

let A be Ordinal;

func Triangle A -> Subset of [:(Day A),(Day A):] means :Def5: :: SURREALR:def 5
for x, y being Surreal holds
( [x,y] in it iff (born x) (+) (born y) c= A );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Triangle SURREALR:def 5 :

registration

let A be Ordinal;

cluster Triangle A -> non empty ;

coherence

proof end;

end;

theorem Th25: :: SURREALR:25

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

proof end;

definition

let A be Ordinal;

func No_sum_op A -> ManySortedSet of Triangle A means :Def6: :: SURREALR:def 6
ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & it = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [((union (rng (S | B))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | B))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] ) ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines No_sum_op SURREALR:def 6 :

theorem Th26: :: SURREALR:26

for S being Function-yielding c=-monotone Sequence st ( for B being Ordinal st B in dom S holds
ex SB being ManySortedSet of Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [((union (rng (S | B))) .: ([:(L_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(L_ (R_ x)):])),((union (rng (S | B))) .: ([:(R_ (L_ x)),{(R_ x)}:] \/ [:{(L_ x)},(R_ (R_ x)):]))] ) ) ) holds
for A being Ordinal st A in dom S holds
No_sum_op A = S . A

proof end;

definition

let x, y be Surreal;

func x + y -> set equals :: SURREALR:def 7
(No_sum_op ((born x) (+) (born y))) . [x,y];

coherence ;

end;

:: deftheorem defines + SURREALR:def 7 :

definition

let X, Y be set ;

func X ++ Y -> set means :Def8: :: SURREALR:def 8
for o being object holds
( o in it iff ex x, y being Surreal st
( x in X & y in Y & o = x + y ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines ++ SURREALR:def 8 :

theorem Th27: :: SURREALR:27

for X being set holds X ++ {} = {}

proof end;

theorem Th28: :: SURREALR:28

for x, y being Surreal holds x + y = [(((L_ x) ++ {y}) \/ ({x} ++ (L_ y))),(((R_ x) ++ {y}) \/ ({x} ++ (R_ y)))]

proof end;

Commutativity of Addition for Surreal Number, Conway Ch.1 Th.3 (ii)

theorem Th29: :: SURREALR:29

for x, y being Surreal holds x + y = y + x

proof end;

definition

let x, y be Surreal;
:: original: +
redefine func x + y -> set ;
commutativity by Th29;

end;

Lm4: for X, Y being set holds X ++ Y c= Y ++ X

proof end;

theorem Th30: :: SURREALR:30

for X, Y being set holds X ++ Y = Y ++ X

proof end;

definition

let X, Y be set ;
:: original: ++
redefine func X ++ Y -> set ;
commutativity by Th30;

end;

Lm5: for D being Ordinal holds
( ( for x, y being Surreal st (born x) (+) (born y) c= D holds
( x + y is surreal & x + y in Day ((born x) (+) (born y)) ) ) & ( for x, y, z, xz, yz being Surreal st (born x) (+) (born z) c= D & (born y) (+) (born z) c= D & xz = x + z & yz = y + z holds
( xz <= yz iff x <= y ) ) )

proof end;

registration

let x, y be Surreal;

cluster x + y -> surreal ;

coherence by Lm5;

end;

definition

let x, y be Surreal;

func x - y -> Surreal equals :: SURREALR:def 9
x + (- y);

coherence ;

end;

:: deftheorem defines - SURREALR:def 9 :

theorem :: SURREALR:31

for x, y being Surreal holds born (x + y) c= (born x) (+) (born y)

proof end;

registration

let X, Y be set ;

cluster X ++ Y -> surreal-membered ;

coherence

proof end;

end;

Transitive Law of Addition for Surreal Number, Conway Ch.1 Th.5

theorem Th32: :: SURREALR:32

for x, y, z being Surreal holds
( x <= y iff x + z <= y + z )

proof end;

theorem Th33: :: SURREALR:33

for X1, X2, Y being set holds (X1 \/ X2) ++ Y = (X1 ++ Y) \/ (X2 ++ Y)

proof end;

theorem :: SURREALR:34

for X, Y1, Y2 being set holds X ++ (Y1 \/ Y2) = (X ++ Y1) \/ (X ++ Y2) by Th33;

theorem :: SURREALR:35

for X1, X2, Y1, Y2 being set st X1 <=_ X2 & Y1 <=_ Y2 holds
X1 ++ Y1 <=_ X2 ++ Y2

proof end;

theorem Th36: :: SURREALR:36

for x, y being Surreal holds {x} ++ {y} = {(x + y)}

proof end;

Associativity of Addition for Surreal Number, Conway Ch.1 Th.3(iii)

theorem Th37: :: SURREALR:37

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

proof end;

Additive Identity for Surreal Number, Conway Ch.1 Th.3(i)

theorem Th38: :: SURREALR:38

for x being Surreal holds x + 0_No = x

proof end;

registration

let x be Surreal;

reduce x + 0_No to x;

reducibility by Th38;

end;

Property of The Aditive Inverse for Surreal Number, Conway Ch.1 Th.4(iii)

theorem Th39: :: SURREALR:39

for x being Surreal holds x - x == 0_No

proof end;

Conway Ch.1 Th.4(i)

theorem Th40: :: SURREALR:40

for x, y being Surreal holds - (x + y) = (- x) + (- y)

proof end;

theorem Th41: :: SURREALR:41

for x, y, z being Surreal holds
( x + y <= z iff x <= z - y )

proof end;

theorem Th42: :: SURREALR:42

for x, y, z being Surreal holds
( x + y < z iff x < z - y )

proof end;

theorem Th43: :: SURREALR:43

for x, y, z, t being Surreal st x <= y & z <= t holds
x + z <= y + t

proof end;

theorem Th44: :: SURREALR:44

for x, y, z, t being Surreal st x <= y & z < t holds
x + z < y + t

proof end;

theorem :: SURREALR:45

for x, y being Surreal holds
( x < y iff 0_No < y - x )

proof end;

theorem :: SURREALR:46

for x, y being Surreal holds
( x < y iff x - y < 0_No )

proof end;

theorem :: SURREALR:47

for x, y being Surreal st x - y == 0_No holds
x == y

proof end;

definition

let x be object ;
assume A1: x is surreal ;

func -' x -> Surreal means :Def10: :: SURREALR:def 10
for x1 being Surreal st x1 = x holds
it = - x1;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines -' SURREALR:def 10 :

registration

let a be Surreal;
let x be object ;

identify - a with -' x when a = x;

compatibility by Def10;

end;

definition

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

func x +' y -> Surreal means :Def11: :: SURREALR:def 11
for x1, y1 being Surreal st x1 = x & y1 = y holds
it = x1 + y1;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines +' SURREALR:def 11 :

registration

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

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

compatibility by Def11;

end;

definition

let A be Ordinal;

func No_mult_op A -> ManySortedSet of Triangle A means :Def12: :: SURREALR:def 12
ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & it = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xL,yL]))) where xL is Element of L_ (L_ x), yL is Element of L_ (R_ x) : ( xL in L_ (L_ x) & yL in L_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xR,yR]))) where xR is Element of R_ (L_ x), yR is Element of R_ (R_ x) : ( xR in R_ (L_ x) & yR in R_ (R_ x) ) } ),( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xL,yR]))) where xL is Element of L_ (L_ x), yR is Element of R_ (R_ x) : ( xL in L_ (L_ x) & yR in R_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xR,yL]))) where xR is Element of R_ (L_ x), yL is Element of L_ (R_ x) : ( xR in R_ (L_ x) & yL in L_ (R_ x) ) } )] ) ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines No_mult_op SURREALR:def 12 :

definition

let x, y be Surreal;

func x * y -> set equals :: SURREALR:def 13
(No_mult_op ((born x) (+) (born y))) . [x,y];

coherence ;

end;

:: deftheorem defines * SURREALR:def 13 :

theorem Th48: :: SURREALR:48

for S being Function-yielding c=-monotone Sequence st ( for B being Ordinal st B in dom S holds
ex SB being ManySortedSet of Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xL,yL]))) where xL is Element of L_ (L_ x), yL is Element of L_ (R_ x) : ( xL in L_ (L_ x) & yL in L_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xR,yR]))) where xR is Element of R_ (L_ x), yR is Element of R_ (R_ x) : ( xR in R_ (L_ x) & yR in R_ (R_ x) ) } ),( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xL,yR]))) where xL is Element of L_ (L_ x), yR is Element of R_ (R_ x) : ( xL in L_ (L_ x) & yR in R_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xR,yL]))) where xR is Element of R_ (L_ x), yL is Element of L_ (R_ x) : ( xR in R_ (L_ x) & yL in L_ (R_ x) ) } )] ) ) ) holds
for A being Ordinal st A in dom S holds
No_mult_op A = S . A

proof end;

definition

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

func comp (X,x,y,Y) -> set means :Def14: :: SURREALR:def 14
for o being object holds
( o in it iff ex x1, y1 being Surreal st
( o = ((x1 * y) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in Y ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines comp SURREALR:def 14 :

theorem Th49: :: SURREALR:49

for x, y being Surreal
for X being set holds comp (X,x,y,{}) = {}

proof end;

theorem Th50: :: SURREALR:50

for x, y being Surreal holds x * y = [((comp ((L_ x),x,y,(L_ y))) \/ (comp ((R_ x),x,y,(R_ y)))),((comp ((L_ x),x,y,(R_ y))) \/ (comp ((R_ x),x,y,(L_ y))))]

proof end;

theorem Th51: :: SURREALR:51

( ( for x, y being Surreal holds x * y is Surreal ) & ( for x, y being Surreal holds x * y = y * x ) & ( for x1, x2, y, x1y, x2y being Surreal st x1 == x2 & x1y = x1 * y & x2y = x2 * y holds
x1y == x2y ) & ( for x1, x2, y1, y2, x1y2, x2y1, x1y1, x2y2 being Surreal st x1y1 = x1 * y1 & x1y2 = x1 * y2 & x2y1 = x2 * y1 & x2y2 = x2 * y2 & x1 < x2 & y1 < y2 holds
x1y2 + x2y1 < x1y1 + x2y2 ) )

proof end;

registration

let a, b be Surreal;

cluster a * b -> surreal ;

coherence by Th51;

end;

Commutativity of Multiplication for Surreal Number, Conway Ch.1 Th.7(iii)

definition

let a, b be Surreal;
:: original: *
redefine func a * b -> set ;
commutativity by Th51;

end;

registration

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

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

coherence

proof end;

end;

definition

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

redefine func comp (X,x,y,Y) means :Def15: :: SURREALR:def 15
for o being object holds
( o in it iff ex x1, y1 being Surreal st
( o = ((x1 * y) + (x * y1)) - (x1 * y1) & x1 in X & y1 in Y ) );

compatibility

proof end;

end;

:: deftheorem Def15 defines comp SURREALR:def 15 :

theorem :: SURREALR:52

for x, y, z, t being Surreal holds comp ({z},x,y,{t}) = {(((z * y) + (x * t)) - (z * t))}

proof end;

Lm6: for x, y being Surreal
for X, Y being set holds comp (X,x,y,Y) c= comp (Y,y,x,X)

proof end;

theorem Th53: :: SURREALR:53

for x, y being Surreal
for X, Y being set holds comp (X,x,y,Y) = comp (Y,y,x,X)

proof end;

Conway Ch.1 Th.8(i)

theorem :: SURREALR:54

for x1, x2, y being Surreal st x1 == x2 holds
x1 * y == x2 * y by Th51;

Conway Ch.1 Th.8(iii)

theorem :: SURREALR:55

for x1, x2, y1, y2 being Surreal st x1 < x2 & y1 < y2 holds
(x1 * y2) + (x2 * y1) < (x1 * y1) + (x2 * y2) by Th51;

Conway Ch.1 Th.7(i)

theorem Th56: :: SURREALR:56

for x being Surreal holds x * 0_No = 0_No

proof end;

Multiplicative Identity for Surreal Number, Conway Ch.1 Th.7(ii)

theorem Th57: :: SURREALR:57

for x being Surreal holds x * 1_No = x

proof end;

registration

let x be Surreal;

reduce x * 0_No to 0_No ;

reducibility by Th56;

reduce x * 1_No to x;

reducibility by Th57;

end;

Lm7: for x, y, z being Surreal
for X, Y, Z being surreal-membered set st ( X = L_ x or X = R_ x or X = {x} ) & ( Y = L_ y or Y = R_ y or Y = {y} ) & ( Z = L_ z or Z = R_ z or Z = {z} ) & ( X <> {x} or Y <> {y} or Z <> {z} ) holds
for x1, y1, z1 being Surreal st x1 in X & y1 in Y & z1 in Z holds
((born x1) (+) (born y1)) (+) (born z1) in ((born x) (+) (born y)) (+) (born z)

proof end;