### The Mizar article:

### Non-Negative Real Numbers. Part I

**by****Andrzej Trybulec**

- Received March 7, 1998
Copyright (c) 1998 Association of Mizar Users

- MML identifier: ARYTM_2
- [ MML identifier index ]

environ vocabulary ARYTM_3, BOOLE, ORDINAL2, ORDINAL1, ARYTM_2, HAHNBAN; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, ARYTM_3; constructors ARYTM_3, XBOOLE_0; clusters ARYTM_3, SUBSET_1, ORDINAL1, ORDINAL2, ZFMISC_1, XBOOLE_0; requirements BOOLE, SUBSET; definitions TARSKI, XBOOLE_0, ORDINAL1; theorems XBOOLE_0, ARYTM_3, ZFMISC_1, TARSKI, SUBSET_1, ORDINAL2, ORDINAL1, ORDINAL3, XBOOLE_1; schemes ARYTM_3; begin reserve r,s,t,x',y',z',p,q for Element of RAT+; definition func DEDEKIND_CUTS -> Subset of bool RAT+ equals :Def1: { A where A is Subset of RAT+: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s } \ { RAT+}; coherence proof set C = { A where A is Subset of RAT+: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s }; A1: C \ {RAT+} c= C by XBOOLE_1:36; C c= bool RAT+ proof let e be set; assume e in C; then ex A being Subset of RAT+ st e = A & for r holds r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s; hence thesis; end; hence thesis by A1,XBOOLE_1:1; end; end; definition cluster DEDEKIND_CUTS -> non empty; coherence proof set X = { s: s < one }; now assume one in X; then ex s st s = one & s < one; hence contradiction; end; then A1: X <> RAT+; {} <=' one by ARYTM_3:71; then {} < one by ARYTM_3:75; then A2: {} in X; X c= RAT+ proof let e be set; assume e in X; then ex s st s = e & s < one; hence thesis; end; then reconsider X as non empty Subset of RAT+ by A2; r in X implies (for s st s <=' r holds s in X) & ex s st s in X & r < s proof assume r in X; then A3: ex s st s = r & s < one; thus for s st s <=' r holds s in X proof let s; assume s <=' r; then s < one by A3,ARYTM_3:74; hence thesis; end; consider s such that A4: r < s and A5: s < one by A3,ARYTM_3:101; take s; thus s in X by A5; thus r < s by A4; end; then X in { A where A is Subset of RAT+: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s }; hence thesis by A1,Def1,ZFMISC_1:64; end; end; definition func REAL+ equals :Def2: RAT+ \/ DEDEKIND_CUTS \ {{ s: s < t}: t <> {}}; coherence; end; reserve x,y,z for Element of REAL+; set IR = { A where A is Subset of RAT+: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s}, RA = {{ s: s < t}: t <> {}}; Lm1: not ex x,y being set st [x,y] in IR proof given x,y being set such that A1: [x,y] in IR; consider A being Subset of RAT+ such that A2: [x,y] = A and A3: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s by A1; A = {{x},{x,y}} by A2,TARSKI:def 5; then A4: {x} in A by TARSKI:def 2; for r,s st r in A & s <=' r holds s in A by A3; then consider r1,r2,r3 being Element of RAT+ such that A5: r1 in A & r2 in A & r3 in A and A6: r1 <> r2 & r2 <> r3 & r3 <> r1 by A4,ARYTM_3:82; [x,y] = { { x,y }, { x } } by TARSKI:def 5; then (r1 = { x,y } or r1 = { x }) & (r2 = { x,y } or r2 = { x }) & (r3 = { x,y } or r3 = { x }) by A2,A5,TARSKI:def 2; hence contradiction by A6; end; Lm2: RAT+ c= RAT+ \/ DEDEKIND_CUTS by XBOOLE_1:7; Lm3: RAT+ misses RA proof assume RAT+ meets RA; then consider e be set such that A1: e in RAT+ and A2: e in RA by XBOOLE_0:3; consider t such that A3: e = { s: s < t } and A4: t <> {} by A2; {} <=' t by ARYTM_3:71; then {} < t by A4,ARYTM_3:75; then A5: {} in e by A3; e c= RAT+ proof let u be set; assume u in e; then ex s st s = u & s < t by A3; hence thesis; end; then reconsider e as non empty Subset of RAT+ by A5; consider s such that A6: s in e and A7: for r st r in e holds r <=' s by A1,ARYTM_3:99; ex r st r = s & r < t by A3,A6; then consider r such that A8: s < r and A9: r < t by ARYTM_3:101; r in e by A3,A9; hence contradiction by A7,A8; end; theorem Th1: RAT+ c= REAL+ by Def2,Lm2,Lm3,XBOOLE_1:86; Lm4: REAL+ c= RAT+ \/ DEDEKIND_CUTS by Def2,XBOOLE_1:36; DEDEKIND_CUTS c= IR by Def1,XBOOLE_1:36; then RAT+ \/ DEDEKIND_CUTS c= RAT+ \/ IR by XBOOLE_1:9; then Lm5: REAL+ c= RAT+ \/ IR by Lm4,XBOOLE_1:1; REAL+ = RAT+ \/ (IR \ { RAT+} \ RA) by Def1,Def2,Lm3,XBOOLE_1:87; then Lm6: DEDEKIND_CUTS \ RA c= REAL+ by Def1,XBOOLE_1:7; theorem Th2: omega c= REAL+ by Th1,ARYTM_3:34,XBOOLE_1:1; definition cluster REAL+ -> non empty; coherence by Th2,ORDINAL2:19; end; definition let x; func DEDEKIND_CUT x -> Element of DEDEKIND_CUTS means :Def3: ex r st x = r & it = { s : s < r } if x in RAT+ otherwise it = x; existence proof thus x in RAT+ implies ex IT being Element of DEDEKIND_CUTS, r st x = r & IT = { s : s < r } proof assume x in RAT+; then reconsider r = x as Element of RAT+; set IT = { s : s < r }; not ex s st s= r & s < r; then not r in IT; then A1: IT <> RAT+; IT c= RAT+ proof let e be set; assume e in IT; then ex s st s = e & s < r; hence thesis; end; then reconsider IT as Subset of RAT+; t in IT implies (for s st s <=' t holds s in IT) & ex s st s in IT & t < s proof assume t in IT; then A2: ex s st t = s & s < r; thus for s st s <=' t holds s in IT proof let s; assume s <=' t; then s < r by A2,ARYTM_3:76; hence s in IT; end; consider s0 being Element of RAT+ such that A3: t < s0 and A4: s0 < r by A2,ARYTM_3:101; take s0; thus s0 in IT by A4; thus t < s0 by A3; end; then IT in IR; then reconsider IT as Element of DEDEKIND_CUTS by A1,Def1,ZFMISC_1:64; take IT,r; thus x = r & IT = { s : s < r }; end; assume A5: not x in RAT+; x in REAL+; then x in DEDEKIND_CUTS by A5,Lm4,XBOOLE_0:def 2; hence thesis; end; uniqueness; consistency; end; theorem not ex y being set st [{},y] in REAL+ proof given y being set such that A1: [{},y] in REAL+; per cases by A1,Lm5,XBOOLE_0:def 2; suppose [{},y] in RAT+; hence contradiction by ARYTM_3:68; suppose [{},y] in IR; hence contradiction by Lm1; end; Lm7: (for r holds r < s iff r < t) implies s = t proof assume A1: for r holds r < s iff r < t; s <=' s & t <=' t; then s <=' t & t <=' s by A1; hence s = t by ARYTM_3:73; end; definition let x be Element of DEDEKIND_CUTS; func GLUED x -> Element of REAL+ means :Def4: ex r st it = r & for s holds s in x iff s < r if ex r st for s holds s in x iff s < r otherwise it = x; uniqueness proof let IT1,IT2 be Element of REAL+; hereby assume ex r st for s holds s in x iff s < r; given r1 being Element of RAT+ such that A1: IT1 = r1 and A2: for s holds s in x iff s < r1; given r2 being Element of RAT+ such that A3: IT2 = r2 and A4: for s holds s in x iff s < r2; for s holds s < r1 iff s < r2 proof let s; s in x iff s < r1 by A2; hence thesis by A4; end; hence IT1 = IT2 by A1,A3,Lm7; end; thus thesis; end; existence proof hereby given r such that A5: for s holds s in x iff s < r; r in RAT+; then reconsider y = r as Element of REAL+ by Th1; take y,r; thus y = r; thus for s holds s in x iff s < r by A5; end; assume A6: not ex r st for s holds s in x iff s < r; now assume x in RA; then consider t such that A7: x = { s: s < t} and t <> {}; for s holds s in x iff s < t proof let s; hereby assume s in x; then ex r st s = r & r < t by A7; hence s < t; end; thus s < t implies s in x by A7; end; hence contradiction by A6; end; then x in DEDEKIND_CUTS \ RA by XBOOLE_0:def 4; then reconsider y = x as Element of REAL+ by Lm6; take y; thus thesis; end; consistency; end; Lm8: for B being set st B in DEDEKIND_CUTS & r in B ex s st s in B & r < s proof let B be set; assume B in DEDEKIND_CUTS; then B in IR by Def1,XBOOLE_0:def 4; then ex A being Subset of RAT+ st B = A & for t st t in A holds (for s st s <=' t holds s in A) & ex s st s in A & t < s; hence thesis; end; Lm9: {} in DEDEKIND_CUTS proof reconsider B = {} as Subset of RAT+ by XBOOLE_1:2; r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s; then {} in { A where A is Subset of RAT+: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s }; hence thesis by Def1,ZFMISC_1:64; end; Lm10: DEDEKIND_CUTS /\ RAT+ = {{}} proof now let e be set; thus e in DEDEKIND_CUTS /\ RAT+ implies e = {} proof assume that A1: e in DEDEKIND_CUTS /\ RAT+ and A2: e <> {}; A3: e in DEDEKIND_CUTS by A1,XBOOLE_0:def 3; then reconsider A = e as non empty Subset of RAT+ by A2; A in RAT+ by A1,XBOOLE_0:def 3; then ex s st s in A & for r st r in A holds r <=' s by ARYTM_3:99; hence contradiction by A3,Lm8; end; thus e = {} implies e in DEDEKIND_CUTS /\ RAT+ by Lm9,XBOOLE_0:def 3; end; hence thesis by TARSKI:def 1; end; Lm11: DEDEKIND_CUT x = {} iff x = {} proof thus DEDEKIND_CUT x = {} implies x = {} proof assume A1: DEDEKIND_CUT x = {}; per cases; suppose x in RAT+; then consider r such that A2: x = r and A3: DEDEKIND_CUT x = { s : s < r } by Def3; assume A4: x <> {}; {} <=' r by ARYTM_3:71; then {} < r by A2,A4,ARYTM_3:75; then {} in DEDEKIND_CUT x by A3; hence contradiction by A1; suppose not x in RAT+; hence x = {} by A1,Def3; end; A5: not ex e being set st e in { s : s < {} } proof given e being set such that A6: e in { s : s < {} }; ex s st s = e & s < {} by A6; hence contradiction by ARYTM_3:71; end; assume x = {}; then ex r st {} = r & DEDEKIND_CUT x = { s : s < r } by Def3; hence DEDEKIND_CUT x = {} by A5,XBOOLE_0:def 1; end; Lm12: for A being Element of DEDEKIND_CUTS holds GLUED A = {} iff A = {} proof let A be Element of DEDEKIND_CUTS; thus GLUED A = {} implies A = {} proof assume A1: GLUED A = {}; per cases; suppose ex r st for s holds s in A iff s < r; then A2: ex r st GLUED A = r & for s holds s in A iff s < r by Def4; assume A <> {}; then consider r such that A3: r in A by SUBSET_1:10; r < {} by A1,A2,A3; hence contradiction by ARYTM_3:71; suppose not ex r st for s holds s in A iff s < r; hence A = {} by A1,Def4; end; assume A4: A = {}; then for s holds s in A iff s < {} by ARYTM_3:71; then consider r such that A5: GLUED A = r and A6: for s holds s in A iff s < r by Def4; assume A7: GLUED A <> {}; {} <=' r by ARYTM_3:71; then {} < r by A5,A7,ARYTM_3:75; hence contradiction by A4,A6; end; Lm13: for A being Element of DEDEKIND_CUTS holds DEDEKIND_CUT GLUED A = A proof let A be Element of DEDEKIND_CUTS; per cases; suppose ex r st for s holds s in A iff s < r; then consider r such that A1: r = GLUED A and A2: for s holds s in A iff s < r by Def4; consider s such that A3: r = s and A4: DEDEKIND_CUT GLUED A = { t : t < s } by A1,Def3; thus DEDEKIND_CUT GLUED A c= A proof let e be set; assume e in DEDEKIND_CUT GLUED A; then ex t st t = e & t < s by A4; hence e in A by A2,A3; end; let e be set; assume A5: e in A; then reconsider s = e as Element of RAT+; s < r by A2,A5; hence e in DEDEKIND_CUT GLUED A by A3,A4; suppose A6: A = {}; then GLUED A = {} by Lm12; hence DEDEKIND_CUT GLUED A = A by A6,Lm11; suppose that A7: A <> {} and A8: not ex r st for s holds s in A iff s < r; A9: GLUED A = A by A8,Def4; now assume GLUED A in RAT+; then GLUED A in RAT+ /\ DEDEKIND_CUTS by A9,XBOOLE_0:def 3; then GLUED A = {} by Lm10,TARSKI:def 1; hence contradiction by A7,Lm12; end; hence DEDEKIND_CUT GLUED A = A by A9,Def3; end; Lm14: for x,y be set st x in IR & y in IR holds x c= y or y c= x proof let x,y be set; assume x in IR; then consider A' being Subset of RAT+ such that A1: x = A' and A2: r in A' implies (for s st s <=' r holds s in A') & ex s st s in A' & r < s; assume y in IR; then consider B' being Subset of RAT+ such that A3: y = B' and A4: r in B' implies (for s st s <=' r holds s in B') & ex s st s in B' & r < s; assume not x c= y; then consider s being set such that A5: s in x and A6: not s in y by TARSKI:def 3; reconsider s as Element of RAT+ by A1,A5; let e be set; assume A7: e in y; then reconsider r = e as Element of RAT+ by A3; r <=' s by A3,A4,A6,A7; hence e in x by A1,A2,A5; end; definition let x,y be Element of REAL+; pred x <=' y means :Def5: ex x',y' st x = x' & y = y' & x' <=' y' if x in RAT+ & y in RAT+, x in y if x in RAT+ & not y in RAT+, not y in x if not x in RAT+ & y in RAT+ otherwise x c= y; consistency; connectedness proof let x,y; assume A1: not(x in RAT+ & y in RAT+ implies ex x',y' st x = x' & y = y' & x' <=' y') or not(x in RAT+ & not y in RAT+ implies x in y) or not(not x in RAT+ & y in RAT+ implies not y in x) or not(not(x in RAT+ & y in RAT+ or x in RAT+ & not y in RAT+ or not x in RAT+ & y in RAT+) implies x c= y); thus y in RAT+ & x in RAT+ implies ex y',x' st y = y' & x = x' & y' <=' x' proof assume y in RAT+ & x in RAT+; then reconsider y' = y, x' = x as Element of RAT+; y' <=' x' by A1; hence thesis; end; thus y in RAT+ & not x in RAT+ implies y in x by A1; thus not y in RAT+ & x in RAT+ implies not x in y by A1; assume A2: not(y in RAT+ & x in RAT+ or y in RAT+ & not x in RAT+ or not y in RAT+ & x in RAT+); x in REAL+ & y in REAL+; then x in IR & y in IR by A2,Lm5,XBOOLE_0:def 2; hence y c= x by A1,A2,Lm14; end; antonym y < x; end; Lm15: x = x' & y = y' implies (x <=' y iff x' <=' y') proof assume that A1: x = x' and A2: y = y'; hereby assume x <=' y; then ex x',y' st x = x' & y = y' & x' <=' y' by A1,A2,Def5; hence x' <=' y' by A1,A2; end; thus thesis by A1,A2,Def5; end; Lm16: for B being set st B in DEDEKIND_CUTS & B <> {} ex r st r in B & r <> {} proof let B be set such that A1: B in DEDEKIND_CUTS and A2: B <> {}; B in IR by A1,Def1,XBOOLE_0:def 4; then consider A being Subset of RAT+ such that A3: B = A and A4: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s; reconsider A as non empty Subset of RAT+ by A2,A3; consider r0 being Element of RAT+ such that A5: r0 in A by SUBSET_1:10; consider r1 being Element of RAT+ such that A6: r1 in A and A7: r0 < r1 by A4,A5; A8: r1 <> {} or r0 <> {} by A7; for r,s st r in A & s <=' r holds s in A by A4; then consider r1,r2,r3 being Element of RAT+ such that A9: r1 in A & r2 in A & r3 in A and A10: r1 <> r2 & r2 <> r3 & r3 <> r1 by A5,A6,A8,ARYTM_3:82; r1 <> {} or r2 <> {} by A10; hence thesis by A3,A9; end; Lm17: for B being set holds B in DEDEKIND_CUTS & r in B & s <=' r implies s in B proof let B be set such that A1: B in DEDEKIND_CUTS and A2: r in B and A3: s <=' r; B in IR by A1,Def1,XBOOLE_0:def 4; then ex A being Subset of RAT+ st B = A & for t st t in A holds (for s st s <=' t holds s in A) & ex s st s in A & t < s; hence s in B by A2,A3; end; Lm18: for B being set st B in DEDEKIND_CUTS & B <> {} holds {} in B proof let B be set such that A1: B in DEDEKIND_CUTS and A2: B <> {}; reconsider B as non empty Subset of RAT+ by A1,A2; consider r such that A3: r in B by SUBSET_1:10; {} <=' r by ARYTM_3:71; hence thesis by A1,A3,Lm17; end; Lm19: for B being set st B in DEDEKIND_CUTS \ RA & not r in B & B <> {} ex s st not s in B & s < r proof let B be set such that A1: B in DEDEKIND_CUTS \ RA and A2: not r in B and A3: B <> {}; A4: B in DEDEKIND_CUTS by A1,XBOOLE_0:def 4; then A5: r <> {} by A2,A3,Lm18; assume A6: for s st not s in B holds not s < r; B = { s: s < r} proof thus B c= { s: s < r} proof let e be set; assume A7: e in B; reconsider B as Element of DEDEKIND_CUTS by A1,XBOOLE_0:def 4; B c= RAT+; then reconsider t = e as Element of RAT+ by A7; not r <=' t by A2,A4,A7,Lm17; hence e in { s: s < r}; end; let e be set; assume e in { s: s < r}; then ex s st s = e & s < r; hence e in B by A6; end; then B in RA by A5; hence contradiction by A1,XBOOLE_0:def 4; end; Lm20: DEDEKIND_CUT x in RA implies x in RAT+ proof assume A1: DEDEKIND_CUT x in RA; assume not x in RAT+; then DEDEKIND_CUT x = x by Def3; hence contradiction by A1,Def2,XBOOLE_0:def 4; end; Lm21: DEDEKIND_CUT x c= DEDEKIND_CUT y implies x <=' y proof assume A1: DEDEKIND_CUT x c= DEDEKIND_CUT y; per cases; suppose that A2: x = {} and A3: not y in RAT+; A4: DEDEKIND_CUT y = y by A3,Def3; y <> {} by A3; then x in y by A2,A4,Lm18; hence thesis by A2,A3,Def5; suppose A5: y = {}; then DEDEKIND_CUT y = {} by Lm11; then DEDEKIND_CUT x = {} by A1,XBOOLE_1:3; then x = {} by Lm11; hence thesis by A5; suppose that A6: x in RAT+ and A7: y in RAT+; consider rx being Element of RAT+ such that A8: x = rx and A9: DEDEKIND_CUT x = { s : s < rx } by A6,Def3; consider ry being Element of RAT+ such that A10: y = ry and A11: DEDEKIND_CUT y = { s : s < ry } by A7,Def3; assume y < x; then ry < rx by A8,A10,Lm15; then ry in DEDEKIND_CUT x by A9; then ry in DEDEKIND_CUT y by A1; then ex s st s = ry & s < ry by A11; hence contradiction; suppose that A12: x in RAT+ and A13: not y in RAT+ and A14: x <> {}; consider rx being Element of RAT+ such that A15: x = rx and A16: DEDEKIND_CUT x = { s : s < rx } by A12,Def3; A17: DEDEKIND_CUT x in RA by A14,A15,A16; A18: DEDEKIND_CUT y = y by A13,Def3; then DEDEKIND_CUT x <> y by A13,A17,Lm20; then not DEDEKIND_CUT y c= DEDEKIND_CUT x by A1,A18,XBOOLE_0:def 10; then consider r0 being Element of RAT+ such that A19: r0 in y and A20: not r0 in DEDEKIND_CUT x by A18,SUBSET_1:7; rx <=' r0 by A16,A20; then x in y by A15,A18,A19,Lm17; hence x <=' y by A12,A13,Def5; suppose that A21: not x in RAT+ and A22: y in RAT+ and A23: y <> {}; consider ry being Element of RAT+ such that A24: y = ry and A25: DEDEKIND_CUT y = { s : s < ry } by A22,Def3; A26: DEDEKIND_CUT y in RA by A23,A24,A25; A27: DEDEKIND_CUT x = x by A21,Def3; then not x in RA by A21,Lm20; then not DEDEKIND_CUT y c= DEDEKIND_CUT x by A1,A26,A27,XBOOLE_0:def 10; then consider r0 being Element of RAT+ such that A28: r0 in DEDEKIND_CUT y and A29: not r0 in x by A27,SUBSET_1:7; ex s st s = r0 & s < ry by A25,A28; then not y in x by A24,A27,A29,Lm17; hence x <=' y by A21,A22,Def5; suppose that A30: not x in RAT+ and A31: not y in RAT+; x = DEDEKIND_CUT x & y = DEDEKIND_CUT y by A30,A31,Def3; hence x <=' y by A1,A30,A31,Def5; end; Lm22: x <=' y & y <=' x implies x = y proof assume that A1: x <=' y and A2: y <=' x; per cases; suppose that A3: x in RAT+ and A4: y in RAT+; reconsider x' = x, y' = y as Element of RAT+ by A3,A4; x' <=' y' & y' <=' x' by A1,A2,Lm15; hence thesis by ARYTM_3:73; suppose that A5: x in RAT+ and A6: not y in RAT+; x in y & not x in y by A1,A2,A5,A6,Def5; hence thesis; suppose that A7: not x in RAT+ and A8: y in RAT+; y in x & not y in x by A1,A2,A7,A8,Def5; hence thesis; suppose that A9: not x in RAT+ and A10: not y in RAT+; x c= y & y c= x by A1,A2,A9,A10,Def5; hence thesis by XBOOLE_0:def 10; end; Lm23: DEDEKIND_CUT x = DEDEKIND_CUT y implies x = y proof assume DEDEKIND_CUT x = DEDEKIND_CUT y; then x <=' y & y <=' x by Lm21; hence x = y by Lm22; end; Lm24: GLUED DEDEKIND_CUT x = x proof DEDEKIND_CUT GLUED DEDEKIND_CUT x = DEDEKIND_CUT x by Lm13; hence thesis by Lm23; end; definition let A,B be Element of DEDEKIND_CUTS; func A + B -> Element of DEDEKIND_CUTS equals :Def6: { r + s : r in A & s in B}; coherence proof { r + s : r in A & s in B} in DEDEKIND_CUTS proof set C = { s + t: s in A & t in B}; C c= RAT+ proof let e be set; assume e in C; then ex s,t st e = s + t & s in A & t in B; hence thesis; end; then reconsider C as Subset of RAT+; r in C implies (for s st s <=' r holds s in C) & ex s st s in C & r < s proof assume r in C; then consider s0,t0 being Element of RAT+ such that A1: r = s0 + t0 and A2: s0 in A & t0 in B; thus for s st s <=' r holds s in C proof let s; assume s <=' r; then consider s1,t1 being Element of RAT+ such that A3: s = s1 + t1 and A4: s1 <=' s0 and A5: t1 <=' t0 by A1,ARYTM_3:95; A6: s1 in A by A2,A4,Lm17; t1 in B by A2,A5,Lm17; hence s in C by A3,A6; end; consider s1 being Element of RAT+ such that A7: s1 in A and A8: s0 < s1 by A2,Lm8; take t2 = s1 + t0; thus t2 in C by A2,A7; s0 <=' s1 & s0 <> s1 by A8; then r <=' t2 & r <> t2 by A1,ARYTM_3:69,83; hence r < t2 by ARYTM_3:75; end; then A9: C in IR; A <> RAT+ by Def1,ZFMISC_1:64; then consider a0 being Element of RAT+ such that A10: not a0 in A by SUBSET_1:49; B <> RAT+ by Def1,ZFMISC_1:64; then consider b0 being Element of RAT+ such that A11: not b0 in B by SUBSET_1:49; now assume a0 + b0 in C; then consider s,t such that A12: a0 + b0 = s + t & s in A & t in B; a0 <=' s or b0 <=' t by A12,ARYTM_3:89; hence contradiction by A10,A11,A12,Lm17; end; then C <> RAT+; hence thesis by A9,Def1,ZFMISC_1:64; end; hence thesis; end; commutativity proof let IT,A,B be Element of DEDEKIND_CUTS; set C = { r + s : r in A & s in B}, D = { r + s : r in B & s in A}; A13: C c= D proof let e be set; assume e in C; then ex r,s st e = r + s & r in A & s in B; hence e in D; end; D c= C proof let e be set; assume e in D; then ex r,s st e = r + s & r in B & s in A; hence e in C; end; hence thesis by A13,XBOOLE_0:def 10; end; end; Lm25: for B being set st B in DEDEKIND_CUTS ex r st not r in B proof let B be set; assume A1: B in DEDEKIND_CUTS; then reconsider B as Subset of RAT+; B <> RAT+ by A1,Def1,ZFMISC_1:64; hence thesis by SUBSET_1:49; end; definition let A,B be Element of DEDEKIND_CUTS; func A *' B -> Element of DEDEKIND_CUTS equals :Def7: { r *' s : r in A & s in B}; coherence proof per cases; suppose A1: A = {}; not ex e being set st e in { r *' s : r in A & s in B} proof given e being set such that A2: e in { r *' s : r in A & s in B}; ex r,s st e = r *' s & r in A & s in B by A2; hence contradiction by A1; end; hence thesis by Lm9,XBOOLE_0:def 1; suppose A3: A <> {}; set C = { r *' s : r in A & s in B}; C c= RAT+ proof let e be set; assume e in C; then ex r,s st r*'s = e & r in A & s in B; hence thesis; end; then reconsider C as Subset of RAT+; r in C implies (for s st s <=' r holds s in C) & ex s st s in C & r < s proof assume r in C; then consider r0,s0 being Element of RAT+ such that A4: r = r0 *' s0 and A5: r0 in A and A6: s0 in B; thus for s st s <=' r holds s in C proof let s; assume s <=' r; then consider t0 being Element of RAT+ such that A7: s = r0 *' t0 and A8: t0 <=' s0 by A4,ARYTM_3:87; t0 in B by A6,A8,Lm17; hence s in C by A5,A7; end; consider t0 being Element of RAT+ such that A9: t0 in B and A10: s0 < t0 by A6,Lm8; per cases; suppose A11: r0 = {}; consider r1 being Element of RAT+ such that A12: r1 in A and A13: r1 <> {} by A3,Lm16; take r1 *' t0; thus r1 *' t0 in C by A9,A12; A14: r = {} by A4,A11,ARYTM_3:54; then A15: r <=' r1 *' t0 by ARYTM_3:71; t0 <> {} by A10,ARYTM_3:71; then r1 *' t0 <> {} by A13,ARYTM_3:86; hence r < r1 *' t0 by A14,A15,ARYTM_3:75; suppose A16: r0 <> {}; take r0 *' t0; thus r0 *' t0 in C by A5,A9; s0 <> t0 by A10; then A17: r <> r0 *' t0 by A4,A16,ARYTM_3:62; r <=' r0 *' t0 by A4,A10,ARYTM_3:90; hence r < r0 *' t0 by A17,ARYTM_3:75; end; then A18: C in IR; consider r0 being Element of RAT+ such that A19: not r0 in A by Lm25; consider s0 being Element of RAT+ such that A20: not s0 in B by Lm25; now assume r0 *' s0 in C; then consider r1,s1 being Element of RAT+ such that A21: r0 *' s0 = r1 *' s1 and A22: r1 in A and A23: s1 in B; r0 <=' r1 or s0 <=' s1 by A21,ARYTM_3:91; hence contradiction by A19,A20,A22,A23,Lm17; end; then C <> RAT+; hence thesis by A18,Def1,ZFMISC_1:64; end; commutativity proof let D,A,B be Element of DEDEKIND_CUTS; assume A24: D = { r *' s : r in A & s in B}; now let e be set; e in D iff ex r,s st e = r*'s & r in A & s in B by A24; then e in D iff ex r,s st e = r*'s & r in B & s in A; hence e in D iff e in { r *' s : r in B & s in A}; end; hence D = { r *' s : r in B & s in A} by TARSKI:2; end; end; definition let x,y be Element of REAL+; func x + y -> Element of REAL+ equals :Def8: x if y = {}, y if x = {} otherwise GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y); coherence; consistency; commutativity; func x *' y -> Element of REAL+ equals :Def9: GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT y); coherence; commutativity; end; theorem Th4: x = {} implies x *' y = {} proof set A = DEDEKIND_CUT x, B = DEDEKIND_CUT y; assume A1: x = {}; not ex e being set st e in { r *' s : r in A & s in B} proof given e being set such that A2: e in { r *' s : r in A & s in B}; ex r,s st e = r *' s & r in A & s in B by A2; hence contradiction by A1,Lm11; end; then { r *' s : r in A & s in B} = {} by XBOOLE_0:def 1; then A3: A *' B = {} by Def7; thus x *' y = GLUED(A *' B) by Def9 .= {} by A3,Lm12; end; canceled; theorem Th6: x + y = {} implies x = {} proof assume A1: x + y = {}; per cases; suppose y = {}; hence x = {} by A1,Def8; suppose A2: y <> {}; assume A3: x <> {}; then GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) = {} by A1,A2,Def8; then A4: DEDEKIND_CUT x + DEDEKIND_CUT y = {} by Lm12; DEDEKIND_CUT x <> {} by A3,Lm11; then consider r0 being Element of RAT+ such that A5: r0 in DEDEKIND_CUT x by SUBSET_1:10; DEDEKIND_CUT y <> {} by A2,Lm11; then consider s0 being Element of RAT+ such that A6: s0 in DEDEKIND_CUT y by SUBSET_1:10; r0 + s0 in { r + s : r in DEDEKIND_CUT x & s in DEDEKIND_CUT y } by A5,A6; hence contradiction by A4,Def6; end; Lm26: for A,B,C being Element of DEDEKIND_CUTS holds A + (B + C) c= A + B + C proof let A,B,C be Element of DEDEKIND_CUTS; let e be set; assume e in A + (B + C); then e in { r + s : r in A & s in B + C} by Def6; then consider r0,s0 being Element of RAT+ such that A1: e = r0 + s0 and A2: r0 in A and A3: s0 in B + C; s0 in { r + s : r in B & s in C} by A3,Def6; then consider r1,s1 being Element of RAT+ such that A4: s0 = r1 + s1 and A5: r1 in B and A6: s1 in C; A7: e = r0 + r1 + s1 by A1,A4,ARYTM_3:57; r0 + r1 in { r + s : r in A & s in B} by A2,A5; then r0 + r1 in A + B by Def6; then e in { r + s : r in A + B & s in C} by A6,A7; hence e in A + B + C by Def6; end; Lm27: for A,B,C being Element of DEDEKIND_CUTS holds A + (B + C) = A + B + C proof let A,B,C be Element of DEDEKIND_CUTS; A + (B + C) c= A + B + C & A + B + C c= A + (B + C) by Lm26; hence thesis by XBOOLE_0:def 10; end; Lm28: for A,B being Element of DEDEKIND_CUTS st A + B = {} holds A = {} or B = {} proof let A,B be Element of DEDEKIND_CUTS such that A1: A + B = {}; assume A <> {}; then consider r0 being Element of RAT+ such that A2: r0 in A by SUBSET_1:10; assume B <> {}; then consider s0 being Element of RAT+ such that A3: s0 in B by SUBSET_1:10; r0 + s0 in { r + s : r in A & s in B} by A2,A3; hence contradiction by A1,Def6; end; theorem Th7: x + (y + z) = (x + y) + z proof per cases; suppose A1: x = {}; hence x + (y + z) = y + z by Def8 .= (x + y) + z by A1,Def8; suppose A2: y = {}; hence x + (y + z) = x + z by Def8 .= (x + y) + z by A2,Def8; suppose A3: z = {}; hence x + (y + z) = x + y by Def8 .= (x + y) + z by A3,Def8; suppose that A4: x <> {} and A5: y <> {} and A6: z <> {}; A7: now assume GLUED(DEDEKIND_CUT y + DEDEKIND_CUT z) = {}; then DEDEKIND_CUT y + DEDEKIND_CUT z = {} by Lm12; then DEDEKIND_CUT y = {} or DEDEKIND_CUT z = {} by Lm28; hence contradiction by A5,A6,Lm11; end; A8: now assume GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) = {}; then DEDEKIND_CUT x + DEDEKIND_CUT y = {} by Lm12; then DEDEKIND_CUT x = {} or DEDEKIND_CUT y = {} by Lm28; hence contradiction by A4,A5,Lm11; end; thus x + (y + z) = x + GLUED(DEDEKIND_CUT y + DEDEKIND_CUT z) by A5,A6,Def8 .= GLUED(DEDEKIND_CUT x + DEDEKIND_CUT GLUED(DEDEKIND_CUT y + DEDEKIND_CUT z)) by A4,A7,Def8 .= GLUED(DEDEKIND_CUT x + (DEDEKIND_CUT y + DEDEKIND_CUT z)) by Lm13 .= GLUED((DEDEKIND_CUT x + DEDEKIND_CUT y) + DEDEKIND_CUT z) by Lm27 .= GLUED(DEDEKIND_CUT GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) + DEDEKIND_CUT z) by Lm13 .= GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) + z by A6,A8,Def8 .= (x + y) + z by A4,A5,Def8; end; theorem IR is c=-linear proof let x,y be set; assume x in IR; then consider A' being Subset of RAT+ such that A1: x = A' and A2: r in A' implies (for s st s <=' r holds s in A') & ex s st s in A' & r < s; assume y in IR; then consider B' being Subset of RAT+ such that A3: y = B' and A4: r in B' implies (for s st s <=' r holds s in B') & ex s st s in B' & r < s; assume not x c= y; then consider s being set such that A5: s in x and A6: not s in y by TARSKI:def 3; reconsider s as Element of RAT+ by A1,A5; let e be set; assume A7: e in y; then reconsider r = e as Element of RAT+ by A3; r <=' s by A3,A4,A6,A7; hence e in x by A1,A2,A5; end; Lm29: for e being set st e in REAL+ holds e <> RAT+ proof let e be set; assume e in REAL+; then e in RAT+ \/ DEDEKIND_CUTS by Def2,XBOOLE_0:def 4; then e in RAT+ or e in DEDEKIND_CUTS by XBOOLE_0:def 2; hence thesis by Def1,ZFMISC_1:64; end; Lm30: for B being set holds B in IR & r in B & s <=' r implies s in B proof let B be set such that A1: B in IR and A2: r in B and A3: s <=' r; ex A being Subset of RAT+ st B = A & for t st t in A holds (for s st s <=' t holds s in A) & ex s st s in A & t < s by A1; hence s in B by A2,A3; end; Lm31: y < x implies ex z st z in RAT+ & z < x & y < z proof assume A1: y < x; per cases; suppose that A2: x in RAT+ and A3: y in RAT+; reconsider x' = x, y' = y as Element of RAT+ by A2,A3; y' < x' by A1,Lm15; then consider z' being Element of RAT+ such that A4: y' < z' & z' < x' by ARYTM_3:101; z' in RAT+; then reconsider z = z' as Element of REAL+ by Th1; take z; thus thesis by A4,Lm15; suppose that A5: not x in RAT+ and A6: y in RAT+; x in REAL+; then x in IR by A5,Lm5,XBOOLE_0:def 2; then consider A being Subset of RAT+ such that A7: x = A and A8: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s; reconsider y' = y as Element of RAT+ by A6; y' in x by A1,A5,Def5; then consider s such that A9: s in A and A10: y' < s by A7,A8; s in RAT+; then reconsider z = s as Element of REAL+ by Th1; take z; thus z in RAT+; thus z < x by A5,A7,A9,Def5; thus y < z by A10,Lm15; suppose that A11: x in RAT+ and A12: not y in RAT+; y in REAL+; then y in IR by A12,Lm5,XBOOLE_0:def 2; then consider B being Subset of RAT+ such that A13: y = B and A14: r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s; reconsider x' = x as Element of RAT+ by A11; A15: not x' in y by A1,A12,Def5; B <> {} by A12,A13; then consider y1 being Element of RAT+ such that A16: y1 in B by SUBSET_1:10; {} <=' y1 by ARYTM_3:71; then A17: x' <> {} by A13,A14,A15,A16; ex z' st z' < x' & not z' in y proof assume A18: not ex z' st z' < x' & not z' in y; set C = { s: s < x' }; y = C proof thus y c= C proof let e be set; assume A19: e in y; then reconsider z' = e as Element of RAT+ by A13; not x' <=' z' by A13,A14,A15,A19; hence e in C; end; let e be set; assume e in C; then consider s such that A20: e = s and A21: s < x'; thus e in y by A18,A20,A21; :: ?? end; then y in RA by A17; hence contradiction by Def2,XBOOLE_0:def 4; end; then consider z' such that A22: z' < x' and A23: not z' in y; z' in RAT+; then reconsider z = z' as Element of REAL+ by Th1; take z; thus z in RAT+; thus z < x by A22,Lm15; thus y < z by A12,A23,Def5; suppose that A24: not x in RAT+ and A25: not y in RAT+; A26: not x c= y by A1,A24,A25,Def5; x in REAL+; then x in IR by A24,Lm5,XBOOLE_0:def 2; then consider A being Subset of RAT+ such that A27: x = A and r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s; y in REAL+; then y in IR by A25,Lm5,XBOOLE_0:def 2; then consider B being Subset of RAT+ such that A28: y = B and r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s; consider z' being Element of RAT+ such that A29: z' in A and A30: not z' in B by A26,A27,A28,SUBSET_1:7; z' in RAT+; then reconsider z = z' as Element of REAL+ by Th1; take z; thus z in RAT+; thus z < x by A24,A27,A29,Def5; thus y < z by A25,A28,A30,Def5; end; Lm32: x <=' y & y <=' z implies x <=' z proof assume that A1: x <=' y and A2: y <=' z; per cases; suppose that A3: x in RAT+ and A4: y in RAT+ and A5: z in RAT+; reconsider x' = x as Element of RAT+ by A3; reconsider y' = y as Element of RAT+ by A4; reconsider z' = z as Element of RAT+ by A5; A6: x' <=' y' by A1,Lm15; y' <=' z' by A2,Lm15; then x' <=' z' by A6,ARYTM_3:74; hence x <=' z by Lm15; suppose that A7: x in RAT+ and A8: y in RAT+ and A9: not z in RAT+; reconsider x' = x as Element of RAT+ by A7; reconsider y' = y as Element of RAT+ by A8; z in REAL+; then z in IR by A9,Lm5,XBOOLE_0:def 2; then consider C being Subset of RAT+ such that A10: z = C and A11: r in C implies (for s st s <=' r holds s in C) & ex s st s in C & r < s; A12: x' <=' y' by A1,Lm15; y in C by A2,A8,A9,A10,Def5; then x' in C by A11,A12; hence x <=' z by A9,A10,Def5; suppose that A13: x in RAT+ and A14: not y in RAT+ and A15: z in RAT+; reconsider x' = x as Element of RAT+ by A13; y in REAL+; then y in IR by A14,Lm5,XBOOLE_0:def 2; then consider B being Subset of RAT+ such that A16: y = B and A17: r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s; reconsider z' = z as Element of RAT+ by A15; A18: x' in B by A1,A14,A16,Def5; not z' in B by A2,A14,A16,Def5; then x' <=' z' by A17,A18; hence x <=' z by Lm15; suppose that A19: x in RAT+ and A20: not y in RAT+ and A21: not z in RAT+; reconsider x' = x as Element of RAT+ by A19; y in REAL+; then y in IR by A20,Lm5,XBOOLE_0:def 2; then consider B being Subset of RAT+ such that A22: y = B and r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s; z in REAL+; then z in IR by A21,Lm5,XBOOLE_0:def 2; then consider C being Subset of RAT+ such that A23: z = C and r in C implies (for s st s <=' r holds s in C) & ex s st s in C & r < s; A24: x' in B by A1,A20,A22,Def5; B c= C by A2,A20,A21,A22,A23,Def5; hence x <=' z by A21,A23,A24,Def5; suppose that A25: not x in RAT+ and A26: y in RAT+ and A27: z in RAT+; x in REAL+; then x in IR by A25,Lm5,XBOOLE_0:def 2; then consider A being Subset of RAT+ such that A28: x = A and A29: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s; reconsider y' = y as Element of RAT+ by A26; reconsider z' = z as Element of RAT+ by A27; A30: not y' in A by A1,A25,A28,Def5; y' <=' z' by A2,Lm15; then not z' in A by A29,A30; hence x <=' z by A25,A28,Def5; suppose that A31: not x in RAT+ and A32: y in RAT+ and A33: not z in RAT+; x in REAL+; then x in IR by A31,Lm5,XBOOLE_0:def 2; then consider A being Subset of RAT+ such that A34: x = A and A35: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s; reconsider y' = y as Element of RAT+ by A32; z in REAL+; then z in IR by A33,Lm5,XBOOLE_0:def 2; then consider C being Subset of RAT+ such that A36: z = C and A37: r in C implies (for s st s <=' r holds s in C) & ex s st s in C & r < s; A38: not y in A by A1,A31,A34,Def5; A39: y in C by A2,A32,A33,A36,Def5; A c= C proof let e be set; assume A40: e in A; then reconsider x' = e as Element of RAT+; x' <=' y' by A35,A38,A40; hence e in C by A37,A39; end; hence x <=' z by A31,A33,A34,A36,Def5; suppose that A41: not x in RAT+ and A42: not y in RAT+ and A43: z in RAT+; x in REAL+; then x in IR by A41,Lm5,XBOOLE_0:def 2; then consider A being Subset of RAT+ such that A44: x = A and r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s; y in REAL+; then y in IR by A42,Lm5,XBOOLE_0:def 2; then consider B being Subset of RAT+ such that A45: y = B and r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s; reconsider z' = z as Element of RAT+ by A43; A c= B by A1,A41,A42,A44,A45,Def5; then not z' in A by A2,A42,A45,Def5; hence x <=' z by A41,A44,Def5; suppose that A46: not x in RAT+ and A47: not y in RAT+ and A48: not z in RAT+; x in REAL+; then x in IR by A46,Lm5,XBOOLE_0:def 2; then consider A being Subset of RAT+ such that A49: x = A and r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s; y in REAL+; then y in IR by A47,Lm5,XBOOLE_0:def 2; then consider B being Subset of RAT+ such that A50: y = B and r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s; z in REAL+; then z in IR by A48,Lm5,XBOOLE_0:def 2; then consider C being Subset of RAT+ such that A51: z = C and r in C implies (for s st s <=' r holds s in C) & ex s st s in C & r < s; A52: A c= B by A1,A46,A47,A49,A50,Def5; B c= C by A2,A47,A48,A50,A51,Def5; then A c= C by A52,XBOOLE_1:1; hence x <=' z by A46,A48,A49,A51,Def5; end; theorem for X,Y being Subset of REAL+ st (ex x st x in X) & (ex x st x in Y) & for x,y st x in X & y in Y holds x <=' y ex z st for x,y st x in X & y in Y holds x <=' z & z <=' y proof let X,Y be Subset of REAL+; given x0 being Element of REAL+ such that x0 in X; given x1 being Element of REAL+ such that A1: x1 in Y; assume A2: for x,y st x in X & y in Y holds x <=' y; set Z = {z' : ex x,z st z = z' & x in X & z < x}; per cases; suppose ex z' st for x' holds x' in Z iff x' < z'; then consider z' such that A3: for x' holds x' in Z iff x' < z'; z' in RAT+; then reconsider z = z' as Element of REAL+ by Th1; take z; let x,y such that A4: x in X and A5: y in Y; thus x <=' z proof assume z < x; then consider x0 being Element of REAL+ such that A6: x0 in RAT+ and A7: x0 < x and A8: z < x0 by Lm31; reconsider x' = x0 as Element of RAT+ by A6; A9: z' < x' by A8,Lm15; x' in Z by A4,A7; hence contradiction by A3,A9; end; assume y < z; then consider y0 being Element of REAL+ such that A10: y0 in RAT+ and A11: y0 < z and A12: y < y0 by Lm31; reconsider y' = y0 as Element of RAT+ by A10; y' < z' by A11,Lm15; then y' in Z by A3; then ex y'' being Element of RAT+ st y' = y'' & ex x,z st z = y'' & x in X & z < x; then consider x1,y1 being Element of REAL+ such that A13: y1 = y' and A14: x1 in X and A15: y1 < x1; y < x1 by A12,A13,A15,Lm32; hence contradiction by A2,A5,A14; suppose A16: not ex z' st for x' holds x' in Z iff x' < z'; A17: now assume Z in RA; then consider t such that A18: Z = { s: s < t } and t <> {}; for x' holds x' in Z iff x' < t proof let x'; hereby assume x' in Z; then ex s st s = x' & s < t by A18; hence x' < t; end; thus x' < t implies x' in Z by A18; end; hence contradiction by A16; end; A19: now assume Z = {}; then A20: for x' st x' in Z holds x' < {}; for x' st x' < {} holds x' in Z by ARYTM_3:71; hence contradiction by A16,A20; end; Z c= RAT+ proof let e be set; assume e in Z; then ex z' st e = z' & ex x,z st z = z' & x in X & z < x; hence e in RAT+; end; then reconsider Z as non empty Subset of RAT+ by A19; t in Z implies (for s st s <=' t holds s in Z) & ex s st s in Z & t < s proof t in RAT+; then reconsider y0 = t as Element of REAL+ by Th1; assume t in Z; then ex z' st z' = t & ex x,z st z = z' & x in X & z < x; then consider x0 being Element of REAL+ such that A21: x0 in X and A22: y0 < x0; thus for s st s <=' t holds s in Z proof let s; s in RAT+; then reconsider z = s as Element of REAL+ by Th1; assume s <=' t; then z <=' y0 by Lm15; then z < x0 by A22,Lm32; hence s in Z by A21; end; consider z such that A23: z in RAT+ and A24: z < x0 and A25: y0 < z by A22,Lm31; reconsider z' = z as Element of RAT+ by A23; take z'; thus z' in Z by A21,A24; thus thesis by A25,Lm15; end; then A26: Z in IR; now assume A27: Z = RAT+; per cases; suppose x1 in RAT+; then reconsider x' = x1 as Element of RAT+; x' in Z by A27; then ex z' st x' = z' & ex x,z st z = z' & x in X & z < x; hence contradiction by A1,A2; suppose A28: not x1 in RAT+; x1 in REAL+; then x1 in IR by A28,Lm5,XBOOLE_0:def 2; then consider A being Subset of RAT+ such that A29: x1 = A and r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s; x1 <> RAT+ by Lm29; then consider x' being Element of RAT+ such that A30: not x' in A by A29,SUBSET_1:49; x' in RAT+; then reconsider x2 = x' as Element of REAL+ by Th1; A31: x1 < x2 by A28,A29,A30,Def5; x2 in Z by A27; then ex z' st x' = z' & ex x,z st z = z' & x in X & z < x; then consider x such that A32: x in X and A33: x2 < x; x1 < x by A31,A33,Lm32; hence contradiction by A1,A2,A32; end; then A34: Z in IR \ {RAT+} by A26,ZFMISC_1:64; then Z in IR \ {RAT+} \ RA by A17,XBOOLE_0:def 4; then reconsider z = Z as Element of REAL+ by Def1,Lm6; A35: now assume z in RAT+; then z in {{}} by A34,Def1,Lm10,XBOOLE_0:def 3; hence contradiction by TARSKI:def 1; end; take z; let x,y such that A36: x in X and A37: y in Y; hereby assume z < x; then consider x0 being Element of REAL+ such that A38: x0 in RAT+ and A39: x0 < x and A40: z < x0 by Lm31; reconsider x' = x0 as Element of RAT+ by A38; x' in z by A36,A39; hence contradiction by A35,A40,Def5; end; assume y < z; then consider y0 being Element of REAL+ such that A41: y0 in RAT+ and A42: y0 < z and A43: y < y0 by Lm31; reconsider y' = y0 as Element of RAT+ by A41; y' in z by A35,A42,Def5; then ex z' st y' = z' & ex x,z st z = z' & x in X & z < x; then consider x0 being Element of REAL+ such that A44: x0 in X and A45: y0 < x0; y < x0 by A43,A45,Lm32; hence contradiction by A2,A37,A44; end; Lm33: one = one; Lm34: {} = {}; Lm35: for A,B being Element of DEDEKIND_CUTS st A + B = A & A <> {} holds B = {} proof let A,B be Element of DEDEKIND_CUTS such that A1: A + B = A and A2: A <> {} and A3: B <> {}; consider y' such that A4: y' in B and A5: y' <> {} by A3,Lm16; A <> RAT+ by Def1,ZFMISC_1:64; then consider r such that A6: not r in A by SUBSET_1:49; consider n being Element of RAT+ such that A7: n in omega and A8: r <=' n *' y' by A5,ARYTM_3:103; defpred _P[Element of RAT+] means $1 *' y' in A; A9: not _P[n] by A6,A8,Lm17; consider A0 being Element of RAT+ such that A10: A0 in A by A2,SUBSET_1:10; A11: {} <=' A0 by ARYTM_3:71; {} *' y' = {} by ARYTM_3:54; then A12: _P[{}] by A10,A11,Lm17; consider n0 being Element of RAT+ such that n0 in omega and A13: _P[n0] and A14: not _P[n0 + one] from DisNat(Lm33,Lm34,A7,A12,A9); A15: (n0 + one) *' y' = n0 *' y' + one *' y' by ARYTM_3:63 .= n0 *' y' + y' by ARYTM_3:59; A + B = { t + s : t in A & s in B} by Def6; hence contradiction by A1,A4,A13,A14,A15; end; Lm36: x + y = x implies y = {} proof assume that A1: x + y = x and A2: y <> {}; A3: x <> {} by A1,A2,Th6; then A4: DEDEKIND_CUT x <> {} by Lm11; DEDEKIND_CUT x = DEDEKIND_CUT GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) by A1,A2,A3,Def8 .= DEDEKIND_CUT x + DEDEKIND_CUT y by Lm13; then DEDEKIND_CUT y = {} by A4,Lm35; hence contradiction by A2,Lm11; end; Lm37: for A,B being Element of DEDEKIND_CUTS st A <> {} & A c= B & A <> B ex C being Element of DEDEKIND_CUTS st A + C = B proof let A,B be Element of DEDEKIND_CUTS such that A1: A <> {} and A2: A c= B and A3: A <> B; set DIF = { t : ex r,s st not r in A & s in B & r + t = s}; not B c= A by A2,A3,XBOOLE_0:def 10; then consider s1 being Element of RAT+ such that A4: s1 in B and A5: not s1 in A by SUBSET_1:7; s1 + {} = s1 by ARYTM_3:92; then A6: {} in DIF by A4,A5; DIF c= RAT+ proof let e be set; assume e in DIF; then ex t st t = e & ex r,s st not r in A & s in B & r + t = s; hence thesis; end; then reconsider DIF as non empty Subset of RAT+ by A6; t in DIF implies (for s st s <=' t holds s in DIF) & ex s st s in DIF & t < s proof assume t in DIF; then ex x' st x' = t & ex r,s st not r in A & s in B & r + x' = s; then consider r0,s0 being Element of RAT+ such that A7: not r0 in A and A8: s0 in B and A9: r0 + t = s0; thus for s st s <=' t holds s in DIF proof let s; assume s <=' t; then consider p such that A10: s + p = t by ARYTM_3:def 12; A11: p <=' t by A10,ARYTM_3:85; t <=' s0 by A9,ARYTM_3:85; then p <=' s0 by A11,ARYTM_3:74; then consider q such that A12: p + q = s0 by ARYTM_3:def 12; r0 + s + p = q + p by A9,A10,A12,ARYTM_3:57; then A13: r0 + s = q by ARYTM_3:69; q <=' s0 by A12,ARYTM_3:85; then q in B by A8,Lm17; hence s in DIF by A7,A13; end; consider s1 being Element of RAT+ such that A14: s1 in B and A15: s0 < s1 by A8,Lm8; consider q such that A16: s0 + q = s1 by A15,ARYTM_3:def 12; take t + q; A17: r0 + (t + q) = s1 by A9,A16,ARYTM_3:57; hence t + q in DIF by A7,A14; A18: t <=' t + q by ARYTM_3:85; t <> t + q by A9,A15,A17; hence thesis by A18,ARYTM_3:75; end; then A19: DIF in IR; B <> RAT+ by Def1,ZFMISC_1:64; then consider s2 being Element of RAT+ such that A20: not s2 in B by SUBSET_1:49; now assume s2 in DIF; then ex t st t = s2 & ex r,s st not r in A & s in B & r + t = s; then consider r,t such that not r in A and A21: t in B and A22: r + s2 = t; s2 <=' t by A22,ARYTM_3:85; hence contradiction by A20,A21,Lm17; end; then DIF <> RAT+; then reconsider DIF as Element of DEDEKIND_CUTS by A19,Def1,ZFMISC_1:64; take DIF; set C = { r + t : r in A & t in DIF}; B = C proof thus B c= C proof let e be set; assume A23: e in B; then reconsider y' = e as Element of RAT+; per cases; suppose A24: y' in A; y' = y' + {} by ARYTM_3:92; hence thesis by A6,A24; suppose A25: not y' in A; consider s0 being Element of RAT+ such that A26: s0 in B and A27: y' < s0 by A23,Lm8; A28: not s0 in A by A25,A27,Lm17; set Z = { r : ex x' st not x' in A & x' + r = s0 }; A29: s0 + {} = s0 by ARYTM_3:92; for r2 being Element of RAT+ st r2 < s0 ex s,t st s in A & t in Z & r2 = s + t proof let r2 be Element of RAT+; assume A30: r2 < s0; then A31: r2 <=' s0 & r2 <> s0; per cases; suppose A32: r2 in A; take r2,{}; thus r2 in A by A32; thus {} in Z by A28,A29; thus r2 = r2 + {} by ARYTM_3:92; suppose A33: not r2 in A; consider q being Element of RAT+ such that A34: r2 + q = s0 by A30,ARYTM_3:def 12; q <> {} by A31,A34,ARYTM_3:92; then consider n being Element of RAT+ such that A35: n in omega and A36: s0 <=' n *' q by ARYTM_3:103; defpred _P[Element of RAT+] means $1 *' q in A; A37: not _P[n] by A28,A36,Lm17; consider y0 being Element of RAT+ such that A38: y0 in A by A1,SUBSET_1:10; {} *' q = {} by ARYTM_3:54; then A39: _P[{}] by A38,Lm18; consider n0 being Element of RAT+ such that n0 in omega and A40: _P[n0] and A41: not _P[n0 + one] from DisNat(Lm33,Lm34,A35,A39,A37); A42: (n0 + one) *' q = n0 *' q + one *' q by ARYTM_3:63 .= n0 *' q + q by ARYTM_3:59; n0 *' q <=' r2 by A33,A40,Lm17; then n0 *' q + q <=' s0 by A34,ARYTM_3:83; then consider t such that A43: n0 *' q + q + t = s0 by ARYTM_3:def 12; take n0 *' q, t; thus n0 *' q in A by A40; thus t in Z by A41,A42,A43; n0 *' q + t + q = r2 + q by A34,A43,ARYTM_3:57; hence r2 = n0 *' q + t by ARYTM_3:69; end; then consider s,t such that A44: s in A and A45: t in Z and A46: y' = s + t by A27; ex r st t= r & ex x' st not x' in A & x' + r = s0 by A45; then t in DIF by A26; hence e in C by A44,A46; end; let e be set; assume e in C; then consider s3,t3 being Element of RAT+ such that A47: e = s3 + t3 and A48: s3 in A and A49: t3 in DIF; ex t st t3 = t & ex r,s st not r in A & s in B & r + t = s by A49; then consider r4,s4 being Element of RAT+ such that A50: not r4 in A and A51: s4 in B and A52: r4 + t3 = s4; s3 <=' r4 by A48,A50,Lm17; then s3 + t3 <=' s4 by A52,ARYTM_3:83; hence e in B by A47,A51,Lm17; end; hence B = A + DIF by Def6; end; Lm38: x <=' y implies DEDEKIND_CUT x c= DEDEKIND_CUT y proof assume A1: x <=' y; A2: DEDEKIND_CUT x in IR & DEDEKIND_CUT y in IR by Def1,XBOOLE_0:def 4; assume A3: not DEDEKIND_CUT x c= DEDEKIND_CUT y; then DEDEKIND_CUT y c= DEDEKIND_CUT x by A2,Lm14; then y <=' x by Lm21; hence thesis by A1,A3,Lm22; end; theorem Th10: x <=' y implies ex z st x + z = y proof assume A1: x <=' y; per cases; suppose A2: x = {}; take y; thus x + y = y by A2,Def8; suppose A3: x = y; {} in RAT+; then reconsider z = {} as Element of REAL+ by Th1; take z; thus thesis by A3,Def8; suppose that A4: x <> {} and A5: x <> y; A6: DEDEKIND_CUT x <> {} by A4,Lm11; A7: DEDEKIND_CUT x <> DEDEKIND_CUT y by A5,Lm23; A8: DEDEKIND_CUT x c= DEDEKIND_CUT y by A1,Lm38; then consider C being Element of DEDEKIND_CUTS such that A9: DEDEKIND_CUT x + C = DEDEKIND_CUT y by A6,A7,Lm37; take GLUED C; now assume A10: C = {}; not ex e being set st e in { r + s : r in C & s in DEDEKIND_CUT x} proof given e being set such that A11: e in { r + s : r in C & s in DEDEKIND_CUT x}; ex r,s st e = r + s & r in C & s in DEDEKIND_CUT x by A11; hence contradiction by A10; end; then { r + s : r in C & s in DEDEKIND_CUT x} = {} by XBOOLE_0:def 1; then DEDEKIND_CUT y = {} by A9,Def6; hence contradiction by A6,A8,XBOOLE_1:3; end; then GLUED C <> {} by Lm12; hence x + GLUED C = GLUED(DEDEKIND_CUT x + DEDEKIND_CUT GLUED C) by A4,Def8 .= GLUED DEDEKIND_CUT y by A9,Lm13 .= y by Lm24; end; theorem Th11: ex z st x + z = y or y + z = x proof x <=' y or y <=' x; hence thesis by Th10; end; theorem Th12: x + y = x + z implies y = z proof assume A1: x + y = x + z; consider q being Element of REAL+ such that A2: z + q = y or y + q = z by Th11; per cases by A2; suppose A3: z + q = y; then x + y = x + y + q by A1,Th7; then q = {} by Lm36; hence y = z by A3,Def8; suppose A4: y + q = z; then x + z = x + z + q by A1,Th7; then q = {} by Lm36; hence y = z by A4,Def8; end; Lm39: for A,B,C being Element of DEDEKIND_CUTS holds A *' (B *' C) c= A *' B *' C proof let A,B,C be Element of DEDEKIND_CUTS; let e be set; assume e in A *' (B *' C); then e in { r *' s : r in A & s in B *' C} by Def7; then consider r0,s0 being Element of RAT+ such that A1: e = r0 *' s0 and A2: r0 in A and A3: s0 in B *' C; s0 in { r *' s : r in B & s in C} by A3,Def7; then consider r1,s1 being Element of RAT+ such that A4: s0 = r1 *' s1 and A5: r1 in B and A6: s1 in C; A7: e = r0 *' r1 *' s1 by A1,A4,ARYTM_3:58; r0 *' r1 in { r *' s : r in A & s in B} by A2,A5; then r0 *' r1 in A *' B by Def7; then e in { r *' s : r in A *' B & s in C} by A6,A7; hence e in A *' B *' C by Def7; end; Lm40: for A,B,C being Element of DEDEKIND_CUTS holds A *' (B *' C) = A *' B *' C proof let A,B,C be Element of DEDEKIND_CUTS; A *' (B *' C) c= A *' B *' C & A *' B *' C c= A *' (B *' C) by Lm39; hence thesis by XBOOLE_0:def 10; end; theorem x *' (y *' z) = x *' y *' z proof thus x *' (y *' z) = x *' GLUED(DEDEKIND_CUT y *' DEDEKIND_CUT z) by Def9 .= GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT GLUED(DEDEKIND_CUT y *' DEDEKIND_CUT z)) by Def9 .= GLUED(DEDEKIND_CUT x *' (DEDEKIND_CUT y *' DEDEKIND_CUT z)) by Lm13 .= GLUED((DEDEKIND_CUT x *' DEDEKIND_CUT y) *' DEDEKIND_CUT z) by Lm40 .= GLUED(DEDEKIND_CUT GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT y) *' DEDEKIND_CUT z) by Lm13 .= GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT y) *' z by Def9 .= x *' y *' z by Def9; end; Lm41: x *' y = {} implies x = {} or y = {} proof assume x *' y = {}; then GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT y) = {} by Def9; then A1: DEDEKIND_CUT x *' DEDEKIND_CUT y = {} by Lm12; DEDEKIND_CUT x = {} or DEDEKIND_CUT y = {} proof assume DEDEKIND_CUT x <> {}; then consider r0 being Element of RAT+ such that A2: r0 in DEDEKIND_CUT x by SUBSET_1:10; assume DEDEKIND_CUT y <> {}; then consider s0 being Element of RAT+ such that A3: s0 in DEDEKIND_CUT y by SUBSET_1:10; r0 *' s0 in { r *' s : r in DEDEKIND_CUT x & s in DEDEKIND_CUT y} by A2,A3; hence contradiction by A1,Def7; end; hence x = {} or y = {} by Lm11; end; Lm42: for A,B,C being Element of DEDEKIND_CUTS holds A *' (B + C) = A *' B + A *' C proof let A,B,C be Element of DEDEKIND_CUTS; thus A *' (B + C) c= A *' B + A *' C proof let e be set; assume e in A *' (B + C); then e in { r *' t : r in A & t in B + C } by Def7; then consider r0, v0 being Element of RAT+ such that A1: e = r0 *' v0 and A2: r0 in A and A3: v0 in B + C; v0 in { s + t : s in B & t in C } by A3,Def6; then consider s0,t0 being Element of RAT+ such that A4: v0 = s0 + t0 and A5: s0 in B and A6: t0 in C; r0 *' s0 in { r *' s: r in A & s in B} by A2,A5; then A7: r0 *' s0 in A *' B by Def7; r0 *' t0 in { r *' s: r in A & s in C} by A2,A6; then A8: r0 *' t0 in A *' C by Def7; e = r0 *' s0 + r0 *' t0 by A1,A4,ARYTM_3:63; then e in { r + s: r in A *' B & s in A *' C } by A7,A8; hence e in A *' B + A *' C by Def6; end; let e be set; assume e in A *' B + A *' C; then e in { r + s: r in A *' B & s in A *' C } by Def6; then consider s1,t1 being Element of RAT+ such that A9: e = s1 + t1 and A10: s1 in A *' B and A11: t1 in A *' C; s1 in { r *' s: r in A & s in B } by A10,Def7; then consider r0,s0 being Element of RAT+ such that A12: s1 = r0 *' s0 and A13: r0 in A and A14: s0 in B; t1 in { r *' s: r in A & s in C } by A11,Def7; then consider r0',t0 being Element of RAT+ such that A15: t1 = r0' *' t0 and A16: r0' in A and A17: t0 in C; per cases; suppose r0 <=' r0'; then r0 *' s0 <=' r0' *' s0 by ARYTM_3:90; then consider s0' being Element of RAT+ such that A18: r0 *' s0 = r0' *' s0' and A19: s0' <=' s0 by ARYTM_3:87; s0' in B by A14,A19,Lm17; then s0' + t0 in { s + t: s in B & t in C } by A17; then A20: s0' + t0 in B + C by Def6; e = r0' *' (s0' + t0) by A9,A12,A15,A18,ARYTM_3:63; then e in { r *' s: r in A & s in B + C } by A16,A20; hence e in A *' (B + C) by Def7; suppose r0' <=' r0; then r0' *' t0 <=' r0 *' t0 by ARYTM_3:90; then consider t0' being Element of RAT+ such that A21: r0' *' t0 = r0 *' t0' and A22: t0' <=' t0 by ARYTM_3:87; t0' in C by A17,A22,Lm17; then s0 + t0' in { s + t: s in B & t in C } by A14; then A23: s0 + t0' in B + C by Def6; e = r0 *' (s0 + t0') by A9,A12,A15,A21,ARYTM_3:63; then e in { r *' s: r in A & s in B + C } by A13,A23; hence e in A *' (B + C) by Def7; end; theorem x *' (y + z) = (x *' y) + (x *' z) proof per cases; suppose A1: x = {}; hence x *' (y + z) = x by Th4 .= x + x by A1,Def8 .= x + (x *' z) by A1,Th4 .= (x *' y) + (x *' z) by A1,Th4; suppose A2: y = {}; hence x *' (y + z) = x *' z by Def8 .= y + x *' z by A2,Def8 .= (x *' y) + (x *' z) by A2,Th4; suppose A3: z = {}; hence x *' (y + z) = x *' y by Def8 .= x *' y + z by A3,Def8 .= (x *' y) + (x *' z) by A3,Th4; suppose that A4: x <> {} and A5: y <> {} and A6: z <> {}; A7: x *' y <> {} by A4,A5,Lm41; A8: x *' z <> {} by A4,A6,Lm41; thus x *' (y + z) = GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT(y + z)) by Def9 .= GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT GLUED(DEDEKIND_CUT y + DEDEKIND_CUT z)) by A5,A6,Def8 .= GLUED(DEDEKIND_CUT x *' (DEDEKIND_CUT y + DEDEKIND_CUT z)) by Lm13 .= GLUED((DEDEKIND_CUT x *' DEDEKIND_CUT y) + (DEDEKIND_CUT x *' DEDEKIND_CUT z)) by Lm42 .= GLUED((DEDEKIND_CUT x *' DEDEKIND_CUT y) + DEDEKIND_CUT GLUED (DEDEKIND_CUT x *' DEDEKIND_CUT z)) by Lm13 .= GLUED((DEDEKIND_CUT x *' DEDEKIND_CUT y) + DEDEKIND_CUT (x*'z)) by Def9 .= GLUED(DEDEKIND_CUT GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT y) + DEDEKIND_CUT (x*'z)) by Lm13 .= GLUED(DEDEKIND_CUT(x*'y) + DEDEKIND_CUT (x*'z)) by Def9 .= (x *' y) + (x *' z) by A7,A8,Def8; end; one in RAT+; then reconsider r_one = one as Element of REAL+ by Th1; Lm43: for B being set st B in IR & B <> {} ex r st r in B & r <> {} proof let B be set such that A1: B in IR and A2: B <> {}; consider A being Subset of RAT+ such that A3: B = A and A4: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s by A1; consider r0 being Element of RAT+ such that A5: r0 in A by A2,A3,SUBSET_1:10; consider r1 being Element of RAT+ such that A6: r1 in A and A7: r0 < r1 by A4,A5; A8: r1 <> {} or r0 <> {} by A7; for r,s st r in A & s <=' r holds s in A by A4; then consider r1,r2,r3 being Element of RAT+ such that A9: r1 in A & r2 in A & r3 in A and A10: r1 <> r2 & r2 <> r3 & r3 <> r1 by A5,A6,A8,ARYTM_3:82; r1 <> {} or r2 <> {} by A10; hence thesis by A3,A9; end; Lm44: for A being Element of DEDEKIND_CUTS st A <> {} ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT r_one proof let A be Element of DEDEKIND_CUTS such that A1: A <> {}; per cases; suppose A in RA; then consider r0 being Element of RAT+ such that A2: A = { s: s < r0} and A3: r0 <> {}; consider s0 being Element of RAT+ such that A4: r0 *' s0 = one by A3,ARYTM_3:60; set B = { s : s < s0 }; B c= RAT+ proof let e be set; assume e in B; then ex s st s = e & s < s0; hence thesis; end; then reconsider B as Subset of RAT+; not ex s st s = s0 & s < s0; then not s0 in B; then A5: B <> RAT+; r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s proof assume r in B; then A6: ex s st s = r & s < s0; thus for s st s <=' r holds s in B proof let s; assume s <=' r; then s < s0 by A6,ARYTM_3:76; hence s in B; end; consider t such that A7: r < t and A8: t < s0 by A6,ARYTM_3:101; take t; thus t in B by A8; thus r < t by A7; end; then B in IR; then reconsider B as Element of DEDEKIND_CUTS by A5,Def1,ZFMISC_1:64; A9: A *' B = { s : s < r0 *' s0 } proof thus A *' B c= { s : s < r0 *' s0 } proof let e be set; assume e in A *' B; then e in { r *' s : r in A & s in B } by Def7; then consider r1,s1 being Element of RAT+ such that A10: e = r1 *' s1 and A11: r1 in A and A12: s1 in B; A13: ex s st s = r1 & s < r0 by A2,A11; A14: ex s st s = s1 & s < s0 by A12; then s1 <> s0; then A15: r0 *' s1 <> r0 *' s0 by A3,ARYTM_3:62; r0 *' s1 <=' r0 *' s0 by A14,ARYTM_3:90; then A16: r0 *' s1 < r0 *' s0 by A15,ARYTM_3:75; r1 *' s1 <=' r0 *' s1 by A13,ARYTM_3:90; then r1 *' s1 < r0 *' s0 by A16,ARYTM_3:76; hence thesis by A10; end; let e be set; assume e in { s : s < r0 *' s0 }; then consider s1 being Element of RAT+ such that A17: e = s1 and A18: s1 < r0 *' s0; consider t0 being Element of RAT+ such that A19: s1 = r0 *' t0 and A20: t0 <=' s0 by A18,ARYTM_3:87; t0 <> s0 by A18,A19; then t0 < s0 by A20,ARYTM_3:75; then t0 in B; then consider t1 being Element of RAT+ such that A21: t1 in B and A22: t0 < t1 by Lm8; r0 *' t0 <=' t1 *' r0 by A22,ARYTM_3:90; then consider r1 being Element of RAT+ such that A23: r0 *' t0 = t1 *' r1 and A24: r1 <=' r0 by ARYTM_3:87; t0 <> t1 by A22; then r1 <> r0 by A3,A23,ARYTM_3:62; then r1 < r0 by A24,ARYTM_3:75; then r1 in A by A2; then e in { r *' s : r in A & s in B } by A17,A19,A21,A23; hence e in A *' B by Def7; end; ex t0 being Element of RAT+ st t0 = r_one & DEDEKIND_CUT r_one = { s : s < t0 } by Def3; hence thesis by A4,A9; suppose A25: not A in RA; set B = { y' : ex x' st not x' in A & x' *' y' <=' one }; A26: A <> RAT+ by Def1,ZFMISC_1:64; then consider x0 being Element of RAT+ such that A27: not x0 in A by SUBSET_1:49; x0 *' {} = {} by ARYTM_3:54; then x0 *' {} <=' one & x0 *' {} <> one by ARYTM_3:71; then A28: {} in B by A27; B c= RAT+ proof let e be set; assume e in B; then ex y' st y' = e & ex x' st not x' in A & x' *' y' <=' one; hence thesis; end; then reconsider B as non empty Subset of RAT+ by A28; A29: A in IR by Def1,ZFMISC_1:64; consider x' such that A30: x' in A by A1,SUBSET_1:10; {} <=' x' by ARYTM_3:71; then A31: {} in A by A29,A30,Lm30; r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s proof assume r in B; then ex y' st r = y' & ex x' st not x' in A & x' *' y' <=' one; then consider x' such that A32: not x' in A and A33: x' *' r <=' one; thus for s st s <=' r holds s in B proof let s; assume s <=' r; then x' *' s <=' x' *' r by ARYTM_3:90; then x' *' s <=' one by A33,ARYTM_3:74; hence thesis by A32; end; A in DEDEKIND_CUTS \ RA by A25,XBOOLE_0:def 4; then consider x'' being Element of RAT+ such that A34: not x'' in A and A35: x'' < x' by A30,A32,Lm19; A36: x'' <=' x' & x'' <> x' by A35; consider s such that A37: one = x'' *' s by A31,A34,ARYTM_3:61; take s; x'' *' s <=' one by A37; hence s in B by A34; x'' *' r <=' x' *' r by A35,ARYTM_3:90; then x'' *' r <=' x'' *' s by A33,A37,ARYTM_3:74; then A38: r <=' s by A31,A34,ARYTM_3:88; A39: x'' *' s <=' x' *' s by A35,ARYTM_3:90; A40: s <> {} by A37,ARYTM_3:54; now assume r = s; then x'' *' s = x' *' s by A33,A37,A39,ARYTM_3:73; hence contradiction by A36,A40,ARYTM_3:62; end; hence r < s by A38,ARYTM_3:75; end; then A41: B in IR; consider x' such that A42: x' in A and A43: x' <> {} by A1,A29,Lm43; consider y' such that A44: x' *' y' = one by A43,ARYTM_3:61; now assume y' in B; then ex s st s = y' & ex x' st not x' in A & x' *' s <=' one; then consider z' such that A45: not z' in A and A46: z' *' y' <=' one; y' <> {} by A44,ARYTM_3:54; then z' <=' x' by A44,A46,ARYTM_3:88; hence contradiction by A29,A42,A45,Lm30; end; then B <> RAT+; then not B in {RAT+} by TARSKI:def 1; then reconsider B as Element of DEDEKIND_CUTS by A41,Def1,XBOOLE_0:def 4; take B; for r holds r in A *' B iff r < one proof let r; hereby assume r in A *' B; then r in { s *' t : s in A & t in B } by Def7; then consider s,t such that A47: r = s *' t and A48: s in A and A49: t in B; ex z' st z' = t & ex x' st not x' in A & x' *' z' <=' one by A49; then consider x' such that A50: not x' in A and A51: x' *' t <=' one; s <=' x' by A29,A48,A50,Lm30; then A52: s *' t <=' x' *' t by ARYTM_3:90; then A53: r <=' one by A47,A51,ARYTM_3:74; now assume A54: r = one; then A55: t <> {} by A47,ARYTM_3:54; s *' t = x' *' t by A47,A51,A52,A54,ARYTM_3:73; hence contradiction by A48,A50,A55,ARYTM_3:62; end; hence r < one by A53,ARYTM_3:75; end; assume A56: r < one; then A57: r <=' one & r <> one; per cases; suppose r = {}; then r = {}*'{} by ARYTM_3:54; then r in { s *' t : s in A & t in B } by A28,A31; hence thesis by Def7; suppose r <> {}; then consider r' being Element of RAT+ such that A58: r *' r' = one by ARYTM_3:61; consider dr being Element of RAT+ such that A59: r + dr = one by A56,ARYTM_3:def 12; set rr = x' *' dr; consider xx being Element of RAT+ such that A60: not xx in A by A26,SUBSET_1:49; dr <> {} by A57,A59,ARYTM_3:56; then rr <> {} by A43,ARYTM_3:86; then consider n0 being Element of RAT+ such that A61: n0 in omega and A62: xx <=' n0 *' rr by ARYTM_3:103; defpred _P[Element of RAT+] means $1 *' rr in A; A63: _P[{}] by A31,ARYTM_3:54; A64: not _P[n0] by A29,A60,A62,Lm30; consider n1 being Element of RAT+ such that n1 in omega and A65: _P[n1] and A66: not _P[n1 + one] from DisNat(Lm33,Lm34,A61,A63,A64); { r *' s : s in A } c= RAT+ proof let e be set; assume e in { r *' s : s in A }; then ex s st e = r *' s & s in A; hence thesis; end; then reconsider rA = { r *' s : s in A } as Subset of RAT+; A67: now assume n1 *' rr in rA; then consider s0 being Element of RAT+ such that A68: r *' s0 = n1 *' rr and A69: s0 in A; A70: (n1 + one) *' rr = n1 *' rr + one *' rr by ARYTM_3:63 .= r *' s0 + dr *' x' by A68,ARYTM_3:59; s0 <=' x' or x' <=' s0; then consider s1 being Element of RAT+ such that A71: s1 = s0 & x' <=' s1 or s1 = x' & s0 <=' s1; r *' s0 <=' r *' s1 by A71,ARYTM_3:90; then A72: r *' s0 + dr *' x' <=' r *' s1 + dr *' x' by ARYTM_3:83; dr *' x' <=' dr *' s1 by A71,ARYTM_3:90; then A73: r *' s1 + dr *' x' <=' r *' s1 + dr *' s1 by ARYTM_3:83; r *' s1 + dr *' s1 = (r + dr) *' s1 by ARYTM_3:63 .= s1 by A59,ARYTM_3:59; hence contradiction by A29,A42,A66,A69,A70,A71,A72,A73,Lm30; end; set s0 = n1 *' rr; r *' {} = {} by ARYTM_3:54; then {} in rA by A31; then consider s' being Element of RAT+ such that A74: s0 *' s' = one by A67,ARYTM_3:61; A75: now assume A76: s0 *' r' in A; r *' (s0 *' r') = one *' s0 by A58,ARYTM_3:58 .= s0 by ARYTM_3:59; hence contradiction by A67,A76; end; s0 *' r' *' (r *' s') = s0 *' r' *' r *' s' by ARYTM_3:58 .= s0 *' one *' s' by A58,ARYTM_3:58 .= one by A74,ARYTM_3:59; then s0 *' r' *' (r *' s') <=' one; then A77: r *' s' in B by A75; s0 *' (r *' s') = s0 *' s' *' r by ARYTM_3:58 .= r by A74,ARYTM_3:59; then r in { s *' t: s in A & t in B} by A65,A77; hence r in A *' B by Def7; end; then DEDEKIND_CUT GLUED(A *' B) = DEDEKIND_CUT r_one by Def4; hence A *' B = DEDEKIND_CUT r_one by Lm13; end; theorem x <> {} implies ex y st x *' y = one proof assume x <> {}; then DEDEKIND_CUT x <> {} by Lm11; then consider B being Element of DEDEKIND_CUTS such that A1: DEDEKIND_CUT x *' B = DEDEKIND_CUT r_one by Lm44; take y = GLUED B; thus x *' y = GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT GLUED B) by Def9 .= GLUED DEDEKIND_CUT r_one by A1,Lm13 .= one by Lm24; end; Lm45: for A,B being Element of DEDEKIND_CUTS st A = { r: r < one } holds A *' B = B proof let A,B be Element of DEDEKIND_CUTS such that A1: A = { r: r < one }; A2: A *' B = { r *' s : r in A & s in B } by Def7; thus A *' B c= B proof let e be set; assume e in A *' B; then consider r,s such that A3: e = r *' s and A4: r in A and A5: s in B by A2; ex t st t = r & t < one by A1,A4; then r *' s <=' one *' s by ARYTM_3:90; then r *' s <=' s by ARYTM_3:59; hence e in B by A3,A5,Lm17; end; let e be set; assume A6: e in B; then reconsider s = e as Element of RAT+; consider s1 being Element of RAT+ such that A7: s1 in B and A8: s < s1 by A6,Lm8; s1 <> {} by A8,ARYTM_3:71; then consider s2 being Element of RAT+ such that A9: s1 *' s2 = s by ARYTM_3:61; one *' s = s2 *' s1 by A9,ARYTM_3:59; then A10: s2 <=' one by A8,ARYTM_3:91; now assume s2 = one; then s = s1 by A9,ARYTM_3:59; hence contradiction by A8; end; then s2 < one by A10,ARYTM_3:75; then s2 in A by A1; hence e in A *' B by A2,A7,A9; end; theorem x = one implies x *' y = y proof assume A1: x = one; then A2: ex r st x = r & DEDEKIND_CUT x = { s : s < r } by Def3; thus x *' y = GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT y) by Def9 .= GLUED DEDEKIND_CUT y by A1,A2,Lm45 .= y by Lm24; end; Lm46: for i,j being Element of omega, x',y' st i = x' & j = y' holds i +^ j = x' + y' proof let i,j be Element of omega, x',y'; assume A1: i = x'; then A2: denominator x' = one by ARYTM_3:def 8; assume A3: j = y'; then A4: denominator y' = one by ARYTM_3:def 8; set a = (denominator x')*^(denominator y'), b = (numerator x')*^(denominator y')+^(numerator y')*^(denominator x'); A5: a = one by A2,A4,ORDINAL2:56; A6: b = (numerator x')*^one+^(numerator y') by A2,A4,ORDINAL2:56 .= (numerator x')+^(numerator y') by ORDINAL2:56 .= i+^(numerator y') by A1,ARYTM_3:def 7 .= i +^ j by A3,ARYTM_3:def 7; A7: RED(a,b) = one by A5,ARYTM_3:29; thus i +^ j = RED(b,a) by A5,A6,ARYTM_3:29 .= b / a by A7,ARYTM_3:def 9 .= x' + y' by ARYTM_3:def 10; end; reconsider one' = one as Element of omega by ORDINAL2:def 21; Lm47: z' < x' + y' & x' <> {} & y' <> {} implies ex r,s st z' = r + s & r < x' & s < y' proof assume that A1: z' < x' + y' and A2: x' <> {} and A3: y' <> {}; consider r0,t0 being Element of RAT+ such that A4: z' = r0 + t0 and A5: r0 <=' x' and A6: t0 <=' y' & t0 <> y' by A1,A3,ARYTM_3:98; per cases; suppose A7: r0 = {}; take {},t0; thus z' = {} + t0 by A4,A7; {} <=' x' by ARYTM_3:71; hence {} < x' by A2,ARYTM_3:75; thus t0 < y' by A6,ARYTM_3:75; suppose A8: r0 <> {}; t0 < y' by A6,ARYTM_3:75; then consider t1 being Element of RAT+ such that A9: t0 < t1 and A10: t1 < y' by ARYTM_3:101; z' < t1 + r0 by A4,A9,ARYTM_3:83; then consider t2,r1 being Element of RAT+ such that A11: z' = t2 + r1 and A12: t2 <=' t1 and A13: r1 <=' r0 & r1 <> r0 by A8,ARYTM_3:98; take r1,t2; thus z' = r1 + t2 by A11; r1 < r0 by A13,ARYTM_3:75; hence r1 < x' by A5,ARYTM_3:76; thus t2 < y' by A10,A12,ARYTM_3:76; end; Lm48: x in RAT+ & y in RAT+ implies ex x',y' st x = x' & y = y' & x + y = x' + y' proof assume that A1: x in RAT+ and A2: y in RAT+; per cases; suppose A3: x = {}; reconsider y' = y as Element of RAT+ by A2; take {},y'; thus x = {} by A3; thus y = y'; thus x + y = y by A3,Def8 .= {} + y' by ARYTM_3:56; suppose A4: y = {}; reconsider x' = x as Element of RAT+ by A1; take x',{}; thus x = x'; thus y = {} by A4; thus x + y = x by A4,Def8 .= x' + {} by ARYTM_3:56; suppose that A5: y <> {} and A6: x <> {}; consider x' such that A7: x = x' and A8: DEDEKIND_CUT x = { s : s < x' } by A1,Def3; consider y' such that A9: y = y' and A10: DEDEKIND_CUT y = { s : s < y' } by A2,Def3; take x',y'; thus x = x' & y = y' by A7,A9; set A = DEDEKIND_CUT x, B = DEDEKIND_CUT y; A11: for s holds s in DEDEKIND_CUT x + DEDEKIND_CUT y iff s < x' + y' proof let s2 be Element of RAT+; thus s2 in A + B implies s2 < x' + y' proof assume s2 in A + B; then s2 in { r + s : r in A & s in B } by Def6; then consider r1,s1 being Element of RAT+ such that A12: s2 = r1 + s1 and A13: r1 in A and A14: s1 in B; ex s st s = s1 & s < y' by A10,A14; then A15: x' + s1 < x' + y' by ARYTM_3:83; ex s st s = r1 & s < x' by A8,A13; then r1 + s1 <=' x' + s1 by ARYTM_3:83; hence thesis by A12,A15,ARYTM_3:76; end; assume s2 < x' + y'; then consider t2,t0 being Element of RAT+ such that A16: s2 = t2 + t0 and A17: t2 < x' and A18: t0 < y' by A5,A6,A7,A9,Lm47; A19: t0 in B by A10,A18; t2 in A by A8,A17; then s2 in { r + s : r in A & s in B } by A16,A19; hence s2 in A + B by Def6; end; then consider r such that A20: GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) = r and A21: for s holds s in DEDEKIND_CUT x + DEDEKIND_CUT y iff s < r by Def4; A22: for s holds s < x' + y' iff s < r proof let s; s in DEDEKIND_CUT x + DEDEKIND_CUT y iff s < x' + y' by A11; hence thesis by A21; end; thus x + y = GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) by A5,A6,Def8 .= x' + y' by A20,A22,Lm7; end; theorem x in omega & y in omega implies y + x in omega proof assume A1: x in omega & y in omega; then reconsider x0 = x, y0 = y as Element of omega; consider x',y' being Element of RAT+ such that A2: x = x' and A3: y = y' and A4: x + y = x' + y' by A1,Lm48,ARYTM_3:34; x' + y' = x0 +^ y0 by A2,A3,Lm46; hence thesis by A4,ORDINAL2:def 21; end; theorem for A being Subset of REAL+ st {} in A & for x,y st x in A & y = one holds x + y in A holds omega c= A proof let A be Subset of REAL+; defpred _P[set] means $1 in A; assume that A1: _P[{}] and A2: for x,y st x in A & y = one holds x + y in A; A3: for a being natural Ordinal st _P[a] holds _P[succ a] proof let a be natural Ordinal; one in RAT+; then reconsider r_one = one as Element of REAL+ by Th1; A4: a in omega by ORDINAL2:def 21; then a in RAT+ by ARYTM_3:34; then reconsider x = a as Element of REAL+ by Th1; assume A5: a in A; consider x', y' being Element of RAT+ such that A6: x = x' and A7: r_one = y' and A8: x + r_one = x' + y' by A4,Lm48,ARYTM_3:34; reconsider i = a as Element of omega by ORDINAL2:def 21; x' + y' = i +^ one' by A6,A7,Lm46 .= succ i by ORDINAL2:48; hence succ a in A by A2,A5,A8; end; A9: for a being natural Ordinal holds _P[a] from Omega_Ind(A1,A3); let e be set; assume e in omega; then e is natural Ordinal by ORDINAL1:23,ORDINAL2:def 21; hence thesis by A9; end; theorem for x st x in omega holds for y holds y in x iff y in omega & y <> x & y <=' x proof let x; assume A1: x in omega; then A2: x c= omega by ORDINAL1:def 2; reconsider m = x as Element of omega by A1; reconsider x' = x as Element of RAT+ by A1,ARYTM_3:34; let y; hereby assume A3: y in x; hence y in omega by A2; then reconsider y' = y as Element of RAT+ by ARYTM_3:34; reconsider n = y as Element of omega by A2,A3; thus y <> x by A3; n c= m by A3,ORDINAL1:def 2; then consider C being Ordinal such that A4: m = n +^ C by ORDINAL3:30; C c= m by A4,ORDINAL3:27; then reconsider C as Element of omega by ORDINAL1:22; C in omega; then reconsider z' = C as Element of RAT+ by ARYTM_3:34; x' = y' + z' by A4,Lm46; then y' <=' x' by ARYTM_3:def 12; hence y <=' x by Lm15; end; assume A5: y in omega; then reconsider n = y as Element of omega; reconsider y' = y as Element of RAT+ by A5,ARYTM_3:34; assume A6: y <> x; assume y <=' x; then y' <=' x' by Lm15; then consider z' such that A7: y' + z' = x' by ARYTM_3:def 12; reconsider k = z' as Element of omega by A1,A5,A7,ARYTM_3:78; n +^ k = m by A7,Lm46; then n c= m by ORDINAL3:27; then n c< m by A6,XBOOLE_0:def 8; hence y in x by ORDINAL1:21; end; theorem x = y + z implies z <=' x proof assume A1: x = y + z; assume A2: not z <=' x; then consider y0 being Element of REAL+ such that A3: x + y0 = z by Th10; {} in RAT+; then reconsider zz = {} as Element of REAL+ by Th1; x = x + (y + y0) by A1,A3,Th7; then x + zz = x + (y + y0) by Def8; then y + y0 = {} by Th12; then y0 = {} by Th6; then z = x by A3,Def8; hence thesis by A2; end; theorem {} in REAL+ & one in REAL+ proof {} in RAT+ & one in RAT+; hence thesis by Th1; end; theorem x in RAT+ & y in RAT+ implies ex x',y' st x = x' & y = y' & x *' y = x' *' y' proof assume that A1: x in RAT+ and A2: y in RAT+; per cases; suppose A3: x = {}; reconsider y' = y as Element of RAT+ by A2; take {},y'; thus x = {} by A3; thus y = y'; thus x *' y = {} by A3,Th4 .= {} *' y' by ARYTM_3:54; suppose A4: y = {}; reconsider x' = x as Element of RAT+ by A1; take x',{}; thus x = x'; thus y = {} by A4; thus x *' y = {} by A4,Th4 .= x' *' {} by ARYTM_3:54; suppose that y <> {} and A5: x <> {}; consider x' such that A6: x = x' and A7: DEDEKIND_CUT x = { s : s < x' } by A1,Def3; consider y' such that A8: y = y' and A9: DEDEKIND_CUT y = { s : s < y' } by A2,Def3; take x',y'; thus x = x' & y = y' by A6,A8; set A = DEDEKIND_CUT x, B = DEDEKIND_CUT y; A10: for s holds s in DEDEKIND_CUT x *' DEDEKIND_CUT y iff s < x' *' y' proof let s2 be Element of RAT+; thus s2 in A *' B implies s2 < x' *' y' proof assume s2 in A *' B; then s2 in { r *' s : r in A & s in B } by Def7; then consider r1,s1 being Element of RAT+ such that A11: s2 = r1 *' s1 and A12: r1 in A and A13: s1 in B; A14: ex s st s = r1 & s < x' by A7,A12; A15: ex s st s = s1 & s < y' by A9,A13; then s1 <> y'; then A16: x' *' s1 <> x' *' y' by A5,A6,ARYTM_3:62; x' *' s1 <=' x' *' y' by A15,ARYTM_3:90; then A17: x' *' s1 < x' *' y' by A16,ARYTM_3:75; r1 *' s1 <=' x' *' s1 by A14,ARYTM_3:90; hence thesis by A11,A17,ARYTM_3:76; end; assume A18: s2 < x' *' y'; then consider t0 being Element of RAT+ such that A19: s2 = x' *' t0 and A20: t0 <=' y' by ARYTM_3:87; t0 <> y' by A18,A19; then t0 < y' by A20,ARYTM_3:75; then consider t1 being Element of RAT+ such that A21: t0 < t1 and A22: t1 < y' by ARYTM_3:101; s2 <=' t1 *' x' by A19,A21,ARYTM_3:90; then consider t2 being Element of RAT+ such that A23: s2 = t1 *' t2 and A24: t2 <=' x' by ARYTM_3:87; now assume t2 = x'; then t0 = t1 by A5,A6,A19,A23,ARYTM_3:62; hence contradiction by A21; end; then t2 < x' by A24,ARYTM_3:75; then A25: t2 in A by A7; t1 in B by A9,A22; then s2 in { r *' s : r in A & s in B } by A23,A25; hence s2 in A *' B by Def7; end; then consider r such that A26: GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT y) = r and A27: for s holds s in DEDEKIND_CUT x *' DEDEKIND_CUT y iff s < r by Def4; A28: for s holds s < x' *' y' iff s < r proof let s; s in DEDEKIND_CUT x *' DEDEKIND_CUT y iff s < x' *' y' by A10; hence thesis by A27; end; thus x *' y = GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT y) by Def9 .= x' *' y' by A26,A28,Lm7; end;

Back to top