:: Surreal Dyadic and Real Numbers: A Formal Construction
:: by Karol P\kak
::
:: Received April 10, 2025
:: Copyright (c) 2025 Association of Mizar Users

definition

func uInt -> ManySortedSet of INT means :Def1: :: SURREALN:def 1
for n being Nat holds
( it . 0 = 0_No & it . (n + 1) = [{(it . n)},{}] & it . (- (n + 1)) = [{},{(it . (- n))}] );

existence
ex b₁ being ManySortedSet of INT st
for n being Nat holds
( b₁ . 0 = 0_No & b₁ . (n + 1) = [{(b₁ . n)},{}] & b₁ . (- (n + 1)) = [{},{(b₁ . (- n))}] )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of INT st ( for n being Nat holds
( b₁ . 0 = 0_No & b₁ . (n + 1) = [{(b₁ . n)},{}] & b₁ . (- (n + 1)) = [{},{(b₁ . (- n))}] ) ) & ( for n being Nat holds
( b₂ . 0 = 0_No & b₂ . (n + 1) = [{(b₂ . n)},{}] & b₂ . (- (n + 1)) = [{},{(b₂ . (- n))}] ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines uInt SURREALN:def 1 :
for b₁ being ManySortedSet of INT holds
( b₁ = uInt iff for n being Nat holds
( b₁ . 0 = 0_No & b₁ . (n + 1) = [{(b₁ . n)},{}] & b₁ . (- (n + 1)) = [{},{(b₁ . (- n))}] ) );

theorem Th1: :: SURREALN:1

for n being Nat holds
( uInt . n in Day n & uInt . (- n) in Day n )

proof end;

registration

let i be Integer;

cluster uInt . i -> surreal ;

coherence
uInt . i is surreal

proof end;

end;

Lm1: for n being Nat holds uInt . n < uInt . (n + 1)

proof end;

Lm2: for n being Nat holds uInt . (- (n + 1)) < uInt . (- n)

proof end;

theorem Th2: :: SURREALN:2

for x being Surreal
for n being Nat st x in Day n holds
( uInt . (- n) <= x & x <= uInt . n )

proof end;

theorem Th3: :: SURREALN:3

for i, j being Integer st i < j holds
uInt . i < uInt . j

proof end;

registration

let n be positive Nat;

cluster uInt . n -> positive ;

coherence
uInt . n is positive

proof end;

end;

theorem Th4: :: SURREALN:4

for n being Nat holds
( n = born (uInt . n) & n = born (uInt . (- n)) )

proof end;

theorem Th5: :: SURREALN:5

for n being Nat holds
( born_eq (uInt . n) = n & born_eq (uInt . (- n)) = n )

proof end;

theorem :: SURREALN:6

for n being Nat holds 0_No <= uInt . n

proof end;

theorem Th7: :: SURREALN:7

for n being Nat holds
( L_ (uInt . (- n)) = {} & {} = R_ (uInt . n) )

proof end;

registration

let i be Integer;

cluster uInt . i -> uniq-surreal ;

coherence
uInt . i is uniq-surreal

proof end;

end;

Lm3: for n being Nat
for i being Integer st - n < i & i < n holds
( uInt . (- n) < uInt . i & uInt . i < uInt . n )

proof end;

Lm4: for i, j being Integer st i < j holds
uInt . i < uInt . j

proof end;

theorem :: SURREALN:8

for i, j being Integer st uInt . i = uInt . j holds
i = j

proof end;

theorem Th9: :: SURREALN:9

for i, j being Integer holds
( i < j iff uInt . i < uInt . j )

proof end;

theorem Th10: :: SURREALN:10

for i being Integer
for x being Surreal holds
( [{(uInt . (i - 1))},{(uInt . (i + 1))}] is Surreal & ( x = [{(uInt . (i - 1))},{(uInt . (i + 1))}] implies x == uInt . i ) )

proof end;

theorem Th11: :: SURREALN:11

uInt . 1 = 1_No

proof end;

theorem Th12: :: SURREALN:12

for i being Integer holds - (uInt . i) = uInt . (- i)

proof end;

theorem Th13: :: SURREALN:13

for n, m being Nat holds (uInt . n) + (uInt . m) = uInt . (n + m)

proof end;

theorem Th14: :: SURREALN:14

for i, j being Integer holds (uInt . i) + (uInt . j) == uInt . (i + j)

proof end;

theorem Th15: :: SURREALN:15

for i, j being Integer holds (uInt . i) * (uInt . j) == uInt . (i * j)

proof end;

theorem Th16: :: SURREALN:16

for x, y being Surreal st x = [{y},{}] & y < 0_No holds
x == 0_No

proof end;

theorem Th17: :: SURREALN:17

for x, y being Surreal st x = [{y},{}] & born x is finite & 0_No <= y holds
ex n being Nat st
( x == uInt . (n + 1) & uInt . n <= y & y < uInt . (n + 1) & n in born x )

proof end;

definition

let r be Rational;

attr r is dyadic-like means :: SURREALN:def 2
ex n being Nat st denominator r = 2 |^ n;

end;

:: deftheorem defines dyadic-like SURREALN:def 2 :
for r being Rational holds
( r is dyadic-like iff ex n being Nat st denominator r = 2 |^ n );

theorem Th18: :: SURREALN:18

for r being Rational holds
( r is dyadic-like iff ex i being Integer ex n being Nat st r = i / (2 |^ n) )

proof end;

registration

let i be Integer;
let n be Nat;

cluster i / (2 |^ n) -> dyadic-like ;

coherence
i / (2 |^ n) is dyadic-like by Th18;

end;

registration

cluster integer -> dyadic-like for object ;

coherence
for b₁ being Integer holds b₁ is dyadic-like

proof end;

end;

registration

let x be dyadic-like Rational;

cluster - x -> dyadic-like ;

coherence
- x is dyadic-like

proof end;

let y be dyadic-like Rational;

cluster x + y -> dyadic-like ;

coherence
x + y is dyadic-like

proof end;

cluster x + y -> dyadic-like ;

coherence
x + y is dyadic-like ;

cluster x * y -> dyadic-like ;

coherence
x * y is dyadic-like

proof end;

end;

definition

func DYADIC -> set means :Def3: :: SURREALN:def 3
for o being object holds
( o in it iff o is dyadic-like Rational );

existence
ex b₁ being set st
for o being object holds
( o in b₁ iff o is dyadic-like Rational )

proof end;

uniqueness
for b₁, b₂ being set st ( for o being object holds
( o in b₁ iff o is dyadic-like Rational ) ) & ( for o being object holds
( o in b₂ iff o is dyadic-like Rational ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines DYADIC SURREALN:def 3 :
for b₁ being set holds
( b₁ = DYADIC iff for o being object holds
( o in b₁ iff o is dyadic-like Rational ) );

registration

cluster DYADIC -> non empty rational-membered ;

coherence
( DYADIC is rational-membered & not DYADIC is empty )

proof end;

end;

registration

cluster -> dyadic-like for Element of DYADIC ;

coherence
for b₁ being Element of DYADIC holds b₁ is dyadic-like by Def3;

end;

definition

mode Dyadic is dyadic-like Rational;

end;

definition

let n be Nat;

func DYADIC n -> Subset of DYADIC means :Def4: :: SURREALN:def 4
for d being Dyadic holds
( d in it iff ex i being Integer st d = i / (2 |^ n) );

existence
ex b₁ being Subset of DYADIC st
for d being Dyadic holds
( d in b₁ iff ex i being Integer st d = i / (2 |^ n) )

proof end;

uniqueness
for b₁, b₂ being Subset of DYADIC st ( for d being Dyadic holds
( d in b₁ iff ex i being Integer st d = i / (2 |^ n) ) ) & ( for d being Dyadic holds
( d in b₂ iff ex i being Integer st d = i / (2 |^ n) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines DYADIC SURREALN:def 4 :
for n being Nat
for b₂ being Subset of DYADIC holds
( b₂ = DYADIC n iff for d being Dyadic holds
( d in b₂ iff ex i being Integer st d = i / (2 |^ n) ) );

theorem Th19: :: SURREALN:19

for n, m being Nat st n <= m holds
DYADIC n c= DYADIC m

proof end;

theorem Th20: :: SURREALN:20

for d being Dyadic
for n being Nat holds
( d in (DYADIC (n + 1)) \ (DYADIC n) iff ex i being Integer st d = ((2 * i) + 1) / (2 |^ (n + 1)) )

proof end;

theorem Th21: :: SURREALN:21

INT = DYADIC 0

proof end;

theorem Th22: :: SURREALN:22

rng uInt c= Day NAT

proof end;

theorem Th23: :: SURREALN:23

for d being Dyadic holds
( d is Integer or ex p being Nat ex i being Integer st d = ((2 * i) + 1) / (2 |^ (p + 1)) )

proof end;

definition

func uDyadic -> ManySortedSet of DYADIC means :Def5: :: SURREALN:def 5
for i, j being Integer
for p being Nat holds
( it . i = uInt . i & it . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(it . (j / (2 |^ p)))},{(it . ((j + 1) / (2 |^ p)))}] );

existence
ex b₁ being ManySortedSet of DYADIC st
for i, j being Integer
for p being Nat holds
( b₁ . i = uInt . i & b₁ . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(b₁ . (j / (2 |^ p)))},{(b₁ . ((j + 1) / (2 |^ p)))}] )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of DYADIC st ( for i, j being Integer
for p being Nat holds
( b₁ . i = uInt . i & b₁ . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(b₁ . (j / (2 |^ p)))},{(b₁ . ((j + 1) / (2 |^ p)))}] ) ) & ( for i, j being Integer
for p being Nat holds
( b₂ . i = uInt . i & b₂ . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(b₂ . (j / (2 |^ p)))},{(b₂ . ((j + 1) / (2 |^ p)))}] ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines uDyadic SURREALN:def 5 :
for b₁ being ManySortedSet of DYADIC holds
( b₁ = uDyadic iff for i, j being Integer
for p being Nat holds
( b₁ . i = uInt . i & b₁ . (((2 * j) + 1) / (2 |^ (p + 1))) = [{(b₁ . (j / (2 |^ p)))},{(b₁ . ((j + 1) / (2 |^ p)))}] ) );

Lm5: for p being Nat holds
( ( for d being Dyadic holds uDyadic . d is Surreal ) & ( for i, j being Integer
for si, sj being Surreal st si = uDyadic . (i / (2 |^ p)) & sj = uDyadic . (j / (2 |^ p)) holds
( i < j iff si < sj ) ) )

proof end;

registration

let d be Dyadic;

cluster uDyadic . d -> surreal ;

coherence
uDyadic . d is surreal by Lm5;

end;

theorem Th24: :: SURREALN:24

for d1, d2 being Dyadic holds
( d1 < d2 iff uDyadic . d1 < uDyadic . d2 )

proof end;

theorem Th25: :: SURREALN:25

for z being Surreal
for n being Nat holds
( ( 0_No <= z & z in Day n & not z == uDyadic . n implies ex x, y, p being Nat st
( z == uDyadic . (x + (y / (2 |^ p))) & y < 2 |^ p & x + p < n ) ) & ( for x, y, p being Nat st y < 2 |^ p & x + p < n holds
( 0_No <= uDyadic . (x + (y / (2 |^ p))) & uDyadic . (x + (y / (2 |^ p))) in Day n ) ) )

proof end;

theorem Th26: :: SURREALN:26

for n, m, p being Nat st (2 * m) + 1 < 2 |^ p holds
born (uDyadic . (n + (((2 * m) + 1) / (2 |^ p)))) = (n + p) + 1

proof end;

theorem Th27: :: SURREALN:27

for d being Dyadic holds uDyadic . (- d) = - (uDyadic . d)

proof end;

theorem Th28: :: SURREALN:28

for d being Dyadic st 0 <= d & d is not Integer holds
ex n, m, p being Nat st
( d = n + (((2 * m) + 1) / (2 |^ (p + 1))) & (2 * m) + 1 < 2 |^ (p + 1) )

proof end;

theorem Th29: :: SURREALN:29

for d being Dyadic holds
( 0 <= d iff 0_No <= uDyadic . d )

proof end;

theorem Th30: :: SURREALN:30

for d being Dyadic holds uDyadic . d in born_eq_set (uDyadic . d)

proof end;

theorem Th31: :: SURREALN:31

for x being Surreal st born x is finite & (card (L_ x)) (+) (card (R_ x)) c= 1 holds
ex i being Integer st x == uInt . i

proof end;

theorem Th32: :: SURREALN:32

for x1, x2, y1, y2, p1, p2 being Nat st x1 + (y1 / (2 |^ p1)) = x2 + (y2 / (2 |^ p2)) & y1 < 2 |^ p1 & y2 < 2 |^ p2 holds
x1 = x2

proof end;

theorem Th33: :: SURREALN:33

for x1, x2, y1, y2, p1, p2 being Nat st x1 + (y1 / (2 |^ p1)) < x2 + (y2 / (2 |^ p2)) & y1 < 2 |^ p1 & y2 < 2 |^ p2 holds
x1 <= x2

proof end;

theorem Th34: :: SURREALN:34

for x1, x2, p1, p2 being Nat st ((2 * x1) + 1) / (2 |^ p1) = x2 / (2 |^ p2) holds
p1 <= p2

proof end;

theorem Th35: :: SURREALN:35

for x being Surreal
for n being Nat st x in Day n holds
ex d being Dyadic st
( x == uDyadic . d & uDyadic . d in Day n )

proof end;

Lm6: for d being Dyadic st d >= 0 holds
ex n being Nat st uDyadic . d in Day n

proof end;

theorem Th36: :: SURREALN:36

for d being Dyadic ex n being Nat st uDyadic . d in Day n

proof end;

registration

let d be Dyadic;

cluster uDyadic . d -> uniq-surreal ;

coherence
uDyadic . d is uniq-surreal

proof end;

end;

theorem Th37: :: SURREALN:37

for x being Surreal holds
( ( x is uSurreal & born x is finite ) iff ex d being Dyadic st x = uDyadic . d )

proof end;

Lm7: for n, p being Nat
for x being Surreal st p > 0 holds
( [{(uDyadic . (n / (2 |^ p)))},{(uDyadic . ((n + 2) / (2 |^ p)))}] is Surreal & ( x = [{(uDyadic . (n / (2 |^ p)))},{(uDyadic . ((n + 2) / (2 |^ p)))}] implies x == uDyadic . ((n + 1) / (2 |^ p)) ) )

proof end;

theorem Th38: :: SURREALN:38

for i being Integer
for p being Nat
for x being Surreal holds
( [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] is Surreal & ( x = [{(uDyadic . (i / (2 |^ p)))},{(uDyadic . ((i + 2) / (2 |^ p)))}] implies x == uDyadic . ((i + 1) / (2 |^ p)) ) )

proof end;

Lm8: for d being Dyadic
for i being Integer holds (uDyadic . i) + (uDyadic . d) == uDyadic . (i + d)

proof end;

theorem Th39: :: SURREALN:39

for d1, d2 being Dyadic holds (uDyadic . d1) + (uDyadic . d2) == uDyadic . (d1 + d2)

proof end;

Lm9: for d being Dyadic
for i being Integer holds (uDyadic . i) * (uDyadic . d) == uDyadic . (i * d)

proof end;

theorem Th40: :: SURREALN:40

for d1, d2 being Dyadic holds (uDyadic . d1) * (uDyadic . d2) == uDyadic . (d1 * d2)

proof end;

definition

func sReal -> ManySortedSet of REAL means :Def6: :: SURREALN:def 6
for r being Real holds it . r = [ { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } , { (uDyadic . ([\((r * (2 |^ m)) + 1)/] / (2 |^ m))) where m is Nat : verum } ];

existence
ex b₁ being ManySortedSet of REAL st
for r being Real holds b₁ . r = [ { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } , { (uDyadic . ([\((r * (2 |^ m)) + 1)/] / (2 |^ m))) where m is Nat : verum } ]

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of REAL st ( for r being Real holds b₁ . r = [ { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } , { (uDyadic . ([\((r * (2 |^ m)) + 1)/] / (2 |^ m))) where m is Nat : verum } ] ) & ( for r being Real holds b₂ . r = [ { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } , { (uDyadic . ([\((r * (2 |^ m)) + 1)/] / (2 |^ m))) where m is Nat : verum } ] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines sReal SURREALN:def 6 :
for b₁ being ManySortedSet of REAL holds
( b₁ = sReal iff for r being Real holds b₁ . r = [ { (uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n))) where n is Nat : verum } , { (uDyadic . ([\((r * (2 |^ m)) + 1)/] / (2 |^ m))) where m is Nat : verum } ] );

theorem Th41: :: SURREALN:41

for n being Nat
for r being Real holds
( [/((r * (2 |^ n)) - 1)\] / (2 |^ n) < r & r < [\((r * (2 |^ n)) + 1)/] / (2 |^ n) )

proof end;

Lm10: for r being Real holds sReal . r in Day omega

proof end;

registration

let r be Real;

cluster sReal . r -> surreal ;

coherence
sReal . r is surreal by Lm10;

end;

definition

func uReal -> ManySortedSet of REAL means :Def7: :: SURREALN:def 7
for r being Real holds it . r = Unique_No (sReal . r);

existence
ex b₁ being ManySortedSet of REAL st
for r being Real holds b₁ . r = Unique_No (sReal . r)

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of REAL st ( for r being Real holds b₁ . r = Unique_No (sReal . r) ) & ( for r being Real holds b₂ . r = Unique_No (sReal . r) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines uReal SURREALN:def 7 :
for b₁ being ManySortedSet of REAL holds
( b₁ = uReal iff for r being Real holds b₁ . r = Unique_No (sReal . r) );

registration

let r be Real;

cluster uReal . r -> surreal ;

coherence
uReal . r is surreal

proof end;

end;

registration

let r be Real;

cluster uReal . r -> uniq-surreal ;

coherence
uReal . r is uniq-surreal

proof end;

end;

theorem Th42: :: SURREALN:42

for x being Surreal
for r being Real holds
( x in L_ (sReal . r) iff ex n being Nat st x = uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) )

proof end;

theorem Th43: :: SURREALN:43

for x being Surreal
for r being Real holds
( x in R_ (sReal . r) iff ex n being Nat st x = uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) )

proof end;

theorem Th44: :: SURREALN:44

for n being Nat
for r being Real holds
( uDyadic . ([/((r * (2 |^ n)) - 1)\] / (2 |^ n)) < sReal . r & sReal . r < uDyadic . ([\((r * (2 |^ n)) + 1)/] / (2 |^ n)) )

proof end;

theorem Th45: :: SURREALN:45

for i1, i2 being Integer
for n1, n2 being Nat st i1 / (2 |^ n1) < i2 / (2 |^ n2) holds
( i1 / (2 |^ n1) < (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) & (((i1 * (2 |^ n2)) * 2) + 1) / (2 |^ ((n1 + n2) + 1)) <= (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) & (((i2 * (2 |^ n1)) * 2) - 1) / (2 |^ ((n1 + n2) + 1)) < i2 / (2 |^ n2) )

proof end;

theorem Th46: :: SURREALN:46

for d being Dyadic holds
( sReal . d == uDyadic . d & uDyadic . d = uReal . d )

proof end;

theorem Th47: :: SURREALN:47

uReal . 0 = 0_No

proof end;

theorem Th48: :: SURREALN:48

uReal . 1 = 1_No

proof end;

theorem Th49: :: SURREALN:49

for r being Real holds born (sReal . r) c= omega

proof end;

theorem Th50: :: SURREALN:50

for r1, r2 being Real holds
( sReal . r1 < sReal . r2 iff r1 < r2 )

proof end;

theorem Th51: :: SURREALN:51

for r1, r2 being Real holds
( uReal . r1 < uReal . r2 iff r1 < r2 )

proof end;

registration

let r be positive Real;

cluster uReal . r -> positive ;

coherence
uReal . r is positive by Th51, Th47;

end;

theorem :: SURREALN:52

for r being Real holds
( born (uReal . r) = omega iff r is not Dyadic )

proof end;

theorem Th53: :: SURREALN:53

for r1, r2 being Real st r1 < r2 holds
ex n being Nat st [\((r1 * (2 |^ n)) + 1)/] / (2 |^ n) < r2

proof end;

theorem Th54: :: SURREALN:54

for r1, r2 being Real st r1 < r2 holds
ex n being Nat st r1 < [/((r2 * (2 |^ n)) - 1)\] / (2 |^ n)

proof end;

Lm11: for r1, r2 being Real holds (L_ (sReal . r1)) ++ {(sReal . r2)} << {(sReal . (r1 + r2))}

proof end;

Lm12: for r1, r2 being Real holds {(sReal . (r1 + r2))} << (R_ (sReal . r1)) ++ {(sReal . r2)}

proof end;

Lm13: for r1, r2 being Real holds (sReal . r1) + (sReal . r2) == sReal . (r1 + r2)

proof end;

theorem Th55: :: SURREALN:55

for r1, r2 being Real holds (uReal . r1) + (uReal . r2) == uReal . (r1 + r2)

proof end;

Lm14: for r being Real holds - (sReal . r) == sReal . (- r)

proof end;

theorem Th56: :: SURREALN:56

for r being Real holds - (uReal . r) == uReal . (- r)

proof end;

Lm15: for i being Integer
for r being Real holds sReal . (r * i) == (sReal . r) * (uDyadic . i)

proof end;

Lm16: for r being Real holds sReal . (r / 2) == (sReal . r) * (uDyadic . (1 / (2 |^ 1)))

proof end;

Lm17: for d being Dyadic
for r being Real holds sReal . (r * d) == (sReal . r) * (uDyadic . d)

proof end;

Lm18: for r1, r2 being Real
for d1, d2 being Dyadic holds (((uDyadic . d1) * (sReal . r2)) + ((sReal . r1) * (uDyadic . d2))) + (- ((uDyadic . d1) * (uDyadic . d2))) == sReal . (((d1 * r2) + (r1 * d2)) - (d1 * d2))

proof end;

Lm19: for r1, r2 being Real holds (sReal . r1) * (sReal . r2) == sReal . (r1 * r2)

proof end;

theorem Th57: :: SURREALN:57

for r1, r2 being Real holds (uReal . r1) * (uReal . r2) == uReal . (r1 * r2)

proof end;

theorem Th58: :: SURREALN:58

for n being Nat st n > 0 holds
(uInt . n) " == uReal . (1 / n)

proof end;

definition

let x be Surreal;

func real_qua x -> Surreal means :Def8: :: SURREALN:def 8
( L_ it = { (x - ((uInt . n) ")) where n is positive Nat : verum } & R_ it = { (x + ((uInt . n) ")) where n is positive Nat : verum } );

existence
ex b₁ being Surreal st
( L_ b₁ = { (x - ((uInt . n) ")) where n is positive Nat : verum } & R_ b₁ = { (x + ((uInt . n) ")) where n is positive Nat : verum } )

proof end;

uniqueness
for b₁, b₂ being Surreal st L_ b₁ = { (x - ((uInt . n) ")) where n is positive Nat : verum } & R_ b₁ = { (x + ((uInt . n) ")) where n is positive Nat : verum } & L_ b₂ = { (x - ((uInt . n) ")) where n is positive Nat : verum } & R_ b₂ = { (x + ((uInt . n) ")) where n is positive Nat : verum } holds
b₁ = b₂ by XTUPLE_0:2;

end;

:: deftheorem Def8 defines real_qua SURREALN:def 8 :
for x, b₂ being Surreal holds
( b₂ = real_qua x iff ( L_ b₂ = { (x - ((uInt . n) ")) where n is positive Nat : verum } & R_ b₂ = { (x + ((uInt . n) ")) where n is positive Nat : verum } ) );

definition

let x be Surreal;

attr x is *real means :: SURREALN:def 9
( x == real_qua x & ex n being Nat st
( uInt . (- n) < x & x < uInt . n ) );

end;

:: deftheorem defines *real SURREALN:def 9 :
for x being Surreal holds
( x is *real iff ( x == real_qua x & ex n being Nat st
( uInt . (- n) < x & x < uInt . n ) ) );

theorem Th59: :: SURREALN:59

for x being Surreal
for n being positive Nat holds
( x - ((uInt . n) ") < real_qua x & real_qua x < x + ((uInt . n) ") )

proof end;

Lm20: for x, y being Surreal st x == y holds
real_qua x <= real_qua y

proof end;

theorem :: SURREALN:60

for x, y being Surreal st x == y holds
real_qua x == real_qua y by Lm20;

Lm21: for r being Real holds sReal . r == real_qua (sReal . r)

proof end;

Lm22: for r being Real ex n being Nat st
( - n < r & r < n )

proof end;

theorem Th61: :: SURREALN:61

for x, y being Surreal st x == y & x is *real holds
y is *real

proof end;

registration

let r be Real;

cluster sReal . r -> *real ;

coherence
sReal . r is *real

proof end;

cluster uReal . r -> *real ;

coherence
uReal . r is *real

proof end;

end;

registration

cluster non empty pair surreal uniq-surreal *real for set ;

existence
ex b₁ being uSurreal st b₁ is *real

proof end;

end;

theorem Th62: :: SURREALN:62

for x being Surreal holds
( x is *real iff ex r being Real st x == uReal . r )

proof end;

registration

let x be *real Surreal;

cluster - x -> *real ;

coherence
- x is *real

proof end;

let y be *real Surreal;

cluster x + y -> *real ;

coherence
x + y is *real

proof end;

cluster x * y -> *real ;

coherence
x * y is *real

proof end;

end;

definition

let x be Surreal;

attr x is No_ordinal means :Def10: :: SURREALN:def 10
R_ x = {} ;

end;

:: deftheorem Def10 defines No_ordinal SURREALN:def 10 :
for x being Surreal holds
( x is No_ordinal iff R_ x = {} );

registration

cluster 0_No -> No_ordinal ;

coherence
0_No is No_ordinal ;
let n be Nat;

cluster uInt . n -> No_ordinal ;

coherence
uInt . n is No_ordinal by Th7;

end;

registration

cluster non empty pair surreal uniq-surreal No_ordinal for set ;

existence
ex b₁ being uSurreal st b₁ is No_ordinal

proof end;

end;

definition

let A be Ordinal;

func No_Ordinal_op A -> set means :Def11: :: SURREALN:def 11
ex S being Sequence st
( it = S . A & dom S = succ A & ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) );

existence
ex b₁ being set ex S being Sequence st
( b₁ = S . A & dom S = succ A & ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) )

proof end;

uniqueness
for b₁, b₂ being set st ex S being Sequence st
( b₁ = S . A & dom S = succ A & ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) ) & ex S being Sequence st
( b₂ = S . A & dom S = succ A & ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines No_Ordinal_op SURREALN:def 11 :
for A being Ordinal
for b₂ being set holds
( b₂ = No_Ordinal_op A iff ex S being Sequence st
( b₂ = S . A & dom S = succ A & ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) ) );

theorem Th63: :: SURREALN:63

for A being Ordinal
for S being Sequence st dom S = succ A & ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) holds
for O being Ordinal st O in succ A holds
S . O = No_Ordinal_op O

proof end;

theorem Th64: :: SURREALN:64

No_Ordinal_op 0 = 0_No

proof end;

theorem Th65: :: SURREALN:65

for A being Ordinal holds No_Ordinal_op (succ A) = [{(No_Ordinal_op A)},{}]

proof end;

theorem Th66: :: SURREALN:66

for A being Ordinal st A is limit_ordinal holds
ex X being set st
( No_Ordinal_op A = [X,{}] & ( for o being object holds
( o in X iff ex B being Ordinal st
( B in A & o = No_Ordinal_op B ) ) ) )

proof end;

theorem Th67: :: SURREALN:67

for A being Ordinal holds No_Ordinal_op A in Day A

proof end;

registration

let A be Ordinal;

cluster No_Ordinal_op A -> surreal ;

coherence
No_Ordinal_op A is surreal

proof end;

end;

registration

let A be Ordinal;

cluster No_Ordinal_op A -> No_ordinal ;

coherence
No_Ordinal_op A is No_ordinal

proof end;

end;

Lm23: for A, B being Ordinal st A in B holds
No_Ordinal_op A < No_Ordinal_op B

proof end;

theorem Th68: :: SURREALN:68

for A, B being Ordinal holds
( No_Ordinal_op A < No_Ordinal_op B iff A in B )

proof end;

theorem Th69: :: SURREALN:69

for A being Ordinal
for x being Surreal st x in Day A holds
x <= No_Ordinal_op A

proof end;

theorem Th70: :: SURREALN:70

for A being Ordinal holds born (No_Ordinal_op A) = A

proof end;

theorem Th71: :: SURREALN:71

for A being Ordinal
for x being Surreal st x in L_ (No_Ordinal_op A) holds
ex B being Ordinal st
( B in A & x = No_Ordinal_op B )

proof end;

Lm24: for x being Surreal st x is No_ordinal holds
ex A being Ordinal st x == No_Ordinal_op A

proof end;

theorem Th72: :: SURREALN:72

for n being Nat holds uInt . n = No_Ordinal_op n

proof end;

registration

let O be No_ordinal Surreal;

cluster Unique_No O -> No_ordinal ;

coherence
Unique_No O is No_ordinal

proof end;

end;

definition

let A be Ordinal;

func No_uOrdinal_op A -> No_ordinal uSurreal equals :: SURREALN:def 12
Unique_No (No_Ordinal_op A);

coherence
Unique_No (No_Ordinal_op A) is No_ordinal uSurreal ;

end;

:: deftheorem defines No_uOrdinal_op SURREALN:def 12 :
for A being Ordinal holds No_uOrdinal_op A = Unique_No (No_Ordinal_op A);

theorem Th73: :: SURREALN:73

for A being Ordinal holds
( No_uOrdinal_op A == No_Ordinal_op A & born (No_uOrdinal_op A) = A )

proof end;

theorem Th74: :: SURREALN:74

for A being Ordinal holds No_uOrdinal_op A in Day A

proof end;

theorem Th75: :: SURREALN:75

for A, B being Ordinal holds
( No_uOrdinal_op A < No_uOrdinal_op B iff A in B )

proof end;

theorem Th76: :: SURREALN:76

for A being Ordinal
for x being Surreal st x in Day A holds
x <= No_uOrdinal_op A

proof end;

theorem :: SURREALN:77

for x being Surreal st x is No_ordinal holds
ex A being Ordinal st x == No_uOrdinal_op A

proof end;

theorem :: SURREALN:78

for n being Nat holds uInt . n = No_uOrdinal_op n

proof end;

theorem :: SURREALN:79

for A being Ordinal holds No_uOrdinal_op (succ A) = [{(No_uOrdinal_op A)},{}]

proof end;

theorem :: SURREALN:80

for A being Ordinal ex x being No_ordinal Surreal st
( born x = A & No_uOrdinal_op A == x & ( for o being object holds
( o in L_ x iff ex B being Ordinal st
( B in A & o = No_uOrdinal_op B ) ) ) )

proof end;

registration

let alpha, beta be No_ordinal Surreal;

cluster alpha + beta -> No_ordinal ;

coherence
alpha + beta is No_ordinal

proof end;

cluster alpha * beta -> No_ordinal ;

coherence
alpha * beta is No_ordinal

proof end;

end;