:: 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 proofend; theorem :: ORDINAL3:3 for A, B being Ordinal holds ( A in B iff succ A in succ B ) proofend; theorem :: ORDINAL3:4 for A being Ordinal for X being set st X c= A holds union X is Ordinal proofend; theorem Th5: :: ORDINAL3:5 for X being set holds union (On X) is Ordinal proofend; theorem Th6: :: ORDINAL3:6 for A being Ordinal for X being set st X c= A holds On X = X proofend; theorem Th7: :: ORDINAL3:7 for A being Ordinal holds On {A} = {A} proofend; theorem Th8: :: ORDINAL3:8 for A being Ordinal st A <> {} holds {} in A proofend; theorem :: ORDINAL3:9 for A being Ordinal holds inf A = {} proofend; theorem :: ORDINAL3:10 for A being Ordinal holds inf {A} = A proofend; theorem :: ORDINAL3:11 for A being Ordinal for X being set st X c= A holds meet X is Ordinal proofend; registration let A, B be Ordinal; clusterA \/ B -> ordinal ; coherence A \/ B is ordinal proofend; clusterA /\ B -> ordinal ; coherence A /\ B is ordinal proofend; end; theorem :: ORDINAL3:12 for A, B being Ordinal holds ( A \/ B = A or A \/ B = B ) proofend; theorem :: ORDINAL3:13 for A, B being Ordinal holds ( A /\ B = A or A /\ B = B ) proofend; Lm1: 1 = succ {} ; theorem Th14: :: ORDINAL3:14 for A being Ordinal st A in 1 holds A = {} proofend; theorem :: ORDINAL3:15 1 = {{}} by Lm1; theorem Th16: :: ORDINAL3:16 for A being Ordinal holds ( not A c= 1 or A = {} or A = 1 ) proofend; 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 proofend; theorem :: ORDINAL3:18 for A, B, C, D being Ordinal st A c= B & C c= D holds A +^ C c= B +^ D proofend; 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 proofend; theorem :: ORDINAL3:20 for A, B, C, D being Ordinal st A c= B & C c= D holds A *^ C c= B *^ D proofend; theorem Th21: :: ORDINAL3:21 for B, C, D being Ordinal st B +^ C = B +^ D holds C = D proofend; theorem Th22: :: ORDINAL3:22 for B, C, D being Ordinal st B +^ C in B +^ D holds C in D proofend; theorem Th23: :: ORDINAL3:23 for B, C, D being Ordinal st B +^ C c= B +^ D holds C c= D proofend; theorem Th24: :: ORDINAL3:24 for A, B being Ordinal holds ( A c= A +^ B & B c= A +^ B ) proofend; theorem :: ORDINAL3:25 for A, B, C being Ordinal st A in B holds ( A in B +^ C & A in C +^ B ) proofend; theorem Th26: :: ORDINAL3:26 for A, B being Ordinal st A +^ B = {} holds ( A = {} & B = {} ) proofend; theorem Th27: :: ORDINAL3:27 for A, B being Ordinal st A c= B holds ex C being Ordinal st B = A +^ C proofend; theorem Th28: :: ORDINAL3:28 for A, B being Ordinal st A in B holds ex C being Ordinal st ( B = A +^ C & C <> {} ) proofend; theorem Th29: :: ORDINAL3:29 for A, B being Ordinal st A <> {} & A is limit_ordinal holds B +^ A is limit_ordinal proofend; theorem Th30: :: ORDINAL3:30 for A, B, C being Ordinal holds (A +^ B) +^ C = A +^ (B +^ C) proofend; theorem :: ORDINAL3:31 for A, B being Ordinal holds ( not A *^ B = {} or A = {} or B = {} ) proofend; theorem :: ORDINAL3:32 for A, B, C being Ordinal st A in B & C <> {} holds ( A in B *^ C & A in C *^ B ) proofend; theorem Th33: :: ORDINAL3:33 for B, A, C being Ordinal st B *^ A = C *^ A & A <> {} holds B = C proofend; theorem Th34: :: ORDINAL3:34 for B, A, C being Ordinal st B *^ A in C *^ A holds B in C proofend; theorem Th35: :: ORDINAL3:35 for B, A, C being Ordinal st B *^ A c= C *^ A & A <> {} holds B c= C proofend; theorem Th36: :: ORDINAL3:36 for B, A being Ordinal st B <> {} holds ( A c= A *^ B & A c= B *^ A ) proofend; theorem :: ORDINAL3:37 for A, B being Ordinal st A *^ B = 1 holds ( A = 1 & B = 1 ) proofend; 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 ) ) proofend; definition let C be Ordinal; let fi be Ordinal-Sequence; funcC +^ 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) ) ) proofend; 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 proofend; funcfi +^ 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 ) ) proofend; 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 proofend; funcC *^ 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) ) ) proofend; 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 proofend; funcfi *^ 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 ) ) proofend; 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 proofend; 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) proofend; theorem Th40: :: ORDINAL3:40 for A, B being Ordinal st A is limit_ordinal holds A *^ B is limit_ordinal proofend; 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 ) proofend; 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 proofend; theorem Th43: :: ORDINAL3:43 for fi being Ordinal-Sequence for C being Ordinal st {} <> dom fi holds sup (C +^ fi) = C +^ (sup fi) proofend; 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 proofend; theorem Th45: :: ORDINAL3:45 for B, A being Ordinal st B <> {} holds union (A +^ B) = A +^ (union B) proofend; theorem Th46: :: ORDINAL3:46 for A, B, C being Ordinal holds (A +^ B) *^ C = (A *^ C) +^ (B *^ C) proofend; 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 ) proofend; 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 ) proofend; 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 proofend; theorem :: ORDINAL3:50 for A, B, C being Ordinal holds (A *^ B) *^ C = A *^ (B *^ C) proofend; definition let A, B be Ordinal; funcA -^ 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 ; funcA 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; funcA 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) proofend; theorem Th52: :: ORDINAL3:52 for A, B being Ordinal holds (A +^ B) -^ A = B proofend; 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 proofend; theorem Th54: :: ORDINAL3:54 for A being Ordinal holds A -^ A = {} proofend; theorem :: ORDINAL3:55 for A, B being Ordinal st A in B holds ( B -^ A <> {} & {} in B -^ A ) proofend; theorem Th56: :: ORDINAL3:56 for A being Ordinal holds ( A -^ {} = A & {} -^ A = {} ) proofend; theorem :: ORDINAL3:57 for A, B, C being Ordinal holds A -^ (B +^ C) = (A -^ B) -^ C proofend; theorem :: ORDINAL3:58 for A, B, C being Ordinal st A c= B holds C -^ B c= C -^ A proofend; theorem :: ORDINAL3:59 for A, B, C being Ordinal st A c= B holds A -^ C c= B -^ C proofend; theorem :: ORDINAL3:60 for C, A, B being Ordinal st C <> {} & A in B +^ C holds A -^ B in C proofend; theorem :: ORDINAL3:61 for A, B, C being Ordinal st A +^ B in C holds B in C -^ A proofend; theorem :: ORDINAL3:62 for A, B being Ordinal holds A c= B +^ (A -^ B) proofend; theorem :: ORDINAL3:63 for A, C, B being Ordinal holds (A *^ C) -^ (B *^ C) = (A -^ B) *^ C proofend; theorem Th64: :: ORDINAL3:64 for A, B being Ordinal holds (A div^ B) *^ B c= A proofend; theorem Th65: :: ORDINAL3:65 for A, B being Ordinal holds A = ((A div^ B) *^ B) +^ (A mod^ B) proofend; 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 ) proofend; 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 ) proofend; theorem Th68: :: ORDINAL3:68 for B, A being Ordinal st B <> {} holds (A *^ B) div^ B = A proofend; theorem :: ORDINAL3:69 for A, B being Ordinal holds (A *^ B) mod^ B = {} proofend; theorem :: ORDINAL3:70 for A being Ordinal holds ( {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A ) proofend; theorem :: ORDINAL3:71 for A being Ordinal holds ( A div^ 1 = A & A mod^ 1 = {} ) proofend; begin :: from ZF_REFLE, 2007.03.13, A.T. theorem :: ORDINAL3:72 for X being set holds sup X c= succ (union (On X)) proofend; theorem :: ORDINAL3:73 for A being Ordinal holds succ A is_cofinal_with 1 proofend; :: 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 ) proofend; registration let a, b be natural Ordinal; clustera -^ b -> natural ; coherence a -^ b is natural proofend; clustera *^ b -> natural ; coherence a *^ b is natural proofend; 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 ) proofend; definition let a, b be natural Ordinal; :: original:+^ redefine funca +^ b -> set ; commutativity for a, b being natural Ordinal holds a +^ b = b +^ a proofend; end; definition let a, b be natural Ordinal; :: original:*^ redefine funca *^ b -> set ; commutativity for a, b being natural Ordinal holds a *^ b = b *^ a proofend; end;