ORDINAL3: Ordinal Arithmetics

:: Ordinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received March 1, 1990
:: Copyright (c) 1990-2011 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

canceled;

theorem :: ORDINAL3:4

canceled;

theorem :: ORDINAL3:5

for A, B being Ordinal holds
( A in B iff succ A in succ B )

proof end;

theorem :: ORDINAL3:6

for A being Ordinal
for X being set st X c= A holds
union X is Ordinal

proof end;

theorem Th7: :: ORDINAL3:7

for X being set holds union (On X) is Ordinal

proof end;

theorem Th8: :: ORDINAL3:8

for A being Ordinal
for X being set st X c= A holds
On X = X

proof end;

theorem Th9: :: ORDINAL3:9

for A being Ordinal holds On {A} = {A}

proof end;

theorem Th10: :: ORDINAL3:10

for A being Ordinal st A <> {} holds
{} in A

proof end;

theorem :: ORDINAL3:11

for A being Ordinal holds inf A = {}

proof end;

theorem :: ORDINAL3:12

for A being Ordinal holds inf {A} = A

proof end;

theorem :: ORDINAL3:13

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

proof end;

cluster A /\ B -> ordinal ;
coherence

proof end;

end;

theorem :: ORDINAL3:14

canceled;

theorem :: ORDINAL3:15

for A, B being Ordinal holds
( A \/ B = A or A \/ B = B )

proof end;

theorem :: ORDINAL3:16

for A, B being Ordinal holds
( A /\ B = A or A /\ B = B )

proof end;

Lm1: 1 = succ {}
;

theorem Th17: :: ORDINAL3:17

for A being Ordinal st A in 1 holds
A = {}

proof end;

theorem :: ORDINAL3:18

1 = {{}} by Lm1;

theorem Th19: :: ORDINAL3:19

for A being Ordinal holds
( not A c= 1 or A = {} or A = 1 )

proof end;

theorem :: ORDINAL3:20

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:21

for A, B, C, D being Ordinal st A c= B & C c= D holds
A +^ C c= B +^ D

proof end;

theorem Th22: :: ORDINAL3:22

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:23

for A, B, C, D being Ordinal st A c= B & C c= D holds
A *^ C c= B *^ D

proof end;

theorem Th24: :: ORDINAL3:24

for B, C, D being Ordinal st B +^ C = B +^ D holds
C = D

proof end;

theorem Th25: :: ORDINAL3:25

for B, C, D being Ordinal st B +^ C in B +^ D holds
C in D

proof end;

theorem Th26: :: ORDINAL3:26

for B, C, D being Ordinal st B +^ C c= B +^ D holds
C c= D

proof end;

theorem Th27: :: ORDINAL3:27

for A, B being Ordinal holds
( A c= A +^ B & B c= A +^ B )

proof end;

theorem :: ORDINAL3:28

for A, B, C being Ordinal st A in B holds
( A in B +^ C & A in C +^ B )

proof end;

theorem Th29: :: ORDINAL3:29

for A, B being Ordinal st A +^ B = {} holds
( A = {} & B = {} )

proof end;

theorem Th30: :: ORDINAL3:30

for A, B being Ordinal st A c= B holds
ex C being Ordinal st B = A +^ C

proof end;

theorem Th31: :: ORDINAL3:31

for A, B being Ordinal st A in B holds
ex C being Ordinal st
( B = A +^ C & C <> {} )

proof end;

theorem Th32: :: ORDINAL3:32

for A, B being Ordinal st A <> {} & A is limit_ordinal holds
B +^ A is limit_ordinal

proof end;

theorem Th33: :: ORDINAL3:33

for A, B, C being Ordinal holds (A +^ B) +^ C = A +^ (B +^ C)

proof end;

theorem :: ORDINAL3:34

for A, B being Ordinal holds
( not A *^ B = {} or A = {} or B = {} )

proof end;

theorem :: ORDINAL3:35

for A, B, C being Ordinal st A in B & C <> {} holds
( A in B *^ C & A in C *^ B )

proof end;

theorem Th36: :: ORDINAL3:36

for B, A, C being Ordinal st B *^ A = C *^ A & A <> {} holds
B = C

proof end;

theorem Th37: :: ORDINAL3:37

for B, A, C being Ordinal st B *^ A in C *^ A holds
B in C

proof end;

theorem Th38: :: ORDINAL3:38

for B, A, C being Ordinal st B *^ A c= C *^ A & A <> {} holds
B c= C

proof end;

theorem Th39: :: ORDINAL3:39

for B, A being Ordinal st B <> {} holds
( A c= A *^ B & A c= B *^ A )

proof end;

theorem :: ORDINAL3:40

canceled;

theorem :: ORDINAL3:41

for A, B being Ordinal st A *^ B = 1 holds
( A = 1 & B = 1 )

proof end;

theorem Th42: :: ORDINAL3:42

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;
canceled;
func C +^ fi -> Ordinal-Sequence means :Def2: :: ORDINAL3:def 2
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = C +^ (fi . A) ) );
existence

proof end;

proof end;

func fi +^ C -> Ordinal-Sequence means :: ORDINAL3:def 3
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = (fi . A) +^ C ) );
existence

proof end;

proof end;

func C *^ fi -> Ordinal-Sequence means :: ORDINAL3:def 4
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = C *^ (fi . A) ) );
existence

proof end;

proof end;

func fi *^ C -> Ordinal-Sequence means :Def5: :: ORDINAL3:def 5
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = (fi . A) *^ C ) );
existence

proof end;

proof end;

end;

:: deftheorem ORDINAL3:def 1 :

:: deftheorem Def2 defines +^ ORDINAL3:def 2 :

:: deftheorem defines +^ ORDINAL3:def 3 :

:: deftheorem defines *^ ORDINAL3:def 4 :

:: deftheorem Def5 defines *^ ORDINAL3:def 5 :

theorem :: ORDINAL3:43

canceled;

theorem :: ORDINAL3:44

canceled;

theorem :: ORDINAL3:45

canceled;

theorem :: ORDINAL3:46

canceled;

theorem Th47: :: ORDINAL3:47

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 Th48: :: ORDINAL3:48

for A, B being Ordinal st A is limit_ordinal holds
A *^ B is limit_ordinal

proof end;

theorem Th49: :: ORDINAL3:49

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 Th50: :: ORDINAL3:50

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 Th51: :: ORDINAL3:51

for fi being Ordinal-Sequence
for C being Ordinal st {} <> dom fi holds
sup (C +^ fi) = C +^ (sup fi)

proof end;

theorem Th52: :: ORDINAL3:52

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 Th53: :: ORDINAL3:53

for B, A being Ordinal st B <> {} holds
union (A +^ B) = A +^ (union B)

proof end;

theorem Th54: :: ORDINAL3:54

for A, B, C being Ordinal holds (A +^ B) *^ C = (A *^ C) +^ (B *^ C)

proof end;

theorem Th55: :: ORDINAL3:55

for A, B being Ordinal st A <> {} holds
ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A )

proof end;

theorem Th56: :: ORDINAL3:56

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 Th57: :: ORDINAL3:57

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:58

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 :Def6: :: ORDINAL3:def 6
A = B +^ it if B c= A
otherwise it = {} ;
existence by Th30;
uniqueness by Th24;
consistency ;
func A div^ B -> Ordinal means :Def7: :: ORDINAL3:def 7
ex C being Ordinal st
( A = (it *^ B) +^ C & C in B ) if B <> {}
otherwise it = {} ;
consistency ;
existence by Th55;
uniqueness by Th56;

end;

:: deftheorem Def6 defines -^ ORDINAL3:def 6 :

:: deftheorem Def7 defines div^ ORDINAL3:def 7 :

definition

let A, B be Ordinal;
func A mod^ B -> Ordinal equals :: ORDINAL3:def 8
A -^ ((A div^ B) *^ B);
correctness ;

end;

:: deftheorem defines mod^ ORDINAL3:def 8 :

theorem :: ORDINAL3:59

canceled;

theorem :: ORDINAL3:60

for A, B being Ordinal st A in B holds
B = A +^ (B -^ A)

proof end;

theorem :: ORDINAL3:61

canceled;

theorem :: ORDINAL3:62

canceled;

theorem :: ORDINAL3:63

canceled;

theorem :: ORDINAL3:64

canceled;

theorem Th65: :: ORDINAL3:65

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

proof end;

theorem Th66: :: ORDINAL3:66

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 Th67: :: ORDINAL3:67

for A being Ordinal holds A -^ A = {}

proof end;

theorem :: ORDINAL3:68

for A, B being Ordinal st A in B holds
( B -^ A <> {} & {} in B -^ A )

proof end;

theorem Th69: :: ORDINAL3:69

for A being Ordinal holds
( A -^ {} = A & {} -^ A = {} )

proof end;

theorem :: ORDINAL3:70

for A, B, C being Ordinal holds A -^ (B +^ C) = (A -^ B) -^ C

proof end;

theorem :: ORDINAL3:71

for A, B, C being Ordinal st A c= B holds
C -^ B c= C -^ A

proof end;

theorem :: ORDINAL3:72

for A, B, C being Ordinal st A c= B holds
A -^ C c= B -^ C

proof end;

theorem :: ORDINAL3:73

for C, A, B being Ordinal st C <> {} & A in B +^ C holds
A -^ B in C

proof end;

theorem :: ORDINAL3:74

for A, B, C being Ordinal st A +^ B in C holds
B in C -^ A

proof end;

theorem :: ORDINAL3:75

for A, B being Ordinal holds A c= B +^ (A -^ B)

proof end;

theorem :: ORDINAL3:76

for A, C, B being Ordinal holds (A *^ C) -^ (B *^ C) = (A -^ B) *^ C

proof end;

theorem Th77: :: ORDINAL3:77

for A, B being Ordinal holds (A div^ B) *^ B c= A

proof end;

theorem Th78: :: ORDINAL3:78

for A, B being Ordinal holds A = ((A div^ B) *^ B) +^ (A mod^ B)

proof end;

theorem :: ORDINAL3:79

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:80

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 Th81: :: ORDINAL3:81

for B, A being Ordinal st B <> {} holds
(A *^ B) div^ B = A

proof end;

theorem :: ORDINAL3:82

for A, B being Ordinal holds (A *^ B) mod^ B = {}

proof end;

theorem :: ORDINAL3:83

for A being Ordinal holds
( {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A )

proof end;

theorem :: ORDINAL3:84

for A being Ordinal holds
( A div^ 1 = A & A mod^ 1 = {} )

proof end;

begin

theorem :: ORDINAL3:85

for X being set holds sup X c= succ (union (On X))

proof end;

theorem :: ORDINAL3:86

for A being Ordinal holds succ A is_cofinal_with 1

proof end;

theorem Th87: :: ORDINAL3:87

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

proof end;

cluster a *^ b -> natural ;
coherence

proof end;

end;

theorem :: ORDINAL3:88

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

proof end;

end;

definition

let a, b be natural Ordinal;
:: original: *^
redefine func a *^ b -> set ;
commutativity

proof end;

end;