Copyright (c) 1998 Association of Mizar Users
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;