:: Ordinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received March 1, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem :: ORDINAL3:1
for X being set holds X c= succ X by XBOOLE_1:7;

theorem :: ORDINAL3:2
for X, Y being set st succ X c= Y holds
X c= Y
proof end;

theorem :: ORDINAL3:3
for A, B being Ordinal holds
( A in B iff succ A in succ B )
proof end;

theorem :: ORDINAL3:4
for A being Ordinal
for X being set st X c= A holds
union X is Ordinal
proof end;

theorem Th5: :: ORDINAL3:5
for X being set holds union (On X) is Ordinal
proof end;

theorem Th6: :: ORDINAL3:6
for A being Ordinal
for X being set st X c= A holds
On X = X
proof end;

theorem Th7: :: ORDINAL3:7
for A being Ordinal holds On {A} = {A}
proof end;

theorem Th8: :: ORDINAL3:8
for A being Ordinal st A <> {} holds
{} in A
proof end;

theorem :: ORDINAL3:9
for A being Ordinal holds inf A = {}
proof end;

theorem :: ORDINAL3:10
for A being Ordinal holds inf {A} = A
proof end;

theorem :: ORDINAL3:11
for A being Ordinal
for X being set st X c= A holds
meet X is Ordinal
proof end;

registration
let A, B be Ordinal;
cluster A \/ B -> ordinal ;
coherence
A \/ B is ordinal
proof end;
cluster A /\ B -> ordinal ;
coherence
A /\ B is ordinal
proof end;
end;

theorem :: ORDINAL3:12
for A, B being Ordinal holds
( A \/ B = A or A \/ B = B )
proof end;

theorem :: ORDINAL3:13
for A, B being Ordinal holds
( A /\ B = A or A /\ B = B )
proof end;

Lm1: 1 = succ {}
;

theorem Th14: :: ORDINAL3:14
for A being Ordinal st A in 1 holds
A = {}
proof end;

theorem :: ORDINAL3:15
1 = {{}} by Lm1;

theorem Th16: :: ORDINAL3:16
for A being Ordinal holds
( not A c= 1 or A = {} or A = 1 )
proof end;

theorem :: ORDINAL3:17
for A, B, C, D being Ordinal st ( A c= B or A in B ) & C in D holds
A +^ C in B +^ D
proof end;

theorem :: ORDINAL3:18
for A, B, C, D being Ordinal st A c= B & C c= D holds
A +^ C c= B +^ D
proof end;

theorem Th19: :: ORDINAL3:19
for A, B, C, D being Ordinal st A in B & ( ( C c= D & D <> {} ) or C in D ) holds
A *^ C in B *^ D
proof end;

theorem :: ORDINAL3:20
for A, B, C, D being Ordinal st A c= B & C c= D holds
A *^ C c= B *^ D
proof end;

theorem Th21: :: ORDINAL3:21
for B, C, D being Ordinal st B +^ C = B +^ D holds
C = D
proof end;

theorem Th22: :: ORDINAL3:22
for B, C, D being Ordinal st B +^ C in B +^ D holds
C in D
proof end;

theorem Th23: :: ORDINAL3:23
for B, C, D being Ordinal st B +^ C c= B +^ D holds
C c= D
proof end;

theorem Th24: :: ORDINAL3:24
for A, B being Ordinal holds
( A c= A +^ B & B c= A +^ B )
proof end;

theorem :: ORDINAL3:25
for A, B, C being Ordinal st A in B holds
( A in B +^ C & A in C +^ B )
proof end;

theorem Th26: :: ORDINAL3:26
for A, B being Ordinal st A +^ B = {} holds
( A = {} & B = {} )
proof end;

theorem Th27: :: ORDINAL3:27
for A, B being Ordinal st A c= B holds
ex C being Ordinal st B = A +^ C
proof end;

theorem Th28: :: ORDINAL3:28
for A, B being Ordinal st A in B holds
ex C being Ordinal st
( B = A +^ C & C <> {} )
proof end;

theorem Th29: :: ORDINAL3:29
for A, B being Ordinal st A <> {} & A is limit_ordinal holds
B +^ A is limit_ordinal
proof end;

theorem Th30: :: ORDINAL3:30
for A, B, C being Ordinal holds (A +^ B) +^ C = A +^ (B +^ C)
proof end;

theorem :: ORDINAL3:31
for A, B being Ordinal holds
( not A *^ B = {} or A = {} or B = {} )
proof end;

theorem :: ORDINAL3:32
for A, B, C being Ordinal st A in B & C <> {} holds
( A in B *^ C & A in C *^ B )
proof end;

theorem Th33: :: ORDINAL3:33
for B, A, C being Ordinal st B *^ A = C *^ A & A <> {} holds
B = C
proof end;

theorem Th34: :: ORDINAL3:34
for B, A, C being Ordinal st B *^ A in C *^ A holds
B in C
proof end;

theorem Th35: :: ORDINAL3:35
for B, A, C being Ordinal st B *^ A c= C *^ A & A <> {} holds
B c= C
proof end;

theorem Th36: :: ORDINAL3:36
for B, A being Ordinal st B <> {} holds
( A c= A *^ B & A c= B *^ A )
proof end;

theorem :: ORDINAL3:37
for A, B being Ordinal st A *^ B = 1 holds
( A = 1 & B = 1 )
proof end;

theorem Th38: :: ORDINAL3:38
for A, B, C being Ordinal holds
( not A in B +^ C or A in B or ex D being Ordinal st
( D in C & A = B +^ D ) )
proof end;

definition
let C be Ordinal;
let fi be Ordinal-Sequence;
func C +^ fi -> Ordinal-Sequence means :Def1: :: ORDINAL3:def 1
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = C +^ (fi . A) ) );
existence
ex b1 being Ordinal-Sequence st
( dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = C +^ (fi . A) ) )
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence st dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = C +^ (fi . A) ) & dom b2 = dom fi & ( for A being Ordinal st A in dom fi holds
b2 . A = C +^ (fi . A) ) holds
b1 = b2
proof end;
func fi +^ C -> Ordinal-Sequence means :: ORDINAL3:def 2
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = (fi . A) +^ C ) );
existence
ex b1 being Ordinal-Sequence st
( dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = (fi . A) +^ C ) )
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence st dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = (fi . A) +^ C ) & dom b2 = dom fi & ( for A being Ordinal st A in dom fi holds
b2 . A = (fi . A) +^ C ) holds
b1 = b2
proof end;
func C *^ fi -> Ordinal-Sequence means :: ORDINAL3:def 3
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = C *^ (fi . A) ) );
existence
ex b1 being Ordinal-Sequence st
( dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = C *^ (fi . A) ) )
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence st dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = C *^ (fi . A) ) & dom b2 = dom fi & ( for A being Ordinal st A in dom fi holds
b2 . A = C *^ (fi . A) ) holds
b1 = b2
proof end;
func fi *^ C -> Ordinal-Sequence means :Def4: :: ORDINAL3:def 4
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = (fi . A) *^ C ) );
existence
ex b1 being Ordinal-Sequence st
( dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = (fi . A) *^ C ) )
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence st dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = (fi . A) *^ C ) & dom b2 = dom fi & ( for A being Ordinal st A in dom fi holds
b2 . A = (fi . A) *^ C ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines +^ ORDINAL3:def 1 :
for C being Ordinal
for fi, b3 being Ordinal-Sequence holds
( b3 = C +^ fi iff ( dom b3 = dom fi & ( for A being Ordinal st A in dom fi holds
b3 . A = C +^ (fi . A) ) ) );

:: deftheorem defines +^ ORDINAL3:def 2 :
for C being Ordinal
for fi, b3 being Ordinal-Sequence holds
( b3 = fi +^ C iff ( dom b3 = dom fi & ( for A being Ordinal st A in dom fi holds
b3 . A = (fi . A) +^ C ) ) );

:: deftheorem defines *^ ORDINAL3:def 3 :
for C being Ordinal
for fi, b3 being Ordinal-Sequence holds
( b3 = C *^ fi iff ( dom b3 = dom fi & ( for A being Ordinal st A in dom fi holds
b3 . A = C *^ (fi . A) ) ) );

:: deftheorem Def4 defines *^ ORDINAL3:def 4 :
for C being Ordinal
for fi, b3 being Ordinal-Sequence holds
( b3 = fi *^ C iff ( dom b3 = dom fi & ( for A being Ordinal st A in dom fi holds
b3 . A = (fi . A) *^ C ) ) );

theorem Th39: :: ORDINAL3:39
for fi, psi being Ordinal-Sequence
for C being Ordinal st {} <> dom fi & dom fi = dom psi & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = C +^ B ) holds
sup psi = C +^ (sup fi)
proof end;

theorem Th40: :: ORDINAL3:40
for A, B being Ordinal st A is limit_ordinal holds
A *^ B is limit_ordinal
proof end;

theorem Th41: :: ORDINAL3:41
for A, B, C being Ordinal st A in B *^ C & B is limit_ordinal holds
ex D being Ordinal st
( D in B & A in D *^ C )
proof end;

theorem Th42: :: ORDINAL3:42
for fi, psi being Ordinal-Sequence
for C being Ordinal st dom fi = dom psi & C <> {} & sup fi is limit_ordinal & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = B *^ C ) holds
sup psi = (sup fi) *^ C
proof end;

theorem Th43: :: ORDINAL3:43
for fi being Ordinal-Sequence
for C being Ordinal st {} <> dom fi holds
sup (C +^ fi) = C +^ (sup fi)
proof end;

theorem Th44: :: ORDINAL3:44
for fi being Ordinal-Sequence
for C being Ordinal st {} <> dom fi & C <> {} & sup fi is limit_ordinal holds
sup (fi *^ C) = (sup fi) *^ C
proof end;

theorem Th45: :: ORDINAL3:45
for B, A being Ordinal st B <> {} holds
union (A +^ B) = A +^ (union B)
proof end;

theorem Th46: :: ORDINAL3:46
for A, B, C being Ordinal holds (A +^ B) *^ C = (A *^ C) +^ (B *^ C)
proof end;

theorem Th47: :: ORDINAL3:47
for A, B being Ordinal st A <> {} holds
ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A )
proof end;

theorem Th48: :: ORDINAL3:48
for A, C1, D1, C2, D2 being Ordinal st (C1 *^ A) +^ D1 = (C2 *^ A) +^ D2 & D1 in A & D2 in A holds
( C1 = C2 & D1 = D2 )
proof end;

theorem Th49: :: ORDINAL3:49
for B, A being Ordinal st 1 in B & A <> {} & A is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for C being Ordinal st C in A holds
fi . C = C *^ B ) holds
A *^ B = sup fi
proof end;

theorem :: ORDINAL3:50
for A, B, C being Ordinal holds (A *^ B) *^ C = A *^ (B *^ C)
proof end;

definition
let A, B be Ordinal;
func A -^ B -> Ordinal means :Def5: :: ORDINAL3:def 5
A = B +^ it if B c= A
otherwise it = {} ;
existence
( ( B c= A implies ex b1 being Ordinal st A = B +^ b1 ) & ( not B c= A implies ex b1 being Ordinal st b1 = {} ) )
by Th27;
uniqueness
for b1, b2 being Ordinal holds
( ( B c= A & A = B +^ b1 & A = B +^ b2 implies b1 = b2 ) & ( not B c= A & b1 = {} & b2 = {} implies b1 = b2 ) )
by Th21;
consistency
for b1 being Ordinal holds verum
;
func A div^ B -> Ordinal means :Def6: :: ORDINAL3:def 6
ex C being Ordinal st
( A = (it *^ B) +^ C & C in B ) if B <> {}
otherwise it = {} ;
consistency
for b1 being Ordinal holds verum
;
existence
( ( B <> {} implies ex b1, C being Ordinal st
( A = (b1 *^ B) +^ C & C in B ) ) & ( not B <> {} implies ex b1 being Ordinal st b1 = {} ) )
by Th47;
uniqueness
for b1, b2 being Ordinal holds
( ( B <> {} & ex C being Ordinal st
( A = (b1 *^ B) +^ C & C in B ) & ex C being Ordinal st
( A = (b2 *^ B) +^ C & C in B ) implies b1 = b2 ) & ( not B <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
by Th48;
end;

:: deftheorem Def5 defines -^ ORDINAL3:def 5 :
for A, B, b3 being Ordinal holds
( ( B c= A implies ( b3 = A -^ B iff A = B +^ b3 ) ) & ( not B c= A implies ( b3 = A -^ B iff b3 = {} ) ) );

:: deftheorem Def6 defines div^ ORDINAL3:def 6 :
for A, B, b3 being Ordinal holds
( ( B <> {} implies ( b3 = A div^ B iff ex C being Ordinal st
( A = (b3 *^ B) +^ C & C in B ) ) ) & ( not B <> {} implies ( b3 = A div^ B iff b3 = {} ) ) );

definition
let A, B be Ordinal;
func A mod^ B -> Ordinal equals :: ORDINAL3:def 7
A -^ ((A div^ B) *^ B);
correctness
coherence
A -^ ((A div^ B) *^ B) is Ordinal
;
;
end;

:: deftheorem defines mod^ ORDINAL3:def 7 :
for A, B being Ordinal holds A mod^ B = A -^ ((A div^ B) *^ B);

theorem :: ORDINAL3:51
for A, B being Ordinal st A in B holds
B = A +^ (B -^ A)
proof end;

theorem Th52: :: ORDINAL3:52
for A, B being Ordinal holds (A +^ B) -^ A = B
proof end;

theorem Th53: :: ORDINAL3:53
for A, B, C being Ordinal st A in B & ( C c= A or C in A ) holds
A -^ C in B -^ C
proof end;

theorem Th54: :: ORDINAL3:54
for A being Ordinal holds A -^ A = {}
proof end;

theorem :: ORDINAL3:55
for A, B being Ordinal st A in B holds
( B -^ A <> {} & {} in B -^ A )
proof end;

theorem Th56: :: ORDINAL3:56
for A being Ordinal holds
( A -^ {} = A & {} -^ A = {} )
proof end;

theorem :: ORDINAL3:57
for A, B, C being Ordinal holds A -^ (B +^ C) = (A -^ B) -^ C
proof end;

theorem :: ORDINAL3:58
for A, B, C being Ordinal st A c= B holds
C -^ B c= C -^ A
proof end;

theorem :: ORDINAL3:59
for A, B, C being Ordinal st A c= B holds
A -^ C c= B -^ C
proof end;

theorem :: ORDINAL3:60
for C, A, B being Ordinal st C <> {} & A in B +^ C holds
A -^ B in C
proof end;

theorem :: ORDINAL3:61
for A, B, C being Ordinal st A +^ B in C holds
B in C -^ A
proof end;

theorem :: ORDINAL3:62
for A, B being Ordinal holds A c= B +^ (A -^ B)
proof end;

theorem :: ORDINAL3:63
for A, C, B being Ordinal holds (A *^ C) -^ (B *^ C) = (A -^ B) *^ C
proof end;

theorem Th64: :: ORDINAL3:64
for A, B being Ordinal holds (A div^ B) *^ B c= A
proof end;

theorem Th65: :: ORDINAL3:65
for A, B being Ordinal holds A = ((A div^ B) *^ B) +^ (A mod^ B)
proof end;

theorem :: ORDINAL3:66
for A, B, C, D being Ordinal st A = (B *^ C) +^ D & D in C holds
( B = A div^ C & D = A mod^ C )
proof end;

theorem :: ORDINAL3:67
for A, B, C being Ordinal st A in B *^ C holds
( A div^ C in B & A mod^ C in C )
proof end;

theorem Th68: :: ORDINAL3:68
for B, A being Ordinal st B <> {} holds
(A *^ B) div^ B = A
proof end;

theorem :: ORDINAL3:69
for A, B being Ordinal holds (A *^ B) mod^ B = {}
proof end;

theorem :: ORDINAL3:70
for A being Ordinal holds
( {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A )
proof end;

theorem :: ORDINAL3:71
for A being Ordinal holds
( A div^ 1 = A & A mod^ 1 = {} )
proof end;

begin

:: from ZF_REFLE, 2007.03.13, A.T.
theorem :: ORDINAL3:72
for X being set holds sup X c= succ (union (On X))
proof end;

theorem :: ORDINAL3:73
for A being Ordinal holds succ A is_cofinal_with 1
proof end;

:: from ARYTM_3, 2007.10.23, A.T.
theorem Th74: :: ORDINAL3:74
for a, b being Ordinal st a +^ b is natural holds
( a in omega & b in omega )
proof end;

registration
let a, b be natural Ordinal;
cluster a -^ b -> natural ;
coherence
a -^ b is natural
proof end;
cluster a *^ b -> natural ;
coherence
a *^ b is natural
proof end;
end;

theorem :: ORDINAL3:75
for a, b being Ordinal st a *^ b is natural & not a *^ b is empty holds
( a in omega & b in omega )
proof end;

definition
let a, b be natural Ordinal;
:: original: +^
redefine func a +^ b -> set ;
commutativity
for a, b being natural Ordinal holds a +^ b = b +^ a
proof end;
end;

definition
let a, b be natural Ordinal;
:: original: *^
redefine func a *^ b -> set ;
commutativity
for a, b being natural Ordinal holds a *^ b = b *^ a
proof end;
end;