:: Natural Addition of Ordinals
:: by Sebastian Koch
::
:: Received May 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

:: into ORDINAL1 ?

theorem Th1: :: ORDINAL7:1

for X being set holds X /\ (succ X) = X

proof end;

:: into ORDINAL2 ?

registration

let A be increasing Ordinal-Sequence;
let a be Ordinal;

cluster A | a -> increasing ;

coherence
A | a is increasing

proof end;

end;

Lm1: succ 0 = 1
;

Lm2: succ (succ 0) = 2
;

:: into ORDINAL2 ?

theorem Th2: :: ORDINAL7:2

for a being Ordinal holds a +^ a = 2 *^ a

proof end;

:: into ORDINAL2 ?

theorem :: ORDINAL7:3

for a, b being Ordinal st 1 in a & a in b holds
b +^ a in a *^ b

proof end;

:: into ORDINAL2 ?

theorem Th4: :: ORDINAL7:4

for a being Ordinal holds a *^ a = exp (a,2)

proof end;

:: into ORDINAL4 ?

theorem :: ORDINAL7:5

for a, b being Ordinal st 1 in a & a in b holds
a *^ b in exp (b,a)

proof end;

:: a |^|^ 2 = exp(a, a) is ORDINAL5:18
:: into ORDINAL5 ?

theorem :: ORDINAL7:6

for a, b being Ordinal st 1 in a & a in b holds
exp (b,a) in b |^|^ a

proof end;

registration

cluster Relation-like Function-like Sequence-like infinite Ordinal-yielding for set ;

existence
ex b₁ being Ordinal-Sequence st b₁ is infinite

proof end;

end;

Th9: for A, B being Sequence holds rng (A ^ B) = (rng A) \/ (rng B)
by ORDINAL4:2;

:: into ORDINAL4 ?

theorem Th10: :: ORDINAL7:7

for A, B being Sequence st A ^ B is Ordinal-yielding holds
( A is Ordinal-yielding & B is Ordinal-yielding )

proof end;

Th13: for D being set
for p being FinSequence of D
for n being Nat holds
( n + 1 in dom p iff n in dom (FS2XFS p) )
by AFINSQ_1:94;

Th15: for D being set
for p being FinSequence of D holds rng p = rng (FS2XFS p)
by AFINSQ_1:96;

Th19: for D being set
for p being one-to-one XFinSequence of D
for n being Nat holds rng (p | n) misses rng (p /^ n)
by AFINSQ_2:87;

:: into ORDINAL5 ?
:: corrolary from theorem above

theorem Th21: :: ORDINAL7:8

for a, b being Ordinal st a in b holds
b -exponent a = 0

proof end;

:: into ORDINAL5 ?

theorem Th22: :: ORDINAL7:9

for a, b, c being Ordinal st a c= c holds
b -exponent a c= b -exponent c

proof end;

:: into ORDINAL5 ?

theorem Th23: :: ORDINAL7:10

for a, b, c being Ordinal st 0 in a & 1 in b & a in exp (b,c) holds
b -exponent a in c

proof end;

:: into ORDINAL5 ?

registration

cluster Relation-like Function-like Sequence-like Ordinal-yielding decreasing -> one-to-one for set ;

coherence
for b₁ being Ordinal-Sequence st b₁ is decreasing holds
b₁ is one-to-one

proof end;

end;

:: into ORDINAL5 ?

registration

let A be decreasing Sequence;
let a be Ordinal;

cluster A | a -> decreasing ;

coherence
A | a is decreasing

proof end;

end;

:: into ORDINAL5 ?

registration

let A be non-decreasing Sequence;
let a be Ordinal;

cluster A | a -> non-decreasing ;

coherence
A | a is non-decreasing

proof end;

end;

:: into ORDINAL5 ?

registration

let A be non-increasing Sequence;
let a be Ordinal;

cluster A | a -> non-increasing ;

coherence
A | a is non-increasing

proof end;

end;

:: into ORDINAL5 ?

theorem Th24: :: ORDINAL7:11

for A, B being finite Ordinal-Sequence holds Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B)

proof end;

:: into ORDINAL5 ?

theorem Th25: :: ORDINAL7:12

for a, b being Ordinal holds Sum^ <%a,b%> = a +^ b

proof end;

:: into ORDINAL5 ?

registration

let A be non-empty non empty finite Ordinal-Sequence;

cluster Sum^ A -> non empty ;

coherence
not Sum^ A is empty

proof end;

let B be finite Ordinal-Sequence;

cluster Sum^ (A ^ B) -> non empty ;

coherence
not Sum^ (A ^ B) is empty

proof end;

cluster Sum^ (B ^ A) -> non empty ;

coherence
not Sum^ (B ^ A) is empty

proof end;

end;

:: into ORDINAL5 ?

theorem Th26: :: ORDINAL7:13

for a being Ordinal
for n being Nat holds Sum^ (n --> a) = n *^ a

proof end;

Lm5: for n being Nat holds succ n = n + 1

proof end;

:: into ORDINAL5 ?

theorem Th27: :: ORDINAL7:14

for A being finite Ordinal-Sequence
for a being Ordinal holds Sum^ (A | a) c= Sum^ A

proof end;

:: into ORDINAL5 ?

theorem Th28: :: ORDINAL7:15

for A, B being finite Ordinal-Sequence st dom A c= dom B & ( for a being object st a in dom A holds
A . a c= B . a ) holds
Sum^ A c= Sum^ B

proof end;

:: into ORDINAL5 ?
:: the mirror theorem of ORDINAL5:67

theorem Th29: :: ORDINAL7:16

for A being Cantor-normal-form Ordinal-Sequence st A <> {} holds
ex B being Cantor-normal-form Ordinal-Sequence ex a being Cantor-component Ordinal st A = B ^ <%a%>

proof end;

:: into ORDINAL5 ?

registration

let A be Cantor-normal-form Ordinal-Sequence;
let n be Nat;

cluster A | n -> Cantor-normal-form ;

coherence
A | n is Cantor-normal-form

proof end;

end;

:: into ORDINAL5 or AFINSQ_2 ?

registration

let A be Cantor-normal-form Ordinal-Sequence;
let n be Nat;

cluster A /^ n -> Cantor-normal-form ;

coherence
A /^ n is Cantor-normal-form

proof end;

end;

registration

cluster Relation-like Function-like Sequence-like natural-valued -> Ordinal-yielding for set ;

coherence
for b₁ being Sequence st b₁ is natural-valued holds
b₁ is Ordinal-yielding

proof end;

end;

registration

cluster limit_ordinal natural -> zero for set ;

coherence
for b₁ being Nat st b₁ is limit_ordinal holds
b₁ is zero ;

cluster epsilon-transitive epsilon-connected ordinal non limit_ordinal V72() for set ;

existence
not for b₁ being Ordinal holds b₁ is limit_ordinal

proof end;

end;

registration

let n, m be Nat;

identify n \/ m with max (n,m);

correctness
compatibility
n \/ m = max (n,m);

proof end;

identify n /\ m with min (n,m);

correctness
compatibility
n /\ m = min (n,m);

proof end;

end;

:: absorption law of ordinal numbers

theorem Th30: :: ORDINAL7:17

for a, b being Ordinal holds
( a +^ b = b iff omega *^ a c= b )

proof end;

theorem Th31: :: ORDINAL7:18

for A being non empty Cantor-normal-form Ordinal-Sequence
for a being object st a in dom A holds
omega -exponent (last A) c= omega -exponent (A . a)

proof end;

theorem Th32: :: ORDINAL7:19

for A being non empty Cantor-normal-form Ordinal-Sequence
for a being object st a in dom A holds
omega -exponent (A . a) c= omega -exponent (A . 0)

proof end;

:: this implies ORDINAL5:68

theorem Th33: :: ORDINAL7:20

for A, B being non empty Cantor-normal-form Ordinal-Sequence st omega -exponent (B . 0) in omega -exponent (last A) holds
A ^ B is Cantor-normal-form

proof end;

Lm6: for A being decreasing Ordinal-Sequence
for n being Nat st len A = n + 1 holds
rng (A | n) = (rng A) \ {(A . n)}

proof end;

Lm7: for A, B being decreasing Ordinal-Sequence
for n being Nat st len A = n + 1 & rng A = rng B holds
A . n = B . n

proof end;

theorem Th34: :: ORDINAL7:21

for A, B being decreasing Ordinal-Sequence st rng A = rng B holds
A = B

proof end;

registration

let a be Ordinal;

cluster exp (omega,a) -> Cantor-component ;

coherence
exp (omega,a) is Cantor-component

proof end;

let n be non zero Nat;

cluster n *^ (exp (omega,a)) -> Cantor-component ;

coherence
n *^ (exp (omega,a)) is Cantor-component

proof end;

end;

registration

cluster natural non zero -> Cantor-component for set ;

coherence
for b₁ being Nat st not b₁ is zero holds
b₁ is Cantor-component

proof end;

end;

registration

let c be Cantor-component Ordinal;

cluster <%c%> -> Cantor-normal-form ;

coherence
<%c%> is Cantor-normal-form

proof end;

end;

theorem Th35: :: ORDINAL7:22

for c, d being Cantor-component Ordinal st omega -exponent d in omega -exponent c holds
<%c,d%> is Cantor-normal-form

proof end;

Lm8: for a being non empty Ordinal
for n, m being non zero Nat holds <%(n *^ (exp (omega,a))),m%> is Cantor-normal-form

proof end;

registration

let a be non empty Ordinal;
let m be non zero Nat;

cluster <%(exp (omega,a)),m%> -> Cantor-normal-form ;

coherence
<%(exp (omega,a)),m%> is Cantor-normal-form

proof end;

let n be non zero Nat;

cluster <%(n *^ (exp (omega,a))),m%> -> Cantor-normal-form ;

coherence
<%(n *^ (exp (omega,a))),m%> is Cantor-normal-form by Lm8;

end;

theorem :: ORDINAL7:23

for c, d, e being Cantor-component Ordinal st omega -exponent d in omega -exponent c & omega -exponent e in omega -exponent d holds
<%c,d,e%> is Cantor-normal-form

proof end;

theorem Th37: :: ORDINAL7:24

for A being non empty Cantor-normal-form Ordinal-Sequence
for b being Ordinal
for n being non zero Nat st b in omega -exponent (last A) holds
A ^ <%(n *^ (exp (omega,b)))%> is Cantor-normal-form

proof end;

theorem :: ORDINAL7:25

for A being non empty Cantor-normal-form Ordinal-Sequence
for b being Ordinal
for n being non zero Nat st omega -exponent (last A) <> 0 holds
A ^ <%n%> is Cantor-normal-form

proof end;

:: variant of ORDINAL5:68

theorem Th39: :: ORDINAL7:26

for A being non empty Cantor-normal-form Ordinal-Sequence
for b being Ordinal
for n being non zero Nat st omega -exponent (A . 0) in b holds
<%(n *^ (exp (omega,b)))%> ^ A is Cantor-normal-form

proof end;

:: closure of ordinal addition

theorem Th40: :: ORDINAL7:27

for a1, a2, b being Ordinal st a1 in exp (omega,b) & a2 in exp (omega,b) holds
a1 +^ a2 in exp (omega,b)

proof end;

theorem Th41: :: ORDINAL7:28

for A being finite Ordinal-Sequence
for b being Ordinal st ( for a being Ordinal st a in dom A holds
A . a in exp (omega,b) ) holds
Sum^ A in exp (omega,b)

proof end;

:: variant of ORDINAL5:7

theorem Th42: :: ORDINAL7:29

for a, b being Ordinal
for n being Nat st a in exp (omega,b) holds
n *^ a in exp (omega,b)

proof end;

theorem Th43: :: ORDINAL7:30

for A being finite Ordinal-Sequence
for a being Ordinal st <%a%> ^ A is Cantor-normal-form holds
Sum^ A in exp (omega,(omega -exponent a))

proof end;

theorem Th44: :: ORDINAL7:31

for A being Cantor-normal-form Ordinal-Sequence holds omega -exponent (Sum^ A) = omega -exponent (A . 0)

proof end;

theorem Th45: :: ORDINAL7:32

for A, B being Cantor-normal-form Ordinal-Sequence st Sum^ A = Sum^ B holds
A = B

proof end;

definition

let A be Ordinal-Sequence;
let b be Ordinal;

func b -exponent A -> Ordinal-Sequence means :Def1: :: ORDINAL7:def 1
( dom it = dom A & ( for a being object st a in dom A holds
it . a = b -exponent (A . a) ) );

existence
ex b₁ being Ordinal-Sequence st
( dom b₁ = dom A & ( for a being object st a in dom A holds
b₁ . a = b -exponent (A . a) ) )

proof end;

uniqueness
for b₁, b₂ being Ordinal-Sequence st dom b₁ = dom A & ( for a being object st a in dom A holds
b₁ . a = b -exponent (A . a) ) & dom b₂ = dom A & ( for a being object st a in dom A holds
b₂ . a = b -exponent (A . a) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines -exponent ORDINAL7:def 1 :
for A being Ordinal-Sequence
for b being Ordinal
for b₃ being Ordinal-Sequence holds
( b₃ = b -exponent A iff ( dom b₃ = dom A & ( for a being object st a in dom A holds
b₃ . a = b -exponent (A . a) ) ) );

registration

let A be empty Ordinal-Sequence;
let b be Ordinal;

cluster b -exponent A -> empty ;

coherence
b -exponent A is empty

proof end;

end;

registration

let A be non empty Ordinal-Sequence;
let b be Ordinal;

cluster b -exponent A -> non empty ;

coherence
not b -exponent A is empty

proof end;

end;

registration

let A be finite Ordinal-Sequence;
let b be Ordinal;

cluster b -exponent A -> finite ;

coherence
b -exponent A is finite

proof end;

end;

registration

let A be infinite Ordinal-Sequence;
let b be Ordinal;

cluster b -exponent A -> infinite ;

coherence
not b -exponent A is finite

proof end;

end;

theorem Th46: :: ORDINAL7:33

for a, b being Ordinal holds b -exponent <%a%> = <%(b -exponent a)%>

proof end;

theorem Th47: :: ORDINAL7:34

for A, B being Ordinal-Sequence
for b being Ordinal holds b -exponent (A ^ B) = (b -exponent A) ^ (b -exponent B)

proof end;

theorem Th48: :: ORDINAL7:35

for A being Ordinal-Sequence
for b, c being Ordinal holds b -exponent (A | c) = (b -exponent A) | c

proof end;

theorem Th49: :: ORDINAL7:36

for A being finite Ordinal-Sequence
for b being Ordinal
for n being Nat holds b -exponent (A /^ n) = (b -exponent A) /^ n

proof end;

registration

let A be Cantor-normal-form Ordinal-Sequence;

cluster omega -exponent A -> decreasing ;

coherence
omega -exponent A is decreasing

proof end;

end;

theorem :: ORDINAL7:37

for A, B being Ordinal-Sequence st A ^ B is Cantor-normal-form holds
rng (omega -exponent A) misses rng (omega -exponent B)

proof end;

theorem Th51: :: ORDINAL7:38

for A being Cantor-normal-form Ordinal-Sequence holds
( 0 in rng (omega -exponent A) iff ( A <> {} & omega -exponent (last A) = 0 ) )

proof end;

definition

let a, b be Ordinal;

func b -leading_coeff a -> Ordinal equals :: ORDINAL7:def 2
a div^ (exp (b,(b -exponent a)));

coherence
a div^ (exp (b,(b -exponent a))) is Ordinal ;

end;

:: deftheorem defines -leading_coeff ORDINAL7:def 2 :
for a, b being Ordinal holds b -leading_coeff a = a div^ (exp (b,(b -exponent a)));

:: This is the undefined case. One could have set the value simply to 0
:: in case that b = 0 just as well.

theorem Th52: :: ORDINAL7:39

for a being Ordinal holds 0 -leading_coeff a = a

proof end;

:: this means that a = a *^ exp(1,0)

theorem Th53: :: ORDINAL7:40

for a being Ordinal holds 1 -leading_coeff a = a

proof end;

:: this means that 0 = 0 *^ exp(b,0)

theorem :: ORDINAL7:41

for b being Ordinal holds b -leading_coeff 0 = 0 by ORDINAL3:70;

:: this means that a = a *^ exp(b,0)

theorem Th55: :: ORDINAL7:42

for a, b being Ordinal st a in b holds
b -leading_coeff a = a

proof end;

:: this means that 1 = 1 *^ exp(b,0)

theorem :: ORDINAL7:43

for b being Ordinal holds b -leading_coeff 1 = 1

proof end;

theorem Th57: :: ORDINAL7:44

for a, b, c being Ordinal st c in b holds
b -leading_coeff (c *^ (exp (b,a))) = c

proof end;

theorem :: ORDINAL7:45

for a, b being Ordinal st 1 in b holds
b -leading_coeff (exp (b,a)) = 1

proof end;

registration

let c be Cantor-component Ordinal;

cluster omega -leading_coeff c -> non empty natural ;

coherence
( omega -leading_coeff c is natural & not omega -leading_coeff c is empty )

proof end;

end;

theorem Th59: :: ORDINAL7:46

for c being Cantor-component Ordinal holds c = (omega -leading_coeff c) *^ (exp (omega,(omega -exponent c)))

proof end;

definition

let A be Ordinal-Sequence;
let b be Ordinal;

func b -leading_coeff A -> Ordinal-Sequence means :Def3: :: ORDINAL7:def 3
( dom it = dom A & ( for a being object st a in dom A holds
it . a = b -leading_coeff (A . a) ) );

existence
ex b₁ being Ordinal-Sequence st
( dom b₁ = dom A & ( for a being object st a in dom A holds
b₁ . a = b -leading_coeff (A . a) ) )

proof end;

uniqueness
for b₁, b₂ being Ordinal-Sequence st dom b₁ = dom A & ( for a being object st a in dom A holds
b₁ . a = b -leading_coeff (A . a) ) & dom b₂ = dom A & ( for a being object st a in dom A holds
b₂ . a = b -leading_coeff (A . a) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines -leading_coeff ORDINAL7:def 3 :
for A being Ordinal-Sequence
for b being Ordinal
for b₃ being Ordinal-Sequence holds
( b₃ = b -leading_coeff A iff ( dom b₃ = dom A & ( for a being object st a in dom A holds
b₃ . a = b -leading_coeff (A . a) ) ) );

registration

let A be empty Ordinal-Sequence;
let b be Ordinal;

cluster b -leading_coeff A -> empty ;

coherence
b -leading_coeff A is empty

proof end;

end;

registration

let A be non empty Ordinal-Sequence;
let b be Ordinal;

cluster b -leading_coeff A -> non empty ;

coherence
not b -leading_coeff A is empty

proof end;

end;

registration

let A be finite Ordinal-Sequence;
let b be Ordinal;

cluster b -leading_coeff A -> finite ;

coherence
b -leading_coeff A is finite

proof end;

end;

registration

let A be infinite Ordinal-Sequence;
let b be Ordinal;

cluster b -leading_coeff A -> infinite ;

coherence
not b -leading_coeff A is finite

proof end;

end;

theorem Th60: :: ORDINAL7:47

for a, b being Ordinal holds b -leading_coeff <%a%> = <%(b -leading_coeff a)%>

proof end;

theorem :: ORDINAL7:48

for A, B being Ordinal-Sequence
for b being Ordinal holds b -leading_coeff (A ^ B) = (b -leading_coeff A) ^ (b -leading_coeff B)

proof end;

theorem :: ORDINAL7:49

for A being Ordinal-Sequence
for b, c being Ordinal holds b -leading_coeff (A | c) = (b -leading_coeff A) | c

proof end;

theorem :: ORDINAL7:50

for A being finite Ordinal-Sequence
for b being Ordinal
for n being Nat holds b -leading_coeff (A /^ n) = (b -leading_coeff A) /^ n

proof end;

registration

let A be Cantor-normal-form Ordinal-Sequence;
let a be object ;

cluster (omega -leading_coeff A) . a -> natural ;

coherence
(omega -leading_coeff A) . a is natural

proof end;

end;

registration

let A be Cantor-normal-form Ordinal-Sequence;

cluster omega -leading_coeff A -> non-empty natural-valued ;

coherence
( omega -leading_coeff A is natural-valued & omega -leading_coeff A is non-empty )

proof end;

end;

theorem Th64: :: ORDINAL7:51

for A being Cantor-normal-form Ordinal-Sequence
for a being object st a in dom A holds
A . a = (omega -leading_coeff (A . a)) *^ (exp (omega,(omega -exponent (A . a))))

proof end;

theorem Th65: :: ORDINAL7:52

for A being Cantor-normal-form Ordinal-Sequence
for a being object st a in dom A holds
A . a = ((omega -leading_coeff A) . a) *^ (exp (omega,((omega -exponent A) . a)))

proof end;

theorem Th66: :: ORDINAL7:53

for A being decreasing Ordinal-Sequence
for B being non-empty natural-valued Ordinal-Sequence st dom A = dom B holds
ex C being Cantor-normal-form Ordinal-Sequence st
( omega -exponent C = A & omega -leading_coeff C = B )

proof end;

theorem Th67: :: ORDINAL7:54

for A, B being Cantor-normal-form Ordinal-Sequence st omega -exponent A = omega -exponent B & omega -leading_coeff A = omega -leading_coeff B holds
A = B

proof end;

definition

let a be Ordinal;

func CantorNF a -> Cantor-normal-form Ordinal-Sequence means :Def4: :: ORDINAL7:def 4
Sum^ it = a;

existence
ex b₁ being Cantor-normal-form Ordinal-Sequence st Sum^ b₁ = a by ORDINAL5:69;
uniqueness
for b₁, b₂ being Cantor-normal-form Ordinal-Sequence st Sum^ b₁ = a & Sum^ b₂ = a holds
b₁ = b₂ by Th45;

end;

:: deftheorem Def4 defines CantorNF ORDINAL7:def 4 :
for a being Ordinal
for b₂ being Cantor-normal-form Ordinal-Sequence holds
( b₂ = CantorNF a iff Sum^ b₂ = a );

registration

let a be Ordinal;

reduce Sum^ (CantorNF a) to a;

correctness
reducibility
Sum^ (CantorNF a) = a;
by Def4;

end;

registration

let A be Cantor-normal-form Ordinal-Sequence;

reduce CantorNF (Sum^ A) to A;

correctness
reducibility
CantorNF (Sum^ A) = A;
by Def4;

end;

theorem :: ORDINAL7:55

CantorNF {} = {} by ORDINAL5:52;

registration

let a be empty Ordinal;

cluster CantorNF a -> empty Cantor-normal-form ;

coherence
CantorNF a is empty by ORDINAL5:52;

end;

registration

let a be non empty Ordinal;

cluster CantorNF a -> non empty Cantor-normal-form ;

coherence
not CantorNF a is empty by ORDINAL5:52;

end;

theorem Th69: :: ORDINAL7:56

for a being Ordinal
for n being non zero Nat holds CantorNF (n *^ (exp (omega,a))) = <%(n *^ (exp (omega,a)))%>

proof end;

theorem Th70: :: ORDINAL7:57

for a being Cantor-component Ordinal holds CantorNF a = <%a%>

proof end;

theorem Th71: :: ORDINAL7:58

for n being non zero Nat holds CantorNF n = <%n%>

proof end;

theorem :: ORDINAL7:59

for a being non empty Ordinal
for n, m being non zero Nat holds CantorNF ((n *^ (exp (omega,a))) +^ m) = <%(n *^ (exp (omega,a))),m%>

proof end;

theorem Th73: :: ORDINAL7:60

for a being non empty Ordinal
for b being Ordinal
for n being non zero Nat st b in omega -exponent (last (CantorNF a)) holds
CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%>

proof end;

theorem :: ORDINAL7:61

for a being non empty Ordinal
for n being non zero Nat st omega -exponent (last (CantorNF a)) <> 0 holds
CantorNF (a +^ n) = (CantorNF a) ^ <%n%>

proof end;

theorem :: ORDINAL7:62

for a being non empty Ordinal
for b being Ordinal
for n being non zero Nat st omega -exponent ((CantorNF a) . 0) in b holds
CantorNF ((n *^ (exp (omega,b))) +^ a) = <%(n *^ (exp (omega,b)))%> ^ (CantorNF a)

proof end;

definition

let a, b be Ordinal;

func a (+) b -> Ordinal means :Def5: :: ORDINAL7:def 5
ex C being Cantor-normal-form Ordinal-Sequence st
( it = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) );

existence
ex b₁ being Ordinal ex C being Cantor-normal-form Ordinal-Sequence st
( b₁ = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Ordinal st ex C being Cantor-normal-form Ordinal-Sequence st
( b₁ = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) & ex C being Cantor-normal-form Ordinal-Sequence st
( b₂ = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, a, b being Ordinal st ex C being Cantor-normal-form Ordinal-Sequence st
( b₁ = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) holds
ex C being Cantor-normal-form Ordinal-Sequence st
( b₁ = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF b))) \/ (rng (omega -exponent (CantorNF a))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) /\ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) ) ) ) )

proof end;

end;

:: deftheorem Def5 defines (+) ORDINAL7:def 5 :
for a, b, b₃ being Ordinal holds
( b₃ = a (+) b iff ex C being Cantor-normal-form Ordinal-Sequence st
( b₃ = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) );

theorem Th76: :: ORDINAL7:63

for a, b being Ordinal holds rng (omega -exponent (CantorNF (a (+) b))) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b)))

proof end;

theorem Th77: :: ORDINAL7:64

for a, b being Ordinal holds dom (CantorNF a) c= dom (CantorNF (a (+) b))

proof end;

theorem Th78: :: ORDINAL7:65

for a, b being Ordinal
for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) holds
omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d)))

proof end;

theorem Th79: :: ORDINAL7:66

for a, b being Ordinal
for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) holds
omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . d))) by Th78;

theorem Th80: :: ORDINAL7:67

for a, b being Ordinal
for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) holds
omega -leading_coeff ((CantorNF (a (+) b)) . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . d))))

proof end;

theorem Th81: :: ORDINAL7:68

for a, b, c being Ordinal holds (a (+) b) (+) c = a (+) (b (+) c)

proof end;

theorem Th82: :: ORDINAL7:69

for a being Ordinal holds a (+) 0 = a

proof end;

theorem Th83: :: ORDINAL7:70

for a, b being Ordinal
for n being Nat st omega -exponent a c= b holds
(n *^ (exp (omega,b))) (+) a = (n *^ (exp (omega,b))) +^ a

proof end;

theorem Th84: :: ORDINAL7:71

for A, B being finite Ordinal-Sequence st A ^ B is Cantor-normal-form holds
(Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B)

proof end;

theorem Th85: :: ORDINAL7:72

for a, b being Ordinal st ( a <> 0 implies omega -exponent b in omega -exponent (last (CantorNF a)) ) holds
a (+) b = a +^ b

proof end;

theorem Th86: :: ORDINAL7:73

for a, b being Ordinal
for n being Nat st ( a <> 0 implies b c= omega -exponent (last (CantorNF a)) ) holds
a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))

proof end;

theorem :: ORDINAL7:74

for a being Ordinal
for n, m being Nat holds (n *^ (exp (omega,a))) (+) (m *^ (exp (omega,a))) = (n + m) *^ (exp (omega,a))

proof end;

theorem Th88: :: ORDINAL7:75

for a being Ordinal
for n being Nat holds a (+) n = a +^ n

proof end;

theorem Th89: :: ORDINAL7:76

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

proof end;

registration

let n, m be Nat;

identify n (+) m with n + m;

correctness
compatibility
n (+) m = n + m;
by Th89;

end;

theorem Th90: :: ORDINAL7:77

for a being Ordinal holds a (+) 1 = succ a

proof end;

theorem :: ORDINAL7:78

for a, b being Ordinal holds a (+) (succ b) = succ (a (+) b)

proof end;

registration

let a be empty Ordinal;

cluster a (+) a -> empty ;

coherence
a (+) a is empty ;

end;

registration

let a be non empty Ordinal;
let b be Ordinal;

cluster a (+) b -> non empty ;

coherence
not a (+) b is empty

proof end;

end;

theorem Th92: :: ORDINAL7:79

for a being Ordinal holds
( a is limit_ordinal iff not 0 in rng (omega -exponent (CantorNF a)) )

proof end;

registration

let a, b be limit_ordinal Ordinal;

cluster a (+) b -> limit_ordinal ;

coherence
a (+) b is limit_ordinal

proof end;

end;

registration

let a be Ordinal;
let b be non limit_ordinal Ordinal;

cluster a (+) b -> non limit_ordinal ;

coherence
not a (+) b is limit_ordinal

proof end;

end;

theorem :: ORDINAL7:80

for a, b being Ordinal
for n being non zero Nat st n *^ (exp (omega,b)) c= a & a in (n + 1) *^ (exp (omega,b)) holds
(CantorNF a) . 0 = n *^ (exp (omega,b))

proof end;

theorem :: ORDINAL7:81

for a, b being Ordinal st rng (omega -exponent (CantorNF a)) = rng (omega -exponent (CantorNF b)) holds
for c being Ordinal st c in dom (CantorNF a) holds
(omega -leading_coeff (CantorNF (a (+) b))) . c = ((omega -leading_coeff (CantorNF a)) . c) + ((omega -leading_coeff (CantorNF b)) . c)

proof end;

theorem Th95: :: ORDINAL7:82

for a, b being Ordinal holds
( ( omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF a)) implies omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF a)) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF b)) implies omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF b)) . 0 ) )

proof end;

theorem :: ORDINAL7:83

for a, b being Ordinal holds
( ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = (CantorNF a) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) ) )

proof end;

theorem Th97: :: ORDINAL7:84

for a, b being Ordinal
for x being object holds (omega -exponent (CantorNF a)) . x c= (omega -exponent (CantorNF (a (+) b))) . x

proof end;

theorem Th98: :: ORDINAL7:85

for a, b being Ordinal
for x being object holds (CantorNF a) . x c= (CantorNF (a (+) b)) . x

proof end;

theorem Th99: :: ORDINAL7:86

for a, b being Ordinal holds a c= a (+) b

proof end;

theorem Th100: :: ORDINAL7:87

for a, b being Ordinal holds omega -exponent (a (+) b) = (omega -exponent a) \/ (omega -exponent b)

proof end;

:: closure of natural addition

theorem Th101: :: ORDINAL7:88

for a, b, c being Ordinal st a in exp (omega,c) & b in exp (omega,c) holds
a (+) b in exp (omega,c)

proof end;

Lm9: for a being Ordinal
for n being Nat holds (n *^ (exp (omega,a))) +^ (exp (omega,a)) = (n *^ (exp (omega,a))) (+) (exp (omega,a))

proof end;

scheme :: ORDINAL7:sch 1
OrdinalCNFIndA{ P₁[ non empty Ordinal] } :

for a being non empty Ordinal holds P₁[a]

provided

A1: for a being Ordinal
for n being non zero Nat holds P₁[n *^ (exp (omega,a))] and
A2: for a being Ordinal
for b being non empty Ordinal
for n being non zero Nat st P₁[b] & not a in rng (omega -exponent (CantorNF b)) holds
P₁[b (+) (n *^ (exp (omega,a)))]

proof end;

scheme :: ORDINAL7:sch 2
OrdinalCNFIndB{ P₁[ non empty Ordinal] } :

for a being non empty Ordinal holds P₁[a]

provided

A1: for a being Ordinal holds P₁[ exp (omega,a)] and
A2: for a being Ordinal
for n being non zero Nat st P₁[n *^ (exp (omega,a))] holds
P₁[(n + 1) *^ (exp (omega,a))] and
A3: for a being Ordinal
for b being non empty Ordinal
for n being non zero Nat st P₁[b] & not a in rng (omega -exponent (CantorNF b)) holds
P₁[b (+) (n *^ (exp (omega,a)))]

proof end;

scheme :: ORDINAL7:sch 3
OrdinalCNFIndC{ P₁[ non empty Ordinal] } :

for a being non empty Ordinal holds P₁[a]

provided

A1: for a being Ordinal holds P₁[ exp (omega,a)] and
A2: for a being Ordinal
for b being non empty Ordinal st P₁[b] holds
P₁[b (+) (exp (omega,a))]

proof end;

theorem Th102: :: ORDINAL7:89

for a, b being Ordinal st omega -exponent a in omega -exponent b holds
a in exp (omega,(omega -exponent b))

proof end;

theorem Th103: :: ORDINAL7:90

for a, b being non empty Ordinal holds
( omega *^ a c= b iff omega -exponent a in omega -exponent b )

proof end;

theorem :: ORDINAL7:91

for a, b being Ordinal st omega -exponent a in omega -exponent b holds
b -^ a = b

proof end;

theorem :: ORDINAL7:92

for a, b being Ordinal holds a +^ b c= a (+) b

proof end;

:: cancelling rule for natural addition

theorem :: ORDINAL7:93

for a, b, c being Ordinal st a (+) b = a (+) c holds
b = c

proof end;

Lm10: for A being Cantor-normal-form Ordinal-Sequence holds omega -exponent A is XFinSequence of sup (omega -exponent A)

proof end;

Lm11: for a being non empty Ordinal
for b, c being Ordinal st b in c & (CantorNF b) . 0 <> (CantorNF c) . 0 holds
a (+) b in a (+) c

proof end;

:: monotonicity of natural addition

theorem Th107: :: ORDINAL7:94

for a, b, c being Ordinal st b in c holds
a (+) b in a (+) c

proof end;

theorem :: ORDINAL7:95

for a, b, c being Ordinal st b c= c holds
a (+) b c= a (+) c

proof end;