:: Ordinal Arithmetics :: by Grzegorz Bancerek :: :: Received March 1, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ORDINAL2, ORDINAL1, TARSKI, XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, SUBSET_1, ORDINAL3, CARD_1; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, SETFAM_1, ORDINAL2; constructors SETFAM_1, ORDINAL2, XTUPLE_0; registrations XBOOLE_0, ORDINAL1, ORDINAL2; requirements SUBSET, BOOLE, NUMERALS; begin reserve fi,psi for Ordinal-Sequence, A,A1,B,C,D for Ordinal, X,Y for set, x,y for object; theorem :: ORDINAL3:1 X c= succ X; theorem :: ORDINAL3:2 succ X c= Y implies X c= Y; theorem :: ORDINAL3:3 A in B iff succ A in succ B; theorem :: ORDINAL3:4 X c= A implies union X is epsilon-transitive epsilon-connected set; theorem :: ORDINAL3:5 union On X is epsilon-transitive epsilon-connected set; theorem :: ORDINAL3:6 X c= A implies On X = X; theorem :: ORDINAL3:7 On {A} = {A}; theorem :: ORDINAL3:8 A <> {} implies {} in A; theorem :: ORDINAL3:9 inf A = {}; theorem :: ORDINAL3:10 inf {A} = A; theorem :: ORDINAL3:11 X c= A implies meet X is Ordinal; registration let A,B; cluster A \/ B -> ordinal; cluster A /\ B -> ordinal; end; theorem :: ORDINAL3:12 A \/ B = A or A \/ B = B; theorem :: ORDINAL3:13 A /\ B = A or A /\ B = B; theorem :: ORDINAL3:14 A in 1 implies A = {}; theorem :: ORDINAL3:15 1 = {{}}; theorem :: ORDINAL3:16 A c= 1 implies A = {} or A = 1; theorem :: ORDINAL3:17 (A c= B or A in B) & C in D implies A+^C in B+^D; theorem :: ORDINAL3:18 A c= B & C c= D implies A+^C c= B+^D; theorem :: ORDINAL3:19 A in B & (C c= D & D <> {} or C in D) implies A*^C in B*^D; theorem :: ORDINAL3:20 A c= B & C c= D implies A*^C c= B*^D; theorem :: ORDINAL3:21 B+^C = B+^D implies C = D; theorem :: ORDINAL3:22 B+^C in B+^D implies C in D; theorem :: ORDINAL3:23 B+^C c= B+^D implies C c= D; theorem :: ORDINAL3:24 A c= A+^B & B c= A+^B; theorem :: ORDINAL3:25 A in B implies A in B+^C & A in C+^B; theorem :: ORDINAL3:26 A+^B = {} implies A = {} & B = {}; theorem :: ORDINAL3:27 A c= B implies ex C st B = A+^C; theorem :: ORDINAL3:28 A in B implies ex C st B = A+^C & C <> {}; theorem :: ORDINAL3:29 A <> {} & A is limit_ordinal implies B+^A is limit_ordinal; theorem :: ORDINAL3:30 A+^B+^C = A+^(B+^C); theorem :: ORDINAL3:31 A*^B = {} implies A = {} or B = {}; theorem :: ORDINAL3:32 A in B & C <> {} implies A in B*^C & A in C*^B; theorem :: ORDINAL3:33 B*^A = C*^A & A <> {} implies B = C; theorem :: ORDINAL3:34 B*^A in C*^A implies B in C; theorem :: ORDINAL3:35 B*^A c= C*^A & A <> {} implies B c= C; theorem :: ORDINAL3:36 B <> {} implies A c= A*^B & A c= B*^A; theorem :: ORDINAL3:37 A*^B = 1 implies A = 1 & B = 1; theorem :: ORDINAL3:38 A in B+^C implies A in B or ex D st D in C & A = B+^D; definition let C,fi; func C+^fi -> Ordinal-Sequence means :: ORDINAL3:def 1 dom it = dom fi & for A st A in dom fi holds it.A = C+^(fi.A); func fi+^C -> Ordinal-Sequence means :: ORDINAL3:def 2 dom it = dom fi & for A st A in dom fi holds it.A = (fi.A)+^C; func C*^fi -> Ordinal-Sequence means :: ORDINAL3:def 3 dom it = dom fi & for A st A in dom fi holds it.A = C*^(fi.A); func fi*^C -> Ordinal-Sequence means :: ORDINAL3:def 4 dom it = dom fi & for A st A in dom fi holds it.A = (fi.A)*^C; end; theorem :: ORDINAL3:39 {} <> dom fi & dom fi = dom psi & (for A,B st A in dom fi & B = fi.A holds psi.A = C+^B) implies sup psi = C+^sup fi; theorem :: ORDINAL3:40 A is limit_ordinal implies A*^B is limit_ordinal; theorem :: ORDINAL3:41 A in B*^C & B is limit_ordinal implies ex D st D in B & A in D*^ C; theorem :: ORDINAL3:42 dom fi = dom psi & C <> {} & sup fi is limit_ordinal & (for A,B st A in dom fi & B = fi.A holds psi.A = B*^C) implies sup psi = (sup fi)*^C; theorem :: ORDINAL3:43 {} <> dom fi implies sup (C+^fi) = C+^sup fi; theorem :: ORDINAL3:44 {} <> dom fi & C <> {} & sup fi is limit_ordinal implies sup (fi *^C) = (sup fi)*^C; theorem :: ORDINAL3:45 B <> {} implies union(A+^B) = A+^union B; theorem :: ORDINAL3:46 (A+^B)*^C = A*^C +^ B*^C; theorem :: ORDINAL3:47 A <> {} implies ex C,D st B = C*^A+^D & D in A; theorem :: ORDINAL3:48 for C1,D1,C2,D2 being Ordinal st C1*^A+^D1 = C2*^A+^D2 & D1 in A & D2 in A holds C1 = C2 & D1 = D2; theorem :: ORDINAL3:49 1 in B & A <> {} & A is limit_ordinal implies for fi st dom fi = A & for C st C in A holds fi.C = C*^B holds A*^B = sup fi; theorem :: ORDINAL3:50 (A*^B)*^C = A*^(B*^C); definition let A,B; func A -^ B -> Ordinal means :: ORDINAL3:def 5 A = B+^it if B c= A otherwise it = {}; func A div^ B -> Ordinal means :: ORDINAL3:def 6 ex C st A = it*^B+^C & C in B if B <> {} otherwise it = {}; end; definition let A,B; func A mod^ B -> Ordinal equals :: ORDINAL3:def 7 A-^(A div^ B)*^B; end; theorem :: ORDINAL3:51 A in B implies B = A+^(B-^A); theorem :: ORDINAL3:52 A+^B-^A = B; theorem :: ORDINAL3:53 A in B & (C c= A or C in A) implies A-^C in B-^C; theorem :: ORDINAL3:54 A-^A = {}; theorem :: ORDINAL3:55 A in B implies B-^A <> {} & {} in B-^A; theorem :: ORDINAL3:56 A-^{} = A & {}-^A = {}; theorem :: ORDINAL3:57 A-^(B+^C) = (A-^B)-^C; theorem :: ORDINAL3:58 A c= B implies C-^B c= C-^A; theorem :: ORDINAL3:59 A c= B implies A-^C c= B-^C; theorem :: ORDINAL3:60 C <> {} & A in B+^C implies A-^B in C; theorem :: ORDINAL3:61 A+^B in C implies B in C-^A; theorem :: ORDINAL3:62 A c= B+^(A-^B); theorem :: ORDINAL3:63 A*^C -^ B*^C = (A-^B)*^C; theorem :: ORDINAL3:64 (A div^ B)*^B c= A; theorem :: ORDINAL3:65 A = (A div^ B)*^B+^(A mod^ B); theorem :: ORDINAL3:66 A = B*^C+^D & D in C implies B = A div^ C & D = A mod^ C; theorem :: ORDINAL3:67 A in B*^C implies A div^ C in B & A mod^ C in C; theorem :: ORDINAL3:68 B <> {} implies A*^B div^ B = A; theorem :: ORDINAL3:69 A*^B mod^ B = {}; theorem :: ORDINAL3:70 {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A; theorem :: ORDINAL3:71 A div^ 1 = A & A mod^ 1 = {}; begin :: Addenda :: from ZF_REFLE, 2007.03.13, A.T. theorem :: ORDINAL3:72 sup X c= succ union On X; :: from ZFREFLE1, 2007.03.14, A.T. reserve e,u for set; theorem :: ORDINAL3:73 succ A is_cofinal_with 1; :: from ARYTM_3, 2007.10.23, A.T. theorem :: ORDINAL3:74 for a,b being Ordinal st a+^b is natural holds a in omega & b in omega; registration let a, b be natural Ordinal; cluster a -^ b -> natural; cluster a *^ b -> natural; end; theorem :: ORDINAL3:75 for a,b being Ordinal st a*^b is natural non empty holds a in omega & b in omega; definition let a,b be natural Ordinal; redefine func a+^b; commutativity; end; definition let a,b be natural Ordinal; redefine func a*^b; commutativity; end;