:: Non negative real numbers. Part I
:: by Andrzej Trybulec
::
:: Received March 7, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, ARYTM_3, SETFAM_1, XBOOLE_0, TARSKI, ZFMISC_1,
ORDINAL1, ORDINAL2, ARYTM_2, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, ORDINAL2,
ARYTM_3;
constructors ARYTM_3, ORDINAL3;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, ARYTM_3, ORDINAL2, ORDINAL3;
requirements BOOLE, SUBSET, NUMERALS;
definitions TARSKI, XBOOLE_0, ORDINAL1;
equalities TARSKI, ARYTM_3;
expansions TARSKI, XBOOLE_0, ARYTM_3;
theorems XBOOLE_0, ARYTM_3, ZFMISC_1, TARSKI, SUBSET_1, ORDINAL2, ORDINAL1,
ORDINAL3, XBOOLE_1;
schemes ARYTM_3, ORDINAL2;
begin
reserve r,s,t,x9,y9,z9,p,q for Element of RAT+;
definition
func DEDEKIND_CUTS -> Subset-Family of RAT+ equals
{ 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 };
C c= bool RAT+
proof
let e be object;
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 XBOOLE_1:1;
end;
end;
registration
cluster DEDEKIND_CUTS -> non empty;
coherence
proof
set X = { s: s < one };
A1: X c= RAT+
proof
let e be object;
assume e in X;
then ex s st s = e & s < one;
hence thesis;
end;
now
assume one in X;
then ex s st s = one & s < one;
hence contradiction;
end;
then
A2: X <> RAT+;
{} <=' one by ARYTM_3:64;
then {} < one by ARYTM_3:68;
then {} in X;
then reconsider X as non empty Subset of RAT+ by A1;
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:67;
hence thesis;
end;
consider s such that
A4: r < s and
A5: s < one by A3,ARYTM_3:93;
take s;
thus s in X by A5;
thus thesis 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 A2,ZFMISC_1:56;
end;
end;
definition
func REAL+ -> set equals
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 object st [x,y] in IR
proof
given x,y being object 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;
{x} in A & for r,s st r in A & s <=' r holds s in A by A2,A3,TARSKI:def 2;
then consider r1,r2,r3 being Element of RAT+ such that
A4: r1 in A and
A5: r2 in A and
A6: r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 by ARYTM_3:75;
A7: r2 = { x,y } or r2 = { x } by A2,A5,TARSKI:def 2;
r1 = { x,y } or r1 = { x } by A2,A4,TARSKI:def 2;
hence contradiction by A2,A6,A7,TARSKI:def 2;
end;
Lm2: RAT+ misses RA
proof
assume RAT+ meets RA;
then consider e be object such that
A1: e in RAT+ and
A2: e in RA by XBOOLE_0:3;
reconsider e as set by TARSKI:1;
consider t such that
A3: e = { s: s < t } and
A4: t <> {} by A2;
{} <=' t by ARYTM_3:64;
then {} < t by A4,ARYTM_3:68;
then
A5: {} in e by A3;
e c= RAT+
proof
let u be object;
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:91;
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:93;
r in e by A3,A9;
hence contradiction by A7,A8;
end;
theorem Th1:
RAT+ c= REAL+ by Lm2,XBOOLE_1:7,86;
RAT+ \/ DEDEKIND_CUTS c= RAT+ \/ IR by XBOOLE_1:9;
then
Lm3: REAL+ c= RAT+ \/ IR;
REAL+ = RAT+ \/ (IR \ { RAT+} \ RA) by Lm2,XBOOLE_1:87;
then
Lm4: DEDEKIND_CUTS \ RA c= REAL+ by XBOOLE_1:7;
Lm5: omega c= ({[c,d] where c,d is Element of omega: c,d are_coprime &
d <> {}} \ the set of all [k,1] where k is Element of omega) \/ omega by
XBOOLE_1:7;
theorem
omega c= REAL+ by Lm5,Th1;
registration
cluster REAL+ -> non empty;
coherence by Th1;
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 };
A1: IT c= RAT+
proof
let e be object;
assume e in IT;
then ex s st s = e & s < r;
hence thesis;
end;
not ex s st s= r & s < r;
then not r in IT;
then
A2: IT <> RAT+;
reconsider IT as Subset of RAT+ by A1;
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
A3: ex s st t = s & s < r;
then consider s0 being Element of RAT+ such that
A4: t < s0 and
A5: s0 < r by ARYTM_3:93;
thus for s st s <=' t holds s in IT
proof
let s;
assume s <=' t;
then s < r by A3,ARYTM_3:69;
hence thesis;
end;
take s0;
thus s0 in IT by A5;
thus thesis by A4;
end;
then IT in IR;
then reconsider IT as Element of DEDEKIND_CUTS by A2,ZFMISC_1:56;
take IT,r;
thus thesis;
end;
A6: x in REAL+;
assume not x in RAT+;
then x in DEDEKIND_CUTS by A6,XBOOLE_0:def 3;
hence thesis;
end;
uniqueness;
consistency;
end;
theorem
not ex y being object st [{},y] in REAL+
proof
given y being object such that
A1: [{},y] in REAL+;
per cases by A1,Lm3,XBOOLE_0:def 3;
suppose
[{},y] in RAT+;
hence contradiction by ARYTM_3:61;
end;
suppose
[{},y] in IR;
hence contradiction by Lm1;
end;
end;
Lm6: (for r holds r < s iff r < t) implies s = t
proof
assume
A1: for r holds r < s iff r < t;
s <=' s;
then
A2: t <=' s by A1;
t <=' t;
then s <=' t by A1;
hence thesis by A2,ARYTM_3:66;
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 by A2,A4;
hence IT1 = IT2 by A1,A3,Lm6;
end;
thus thesis;
end;
existence
proof
hereby
given r such that
A5: for s holds s in x iff s < r;
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 thesis by A7;
end;
hence contradiction by A6;
end;
then x in DEDEKIND_CUTS \ RA by XBOOLE_0:def 5;
then reconsider y = x as Element of REAL+ by Lm4;
take y;
thus thesis;
end;
consistency;
end;
Lm7: 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;
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;
Lm8: {} 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 ZFMISC_1:56;
end;
Lm9: DEDEKIND_CUTS /\ RAT+ = {{}}
proof
now
let e be object;
thus e in DEDEKIND_CUTS /\ RAT+ implies e = {}
proof
assume that
A1: e in DEDEKIND_CUTS /\ RAT+ and
A2: e <> {};
reconsider A = e as non empty Subset of RAT+ by A1,A2;
A in RAT+ by A1,XBOOLE_0:def 4;
then
A3: ex s st s in A & for r st r in A holds r <=' s by ARYTM_3:91;
e in DEDEKIND_CUTS by A1,XBOOLE_0:def 4;
hence contradiction by A3,Lm7;
end;
thus e = {} implies e in DEDEKIND_CUTS /\ RAT+ by Lm8,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
Lm10: DEDEKIND_CUT x = {} iff x = {}
proof
A1: not ex e being object st e in { s : s < {} }
proof
given e being object such that
A2: e in { s : s < {} };
ex s st s = e & s < {} by A2;
hence contradiction by ARYTM_3:64;
end;
thus DEDEKIND_CUT x = {} implies x = {}
proof
assume
A3: DEDEKIND_CUT x = {};
per cases;
suppose
A4: x in RAT+;
assume
A5: x <> {};
consider r such that
A6: x = r and
A7: DEDEKIND_CUT x = { s : s < r } by A4,Def3;
{} <=' r by ARYTM_3:64;
then {} < r by A6,A5,ARYTM_3:68;
then {} in DEDEKIND_CUT x by A7;
hence contradiction by A3;
end;
suppose
not x in RAT+;
hence thesis by A3,Def3;
end;
end;
assume x = {};
then ex r st {} = r & DEDEKIND_CUT x = { s : s < r } by Def3;
hence thesis by A1,XBOOLE_0:def 1;
end;
Lm11: 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
A2: ex r st for s holds s in A iff s < r;
assume A <> {};
then consider r such that
A3: r in A by SUBSET_1:4;
ex r st GLUED A = r & for s holds s in A iff s < r by A2,Def4;
then r < {} by A1,A3;
hence contradiction by ARYTM_3:64;
end;
suppose
not ex r st for s holds s in A iff s < r;
hence thesis by A1,Def4;
end;
end;
assume
A4: A = {};
then for s holds s in A iff s < {} by ARYTM_3:64;
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:64;
then {} < r by A5,A7,ARYTM_3:68;
hence contradiction by A4,A6;
end;
Lm12: 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 object;
assume e in DEDEKIND_CUT GLUED A;
then ex t st t = e & t < s by A4;
hence thesis by A2,A3;
end;
let e be object;
assume
A5: e in A;
then reconsider s = e as Element of RAT+;
s < r by A2,A5;
hence thesis by A3,A4;
end;
suppose
A6: A = {};
then GLUED A = {} by Lm11;
hence thesis by A6,Lm10;
end;
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 4;
then GLUED A = {} by Lm9,TARSKI:def 1;
hence contradiction by A7,Lm11;
end;
hence thesis by A9,Def3;
end;
end;
Lm13: 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
A1: ex A9 being Subset of RAT+ st x = A9 & for r holds r in A9 implies (for s
st s <=' r holds s in A9) & ex s st s in A9 & r < s;
assume y in IR;
then
A2: ex B9 being Subset of RAT+ st y = B9 & for r holds r in B9 implies (for s
st s <=' r holds s in B9) & ex s st s in B9 & r < s;
assume not x c= y;
then consider s being object such that
A3: s in x and
A4: not s in y;
reconsider s as Element of RAT+ by A1,A3;
let e be object;
assume
A5: e in y;
then reconsider r = e as Element of RAT+ by A2;
r <=' s by A2,A4,A5;
hence thesis by A1,A3;
end;
definition
let x,y be Element of REAL+;
pred x <=' y means
:Def5:
ex x9,y9 st x = x9 & y = y9 & x9 <=' y9 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 x9,y9 st x = x9 & y = y9 & x9
<=' y9) 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 y9,x9 st y = y9 & x = x9 & y9 <=' x9
proof
assume y in RAT+ & x in RAT+;
then reconsider y9 = y, x9 = x as Element of RAT+;
y9 <=' x9 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+);
y in REAL+;
then
A3: y in IR by A2,Lm3,XBOOLE_0:def 3;
x in REAL+;
then x in IR by A2,Lm3,XBOOLE_0:def 3;
hence thesis by A1,A2,A3,Lm13;
end;
end;
notation
let x,y be Element of REAL+;
antonym y < x for x <=' y;
end;
Lm14: x = x9 & y = y9 implies (x <=' y iff x9 <=' y9)
proof
assume
A1: x = x9 & y = y9;
hereby
assume x <=' y;
then ex x9,y9 st x = x9 & y = y9 & x9 <=' y9 by A1,Def5;
hence x9 <=' y9 by A1;
end;
thus thesis by A1,Def5;
end;
Lm15: 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;
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:4;
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 and
r3 in A and
A10: r1 <> r2 and
r2 <> r3 and
r3 <> r1 by A5,A6,A8,ARYTM_3:75;
r1 <> {} or r2 <> {} by A10;
hence thesis by A3,A9;
end;
Lm16: 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 & s <=' r;
B in IR by A1;
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 by A2;
end;
Lm17: 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;
ex r st r in B by SUBSET_1:4;
hence thesis by A1,Lm16,ARYTM_3:64;
end;
Lm18: 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 5;
assume
A5: for s st not s in B holds not s < r;
A6: B = { s: s < r}
proof
thus B c= { s: s < r}
proof
let e be object;
assume
A7: e in B;
reconsider B as Element of DEDEKIND_CUTS by A1,XBOOLE_0:def 5;
B c= RAT+;
then reconsider t = e as Element of RAT+ by A7;
not r <=' t by A2,A4,A7,Lm16;
hence thesis;
end;
let e be object;
assume e in { s: s < r};
then ex s st s = e & s < r;
hence thesis by A5;
end;
r <> {} by A2,A3,A4,Lm17;
then B in RA by A6;
hence contradiction by A1,XBOOLE_0:def 5;
end;
Lm19: 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,XBOOLE_0:def 5;
end;
Lm20: 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+;
DEDEKIND_CUT y = y & y <> {} by A3,Def3;
then x in y by A2,Lm17;
hence thesis by A2,A3,Def5;
end;
suppose
A4: y = {};
then DEDEKIND_CUT y = {} by Lm10;
then DEDEKIND_CUT x = {} by A1;
then x = {} by Lm10;
hence thesis by A4;
end;
suppose that
A5: x in RAT+ and
A6: y in RAT+;
consider ry being Element of RAT+ such that
A7: y = ry and
A8: DEDEKIND_CUT y = { s : s < ry } by A6,Def3;
consider rx being Element of RAT+ such that
A9: x = rx and
A10: DEDEKIND_CUT x = { s : s < rx } by A5,Def3;
assume y < x;
then ry < rx by A9,A7,Lm14;
then ry in DEDEKIND_CUT x by A10;
then ry in DEDEKIND_CUT y by A1;
then ex s st s = ry & s < ry by A8;
hence contradiction;
end;
suppose that
A11: x in RAT+ and
A12: not y in RAT+ and
A13: x <> {};
A14: DEDEKIND_CUT y = y by A12,Def3;
consider rx being Element of RAT+ such that
A15: x = rx and
A16: DEDEKIND_CUT x = { s : s < rx } by A11,Def3;
DEDEKIND_CUT x in RA by A13,A15,A16;
then DEDEKIND_CUT x <> y by A12,A14,Lm19;
then not DEDEKIND_CUT y c= DEDEKIND_CUT x by A1,A14;
then consider r0 being Element of RAT+ such that
A17: r0 in y and
A18: not r0 in DEDEKIND_CUT x by A14;
rx <=' r0 by A16,A18;
then x in y by A15,A14,A17,Lm16;
hence thesis by A11,A12,Def5;
end;
suppose that
A19: not x in RAT+ and
A20: y in RAT+ and
A21: y <> {};
consider ry being Element of RAT+ such that
A22: y = ry and
A23: DEDEKIND_CUT y = { s : s < ry } by A20,Def3;
A24: DEDEKIND_CUT y in RA by A21,A22,A23;
A25: DEDEKIND_CUT x = x by A19,Def3;
then not x in RA by A19,Lm19;
then not DEDEKIND_CUT y c= DEDEKIND_CUT x by A1,A24,A25,XBOOLE_0:def 10;
then consider r0 being Element of RAT+ such that
A26: r0 in DEDEKIND_CUT y and
A27: not r0 in x by A25;
ex s st s = r0 & s < ry by A23,A26;
then not y in x by A22,A25,A27,Lm16;
hence thesis by A19,A20,Def5;
end;
suppose that
A28: ( not x in RAT+)& not y in RAT+;
x = DEDEKIND_CUT x & y = DEDEKIND_CUT y by A28,Def3;
hence thesis by A1,A28,Def5;
end;
end;
Lm21: x <=' y & y <=' x implies x = y
proof
assume that
A1: x <=' y and
A2: y <=' x;
per cases;
suppose
x in RAT+ & y in RAT+;
then reconsider x9 = x, y9 = y as Element of RAT+;
x9 <=' y9 & y9 <=' x9 by A1,A2,Lm14;
hence thesis by ARYTM_3:66;
end;
suppose that
A3: x in RAT+ & not y in RAT+;
x in y by A1,A3,Def5;
hence thesis by A2,A3,Def5;
end;
suppose that
A4: ( not x in RAT+)& y in RAT+;
y in x by A2,A4,Def5;
hence thesis by A1,A4,Def5;
end;
suppose
( not x in RAT+)& not y in RAT+;
then x c= y & y c= x by A1,A2,Def5;
hence thesis;
end;
end;
Lm22: DEDEKIND_CUT x = DEDEKIND_CUT y implies x = y
proof
assume DEDEKIND_CUT x = DEDEKIND_CUT y;
then x <=' y & y <=' x by Lm20;
hence thesis by Lm21;
end;
Lm23: GLUED DEDEKIND_CUT x = x
proof
DEDEKIND_CUT GLUED DEDEKIND_CUT x = DEDEKIND_CUT x by Lm12;
hence thesis by Lm22;
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 object;
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+;
A <> RAT+ by ZFMISC_1:56;
then consider a0 being Element of RAT+ such that
A1: not a0 in A by SUBSET_1:28;
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
A2: r = s0 + t0 and
A3: s0 in A and
A4: 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
A5: s = s1 + t1 and
A6: s1 <=' s0 & t1 <=' t0 by A2,ARYTM_3:87;
s1 in A & t1 in B by A3,A4,A6,Lm16;
hence thesis by A5;
end;
consider s1 being Element of RAT+ such that
A7: s1 in A and
A8: s0 < s1 by A3,Lm7;
take t2 = s1 + t0;
thus t2 in C by A4,A7;
thus thesis by A2,A8,ARYTM_3:76;
end;
then
A9: C in IR;
B <> RAT+ by ZFMISC_1:56;
then consider b0 being Element of RAT+ such that
A10: not b0 in B by SUBSET_1:28;
now
assume a0 + b0 in C;
then consider s,t such that
A11: a0 + b0 = s + t and
A12: s in A & t in B;
a0 <=' s or b0 <=' t by A11,ARYTM_3:81;
hence contradiction by A1,A10,A12,Lm16;
end;
then C <> RAT+;
hence thesis by A9,ZFMISC_1:56;
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: D c= C
proof
let e be object;
assume e in D;
then ex r,s st e = r + s & r in B & s in A;
hence thesis;
end;
C c= D
proof
let e be object;
assume e in C;
then ex r,s st e = r + s & r in A & s in B;
hence thesis;
end;
hence thesis by A13;
end;
end;
Lm24: 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,ZFMISC_1:56;
hence thesis by SUBSET_1:28;
end;
definition
let A,B be Element of DEDEKIND_CUTS;
func A *' B -> Element of DEDEKIND_CUTS equals
{ r *' s : r in A & s in B};
coherence
proof
per cases;
suppose
A1: A = {};
not ex e being object st e in { r *' s : r in A & s in B}
proof
given e being object 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 Lm8,XBOOLE_0:def 1;
end;
suppose
A3: A <> {};
set C = { r *' s : r in A & s in B};
C c= RAT+
proof
let e be object;
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:79;
t0 in B by A6,A8,Lm16;
hence thesis by A5,A7;
end;
consider t0 being Element of RAT+ such that
A9: t0 in B and
A10: s0 < t0 by A6,Lm7;
per cases;
suppose
A11: r0 = {};
consider r1 being Element of RAT+ such that
A12: r1 in A and
A13: r1 <> {} by A3,Lm15;
take r1 *' t0;
thus r1 *' t0 in C by A9,A12;
t0 <> {} by A10,ARYTM_3:64;
then
A14: r1 *' t0 <> {} by A13,ARYTM_3:78;
A15: r = {} by A4,A11,ARYTM_3:48;
then r <=' r1 *' t0 by ARYTM_3:64;
hence thesis by A15,A14,ARYTM_3:68;
end;
suppose
A16: r0 <> {};
s0 <> t0 by A10;
then
A17: r <> r0 *' t0 by A4,A16,ARYTM_3:56;
take r0 *' t0;
thus r0 *' t0 in C by A5,A9;
r <=' r0 *' t0 by A4,A10,ARYTM_3:82;
hence thesis by A17,ARYTM_3:68;
end;
end;
then
A18: C in IR;
consider r0 being Element of RAT+ such that
A19: not r0 in A by Lm24;
consider s0 being Element of RAT+ such that
A20: not s0 in B by Lm24;
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 & s1 in B;
r0 <=' r1 or s0 <=' s1 by A21,ARYTM_3:83;
hence contradiction by A19,A20,A22,Lm16;
end;
then C <> RAT+;
hence thesis by A18,ZFMISC_1:56;
end;
end;
commutativity
proof
let D,A,B be Element of DEDEKIND_CUTS;
assume
A23: D = { r *' s : r in A & s in B};
now
let e be object;
e in D iff ex r,s st e = r*'s & r in A & s in B by A23;
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 thesis 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
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 object st e in { r *' s : r in A & s in B}
proof
given e being object 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,Lm10;
end;
then { r *' s : r in A & s in B} = {} by XBOOLE_0:def 1;
hence thesis by Lm11;
end;
theorem Th5:
x + y = {} implies x = {}
proof
assume
A1: x + y = {};
per cases;
suppose
y = {};
hence thesis by A1,Def8;
end;
suppose
A2: y <> {};
then DEDEKIND_CUT y <> {} by Lm10;
then consider s0 being Element of RAT+ such that
A3: s0 in DEDEKIND_CUT y by SUBSET_1:4;
assume
A4: x <> {};
then DEDEKIND_CUT x <> {} by Lm10;
then consider r0 being Element of RAT+ such that
A5: r0 in DEDEKIND_CUT x by SUBSET_1:4;
A6: r0 + s0 in { r + s : r in DEDEKIND_CUT x & s in DEDEKIND_CUT y } by A5,A3;
GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) = {} by A1,A2,A4,Def8;
hence contradiction by A6,Lm11;
end;
end;
Lm25: 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 object;
assume e in A + (B + C);
then consider r0,s0 being Element of RAT+ such that
A1: e = r0 + s0 & r0 in A and
A2: s0 in B + C;
consider r1,s1 being Element of RAT+ such that
A3: s0 = r1 + s1 & r1 in B and
A4: s1 in C by A2;
e = r0 + r1 + s1 & r0 + r1 in A + B by A1,A3,ARYTM_3:51;
hence thesis by A4;
end;
Lm26: for A,B,C being Element of DEDEKIND_CUTS holds A + (B + C) = A + B + C
by Lm25;
Lm27: 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:4;
assume B <> {};
then consider s0 being Element of RAT+ such that
A3: s0 in B by SUBSET_1:4;
r0 + s0 in { r + s : r in A & s in B} by A2,A3;
hence contradiction by A1;
end;
theorem Th6:
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;
end;
suppose
A2: y = {};
hence x + (y + z) = x + z by Def8
.= (x + y) + z by A2,Def8;
end;
suppose
A3: z = {};
hence x + (y + z) = x + y by Def8
.= (x + y) + z by A3,Def8;
end;
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 Lm11;
then DEDEKIND_CUT y = {} or DEDEKIND_CUT z = {} by Lm27;
hence contradiction by A5,A6,Lm10;
end;
A8: now
assume GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) = {};
then DEDEKIND_CUT x + DEDEKIND_CUT y = {} by Lm11;
then DEDEKIND_CUT x = {} or DEDEKIND_CUT y = {} by Lm27;
hence contradiction by A4,A5,Lm10;
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 Lm12
.= GLUED((DEDEKIND_CUT x + DEDEKIND_CUT y) + DEDEKIND_CUT z) by Lm26
.= GLUED(DEDEKIND_CUT GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) +
DEDEKIND_CUT z) by Lm12
.= GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) + z by A6,A8,Def8
.= (x + y) + z by A4,A5,Def8;
end;
end;
theorem
{ 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} is c=-linear
proof
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};
let x,y be set;
assume x in IR;
then
A1: ex A9 being Subset of RAT+ st x = A9 & for r holds r in A9 implies (for s
st s <=' r holds s in A9) & ex s st s in A9 & r < s;
assume y in IR;
then
A2: ex B9 being Subset of RAT+ st y = B9 & for r holds r in B9 implies (for s
st s <=' r holds s in B9) & ex s st s in B9 & r < s;
assume not x c= y;
then consider s being object such that
A3: s in x and
A4: not s in y;
reconsider s as Element of RAT+ by A1,A3;
let e be object;
assume
A5: e in y;
then reconsider r = e as Element of RAT+ by A2;
r <=' s by A2,A4,A5;
hence thesis by A1,A3;
end;
Lm28: for e being set st e in REAL+ holds e <> RAT+
proof
let e be set;
assume e in REAL+;
then e in RAT+ or e in DEDEKIND_CUTS by XBOOLE_0:def 3;
hence thesis by ZFMISC_1:56;
end;
Lm29: 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 & 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 thesis by A2;
end;
Lm30: y < x implies ex z st z in RAT+ & z < x & y < z
proof
assume
A1: y < x;
per cases;
suppose
x in RAT+ & y in RAT+;
then reconsider x9 = x, y9 = y as Element of RAT+;
y9 < x9 by A1,Lm14;
then consider z9 being Element of RAT+ such that
A2: y9 < z9 & z9 < x9 by ARYTM_3:93;
reconsider z = z9 as Element of REAL+ by Th1;
take z;
thus thesis by A2,Lm14;
end;
suppose that
A3: not x in RAT+ and
A4: y in RAT+;
reconsider y9 = y as Element of RAT+ by A4;
x in REAL+;
then x in IR by A3,Lm3,XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A5: x = A and
A6: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s;
y9 in x by A1,A3,Def5;
then consider s such that
A7: s in A and
A8: y9 < s by A5,A6;
reconsider z = s as Element of REAL+ by Th1;
take z;
thus z in RAT+;
thus z < x by A3,A5,A7,Def5;
thus thesis by A8,Lm14;
end;
suppose that
A9: x in RAT+ and
A10: not y in RAT+;
reconsider x9 = x as Element of RAT+ by A9;
A11: not x9 in y by A1,A10,Def5;
y in REAL+;
then y in IR by A10,Lm3,XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A12: y = B and
A13: r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s;
B <> {} by A10,A12;
then consider y1 being Element of RAT+ such that
A14: y1 in B by SUBSET_1:4;
{} <=' y1 by ARYTM_3:64;
then
A15: x9 <> {} by A12,A13,A11,A14;
ex z9 st z9 < x9 & not z9 in y
proof
set C = { s: s < x9 };
assume
A16: not ex z9 st z9 < x9 & not z9 in y;
y = C
proof
thus y c= C
proof
let e be object;
assume
A17: e in y;
then reconsider z9 = e as Element of RAT+ by A12;
not x9 <=' z9 by A12,A13,A11,A17;
hence thesis;
end;
let e be object;
assume e in C;
then ex s st e = s & s < x9;
hence thesis by A16;
end;
then y in RA by A15;
hence contradiction by XBOOLE_0:def 5;
end;
then consider z9 such that
A18: z9 < x9 and
A19: not z9 in y;
reconsider z = z9 as Element of REAL+ by Th1;
take z;
thus z in RAT+;
thus z < x by A18,Lm14;
thus thesis by A10,A19,Def5;
end;
suppose that
A20: not x in RAT+ and
A21: not y in RAT+;
y in REAL+;
then y in IR by A21,Lm3,XBOOLE_0:def 3;
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;
x in REAL+;
then x in IR by A20,Lm3,XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A23: x = A and
r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s;
not x c= y by A1,A20,A21,Def5;
then consider z9 being Element of RAT+ such that
A24: z9 in A and
A25: not z9 in B by A23,A22;
reconsider z = z9 as Element of REAL+ by Th1;
take z;
thus z in RAT+;
thus z < x by A20,A23,A24,Def5;
thus thesis by A21,A22,A25,Def5;
end;
end;
Lm31: 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 z9 = z as Element of RAT+ by A5;
reconsider y9 = y as Element of RAT+ by A4;
reconsider x9 = x as Element of RAT+ by A3;
x9 <=' y9 & y9 <=' z9 by A1,A2,Lm14;
then x9 <=' z9 by ARYTM_3:67;
hence thesis by Lm14;
end;
suppose that
A6: x in RAT+ and
A7: y in RAT+ and
A8: not z in RAT+;
reconsider y9 = y as Element of RAT+ by A7;
reconsider x9 = x as Element of RAT+ by A6;
A9: x9 <=' y9 by A1,Lm14;
z in REAL+;
then z in IR by A8,Lm3,XBOOLE_0:def 3;
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;
y in C by A2,A7,A8,A10,Def5;
then x9 in C by A11,A9;
hence thesis by A8,A10,Def5;
end;
suppose that
A12: x in RAT+ and
A13: not y in RAT+ and
A14: z in RAT+;
reconsider z9 = z as Element of RAT+ by A14;
reconsider x9 = x as Element of RAT+ by A12;
y in REAL+;
then y in IR by A13,Lm3,XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A15: y = B and
A16: r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s;
x9 in B & not z9 in B by A1,A2,A13,A15,Def5;
then x9 <=' z9 by A16;
hence thesis by Lm14;
end;
suppose that
A17: x in RAT+ and
A18: not y in RAT+ and
A19: not z in RAT+;
reconsider x9 = x as Element of RAT+ by A17;
y in REAL+;
then y in IR by A18,Lm3,XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A20: y = B and
r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s;
A21: x9 in B by A1,A18,A20,Def5;
z in REAL+;
then z in IR by A19,Lm3,XBOOLE_0:def 3;
then consider C being Subset of RAT+ such that
A22: z = C and
r in C implies (for s st s <=' r holds s in C) & ex s st s in C & r < s;
B c= C by A2,A18,A19,A20,A22,Def5;
hence thesis by A19,A22,A21,Def5;
end;
suppose that
A23: not x in RAT+ and
A24: y in RAT+ and
A25: z in RAT+;
reconsider z9 = z as Element of RAT+ by A25;
reconsider y9 = y as Element of RAT+ by A24;
A26: y9 <=' z9 by A2,Lm14;
x in REAL+;
then x in IR by A23,Lm3,XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A27: x = A and
A28: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s;
not y9 in A by A1,A23,A27,Def5;
then not z9 in A by A28,A26;
hence thesis by A23,A27,Def5;
end;
suppose that
A29: not x in RAT+ and
A30: y in RAT+ and
A31: not z in RAT+;
x in REAL+;
then x in IR by A29,Lm3,XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A32: x = A and
A33: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s;
A34: not y in A by A1,A29,A32,Def5;
reconsider y9 = y as Element of RAT+ by A30;
z in REAL+;
then z in IR by A31,Lm3,XBOOLE_0:def 3;
then consider C being Subset of RAT+ such that
A35: z = C and
A36: r in C implies (for s st s <=' r holds s in C) & ex s st s in C & r < s;
A37: y in C by A2,A30,A31,A35,Def5;
A c= C
proof
let e be object;
assume
A38: e in A;
then reconsider x9 = e as Element of RAT+;
x9 <=' y9 by A33,A34,A38;
hence thesis by A36,A37;
end;
hence thesis by A29,A31,A32,A35,Def5;
end;
suppose that
A39: not x in RAT+ and
A40: not y in RAT+ and
A41: z in RAT+;
reconsider z9 = z as Element of RAT+ by A41;
x in REAL+;
then x in IR by A39,Lm3,XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A42: 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 A40,Lm3,XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A43: y = B and
r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s;
A c= B by A1,A39,A40,A42,A43,Def5;
then not z9 in A by A2,A40,A43,Def5;
hence thesis by A39,A42,Def5;
end;
suppose that
A44: not x in RAT+ and
A45: not y in RAT+ and
A46: not z in RAT+;
z in REAL+;
then z in IR by A46,Lm3,XBOOLE_0:def 3;
then consider C being Subset of RAT+ such that
A47: z = C and
r in C implies (for s st s <=' r holds s in C) & ex s st s in C & r < s;
y in REAL+;
then y in IR by A45,Lm3,XBOOLE_0:def 3;
then consider B being Subset of RAT+ such that
A48: y = B and
r in B implies (for s st s <=' r holds s in B) & ex s st s in B & r < s;
A49: B c= C by A2,A45,A46,A48,A47,Def5;
x in REAL+;
then x in IR by A44,Lm3,XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A50: x = A and
r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s;
A c= B by A1,A44,A45,A50,A48,Def5;
then A c= C by A49;
hence thesis by A44,A46,A50,A47,Def5;
end;
end;
theorem
for X,Y being Subset of REAL+ st (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 x1 being Element of REAL+ such that
A1: x1 in Y;
set Z = {z9 : ex x,z st z = z9 & x in X & z < x};
assume
A2: for x,y st x in X & y in Y holds x <=' y;
per cases;
suppose
ex z9 st for x9 holds x9 in Z iff x9 < z9;
then consider z9 such that
A3: for x9 holds x9 in Z iff x9 < z9;
reconsider z = z9 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 & z < x0 by Lm30;
reconsider x9 = x0 as Element of RAT+ by A6;
z9 < x9 & x9 in Z by A4,A7,Lm14;
hence contradiction by A3;
end;
assume y < z;
then consider y0 being Element of REAL+ such that
A8: y0 in RAT+ and
A9: y0 < z and
A10: y < y0 by Lm30;
reconsider y9 = y0 as Element of RAT+ by A8;
y9 < z9 by A9,Lm14;
then y9 in Z by A3;
then
ex y99 being Element of RAT+ st y9 = y99 & ex x,z st z = y99 & x in X
& z < x;
then consider x1,y1 being Element of REAL+ such that
A11: y1 = y9 and
A12: x1 in X and
A13: y1 < x1;
y < x1 by A10,A11,A13,Lm31;
hence contradiction by A2,A5,A12;
end;
suppose
A14: not ex z9 st for x9 holds x9 in Z iff x9 < z9;
A15: now
assume Z in RA;
then consider t such that
A16: Z = { s: s < t } and
t <> {};
for x9 holds x9 in Z iff x9 < t
proof
let x9;
hereby
assume x9 in Z;
then ex s st s = x9 & s < t by A16;
hence x9 < t;
end;
thus thesis by A16;
end;
hence contradiction by A14;
end;
A17: Z c= RAT+
proof
let e be object;
assume e in Z;
then ex z9 st e = z9 & ex x,z st z = z9 & x in X & z < x;
hence thesis;
end;
now
assume Z = {};
then
A18: for x9 st x9 in Z holds x9 < {};
for x9 st x9 < {} holds x9 in Z by ARYTM_3:64;
hence contradiction by A14,A18;
end;
then reconsider Z as non empty Subset of RAT+ by A17;
A19: now
assume
A20: Z = RAT+;
per cases;
suppose
x1 in RAT+;
then reconsider x9 = x1 as Element of RAT+;
x9 in Z by A20;
then ex z9 st x9 = z9 & ex x,z st z = z9 & x in X & z < x;
hence contradiction by A1,A2;
end;
suppose
A21: not x1 in RAT+;
x1 in REAL+;
then x1 in IR by A21,Lm3,XBOOLE_0:def 3;
then consider A being Subset of RAT+ such that
A22: 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 Lm28;
then consider x9 being Element of RAT+ such that
A23: not x9 in A by A22,SUBSET_1:28;
reconsider x2 = x9 as Element of REAL+ by Th1;
x2 in Z by A20;
then ex z9 st x9 = z9 & ex x,z st z = z9 & x in X & z < x;
then consider x such that
A24: x in X and
A25: x2 < x;
x1 < x2 by A21,A22,A23,Def5;
then x1 < x by A25,Lm31;
hence contradiction by A1,A2,A24;
end;
end;
t in Z implies (for s st s <=' t holds s in Z) & ex s st s in Z & t < s
proof
reconsider y0 = t as Element of REAL+ by Th1;
assume t in Z;
then ex z9 st z9 = t & ex x,z st z = z9 & x in X & z < x;
then consider x0 being Element of REAL+ such that
A26: x0 in X and
A27: y0 < x0;
thus for s st s <=' t holds s in Z
proof
let s;
reconsider z = s as Element of REAL+ by Th1;
assume s <=' t;
then z <=' y0 by Lm14;
then z < x0 by A27,Lm31;
hence thesis by A26;
end;
consider z such that
A28: z in RAT+ and
A29: z < x0 and
A30: y0 < z by A27,Lm30;
reconsider z9 = z as Element of RAT+ by A28;
take z9;
thus z9 in Z by A26,A29;
thus thesis by A30,Lm14;
end;
then Z in IR;
then
A31: Z in IR \ {RAT+} by A19,ZFMISC_1:56;
then Z in IR \ {RAT+} \ RA by A15,XBOOLE_0:def 5;
then reconsider z = Z as Element of REAL+ by Lm4;
take z;
let x,y such that
A32: x in X and
A33: y in Y;
A34: now
assume z in RAT+;
then z in {{}} by A31,Lm9,XBOOLE_0:def 4;
hence contradiction by TARSKI:def 1;
end;
hereby
assume z < x;
then consider x0 being Element of REAL+ such that
A35: x0 in RAT+ and
A36: x0 < x and
A37: z < x0 by Lm30;
reconsider x9 = x0 as Element of RAT+ by A35;
x9 in z by A32,A36;
hence contradiction by A34,A37,Def5;
end;
assume y < z;
then consider y0 being Element of REAL+ such that
A38: y0 in RAT+ and
A39: y0 < z and
A40: y < y0 by Lm30;
reconsider y9 = y0 as Element of RAT+ by A38;
y9 in z by A34,A39,Def5;
then ex z9 st y9 = z9 & ex x,z st z = z9 & x in X & z < x;
then consider x0 being Element of REAL+ such that
A41: x0 in X and
A42: y0 < x0;
y < x0 by A40,A42,Lm31;
hence contradiction by A2,A33,A41;
end;
end;
Lm32: one = 1;
Lm33: {} = {};
Lm34: 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 <> {};
A4: ex A0 being Element of RAT+ st A0 in A by A2,SUBSET_1:4;
consider y9 such that
A5: y9 in B and
A6: y9 <> {} by A3,Lm15;
defpred P[Element of RAT+] means $1 *' y9 in A;
{} *' y9 = {} by ARYTM_3:48;
then
A7: P[{}] by A4,Lm16,ARYTM_3:64;
A <> RAT+ by ZFMISC_1:56;
then consider r such that
A8: not r in A by SUBSET_1:28;
consider n being Element of RAT+ such that
A9: n in omega and
A10: r <=' n *' y9 by A6,ARYTM_3:95;
A11: not P[n] by A8,A10,Lm16;
consider n0 being Element of RAT+ such that
n0 in omega and
A12: ( P[n0])& not P[n0 + one] from ARYTM_3:sch 1(Lm32,Lm33,A9,A7,A11);
(n0 + one) *' y9 = n0 *' y9 + one *' y9 by ARYTM_3:57
.= n0 *' y9 + y9 by ARYTM_3:53;
hence contradiction by A1,A5,A12;
end;
Lm35: x + y = x implies y = {}
proof
assume that
A1: x + y = x and
A2: y <> {};
A3: x <> {} by A1,A2,Th5;
then
A4: DEDEKIND_CUT x <> {} by Lm10;
DEDEKIND_CUT x = DEDEKIND_CUT GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) by A1,A2
,A3,Def8
.= DEDEKIND_CUT x + DEDEKIND_CUT y by Lm12;
then DEDEKIND_CUT y = {} by A4,Lm34;
hence contradiction by A2,Lm10;
end;
Lm36: 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 & A <> B;
not B c= A by A2;
then consider s1 being Element of RAT+ such that
A3: s1 in B & not s1 in A;
set DIF = { t : ex r,s st not r in A & s in B & r + t = s};
A4: DIF c= RAT+
proof
let e be object;
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;
s1 + {} = s1 by ARYTM_3:84;
then
A5: {} in DIF by A3;
then reconsider DIF as non empty Subset of RAT+ by A4;
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 x9 st x9 = t & ex r,s st not r in A & s in B & r + x9 = s;
then consider r0,s0 being Element of RAT+ such that
A6: not r0 in A and
A7: s0 in B and
A8: r0 + t = s0;
thus for s st s <=' t holds s in DIF
proof
let s;
assume s <=' t;
then consider p such that
A9: s + p = t;
A10: t <=' s0 by A8;
p <=' t by A9;
then p <=' s0 by A10,ARYTM_3:67;
then consider q such that
A11: p + q = s0;
r0 + s + p = q + p by A8,A9,A11,ARYTM_3:51;
then
A12: r0 + s = q by ARYTM_3:62;
q in B by A7,A11,Lm16,ARYTM_3:77;
hence thesis by A6,A12;
end;
consider s1 being Element of RAT+ such that
A13: s1 in B and
A14: s0 < s1 by A7,Lm7;
consider q such that
A15: s0 + q = s1 by A14,ARYTM_3:def 13;
take t + q;
A16: r0 + (t + q) = s1 by A8,A15,ARYTM_3:51;
hence t + q in DIF by A6,A13;
t <=' t + q & t <> t + q by A8,A14,A16;
hence thesis by ARYTM_3:68;
end;
then
A17: DIF in IR;
B <> RAT+ by ZFMISC_1:56;
then consider s2 being Element of RAT+ such that
A18: not s2 in B by SUBSET_1:28;
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;
hence contradiction by A18,Lm16,ARYTM_3:77;
end;
then DIF <> RAT+;
then reconsider DIF as Element of DEDEKIND_CUTS by A17,ZFMISC_1:56;
take DIF;
set C = { r + t : r in A & t in DIF};
B = C
proof
thus B c= C
proof
let e be object;
assume
A19: e in B;
then reconsider y9 = e as Element of RAT+;
per cases;
suppose
A20: y9 in A;
y9 = y9 + {} by ARYTM_3:84;
hence thesis by A5,A20;
end;
suppose
A21: not y9 in A;
consider s0 being Element of RAT+ such that
A22: s0 in B and
A23: y9 < s0 by A19,Lm7;
set Z = { r : ex x9 st not x9 in A & x9 + r = s0 };
A24: not s0 in A by A21,A23,Lm16;
A25: s0 + {} = s0 by ARYTM_3:84;
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
A26: r2 < s0;
then
A27: r2 <> s0;
per cases;
suppose
A28: r2 in A;
take r2,{};
thus r2 in A by A28;
thus {} in Z by A24,A25;
thus thesis by ARYTM_3:84;
end;
suppose
A29: not r2 in A;
consider q being Element of RAT+ such that
A30: r2 + q = s0 by A26,ARYTM_3:def 13;
defpred P[Element of RAT+] means $1 *' q in A;
{} *' q = {} by ARYTM_3:48;
then
A31: P[{}] by A1,Lm17;
q <> {} by A27,A30,ARYTM_3:84;
then consider n being Element of RAT+ such that
A32: n in omega and
A33: s0 <=' n *' q by ARYTM_3:95;
A34: not P[n] by A24,A33,Lm16;
consider n0 being Element of RAT+ such that
n0 in omega and
A35: P[n0] and
A36: not P[n0 + one] from ARYTM_3:sch 1(Lm32,Lm33,A32,A31,A34);
n0 *' q <=' r2 by A29,A35,Lm16;
then n0 *' q + q <=' s0 by A30,ARYTM_3:76;
then consider t such that
A37: n0 *' q + q + t = s0;
take n0 *' q, t;
thus n0 *' q in A by A35;
(n0 + one) *' q = n0 *' q + one *' q by ARYTM_3:57
.= n0 *' q + q by ARYTM_3:53;
hence t in Z by A36,A37;
n0 *' q + t + q = r2 + q by A30,A37,ARYTM_3:51;
hence thesis by ARYTM_3:62;
end;
end;
then consider s,t such that
A38: s in A and
A39: t in Z and
A40: y9 = s + t by A23;
ex r st t= r & ex x9 st not x9 in A & x9 + r = s0 by A39;
then t in DIF by A22;
hence thesis by A38,A40;
end;
end;
let e be object;
assume e in C;
then consider s3,t3 being Element of RAT+ such that
A41: e = s3 + t3 and
A42: s3 in A and
A43: t3 in DIF;
ex t st t3 = t & ex r,s st not r in A & s in B & r + t = s by A43;
then consider r4,s4 being Element of RAT+ such that
A44: not r4 in A and
A45: s4 in B and
A46: r4 + t3 = s4;
s3 <=' r4 by A42,A44,Lm16;
then s3 + t3 <=' s4 by A46,ARYTM_3:76;
hence thesis by A41,A45,Lm16;
end;
hence thesis;
end;
Lm37: x <=' y implies DEDEKIND_CUT x c= DEDEKIND_CUT y
proof
assume
A1: x <=' y;
assume
A2: not DEDEKIND_CUT x c= DEDEKIND_CUT y;
DEDEKIND_CUT x in IR & DEDEKIND_CUT y in IR by XBOOLE_0:def 5;
then DEDEKIND_CUT y c= DEDEKIND_CUT x by A2,Lm13;
then y <=' x by Lm20;
hence thesis by A1,A2,Lm21;
end;
theorem Th9:
x <=' y implies ex z st x + z = y
proof
assume
A1: x <=' y;
per cases;
suppose
A2: x = {};
take y;
thus thesis by A2,Def8;
end;
suppose
A3: x = y;
reconsider z = {} as Element of REAL+ by Th1;
take z;
thus thesis by A3,Def8;
end;
suppose that
A4: x <> {} and
A5: x <> y;
A6: DEDEKIND_CUT x <> {} by A4,Lm10;
DEDEKIND_CUT x <> DEDEKIND_CUT y by A5,Lm22;
then consider C being Element of DEDEKIND_CUTS such that
A7: DEDEKIND_CUT x + C = DEDEKIND_CUT y by A1,A6,Lm36,Lm37;
take GLUED C;
now
assume
A8: C = {};
not ex e being object st e in { r + s : r in C & s in DEDEKIND_CUT x}
proof
given e being object such that
A9: 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 A9;
hence contradiction by A8;
end;
then { r + s : r in C & s in DEDEKIND_CUT x} = {} by XBOOLE_0:def 1;
then DEDEKIND_CUT y = {} by A7,Def6;
hence contradiction by A1,A6,Lm37,XBOOLE_1:3;
end;
then GLUED C <> {} by Lm11;
hence x + GLUED C = GLUED(DEDEKIND_CUT x + DEDEKIND_CUT GLUED C) by A4,Def8
.= GLUED DEDEKIND_CUT y by A7,Lm12
.= y by Lm23;
end;
end;
theorem Th10:
ex z st x + z = y or y + z = x
proof
x <=' y or y <=' x;
hence thesis by Th9;
end;
theorem Th11:
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 Th10;
per cases by A2;
suppose
A3: z + q = y;
then x + y = x + y + q by A1,Th6;
then q = {} by Lm35;
hence thesis by A3,Def8;
end;
suppose
A4: y + q = z;
then x + z = x + z + q by A1,Th6;
then q = {} by Lm35;
hence thesis by A4,Def8;
end;
end;
Lm38: 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 object;
assume e in A *' (B *' C);
then consider r0,s0 being Element of RAT+ such that
A1: e = r0 *' s0 & r0 in A and
A2: s0 in B *' C;
consider r1,s1 being Element of RAT+ such that
A3: s0 = r1 *' s1 & r1 in B and
A4: s1 in C by A2;
e = r0 *' r1 *' s1 & r0 *' r1 in A *' B by A1,A3,ARYTM_3:52;
hence thesis by A4;
end;
Lm39: for A,B,C being Element of DEDEKIND_CUTS holds A *' (B *' C) = A *' B *'
C
by Lm38;
theorem
x *' (y *' z) = x *' y *' z
proof
thus x *' (y *' z) = GLUED(DEDEKIND_CUT x *' (DEDEKIND_CUT y *' DEDEKIND_CUT
z)) by Lm12
.= GLUED((DEDEKIND_CUT x *' DEDEKIND_CUT y) *' DEDEKIND_CUT z) by Lm39
.= x *' y *' z by Lm12;
end;
Lm40: x *' y = {} implies x = {} or y = {}
proof
assume
A1: x *' y = {};
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:4;
assume DEDEKIND_CUT y <> {};
then consider s0 being Element of RAT+ such that
A3: s0 in DEDEKIND_CUT y by SUBSET_1:4;
r0 *' s0 in { r *' s: r in DEDEKIND_CUT x & s in DEDEKIND_CUT y} by A2,A3;
hence contradiction by A1,Lm11;
end;
hence thesis by Lm10;
end;
Lm41: 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 object;
assume e in A *' (B + C);
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;
consider s0,t0 being Element of RAT+ such that
A4: v0 = s0 + t0 and
A5: s0 in B & t0 in C by A3;
A6: e = r0 *' s0 + r0 *' t0 by A1,A4,ARYTM_3:57;
r0 *' s0 in A *' B & r0 *' t0 in A *' C by A2,A5;
hence thesis by A6;
end;
let e be object;
assume e in A *' B + A *' C;
then consider s1,t1 being Element of RAT+ such that
A7: e = s1 + t1 and
A8: s1 in A *' B and
A9: t1 in A *' C;
consider r0,s0 being Element of RAT+ such that
A10: s1 = r0 *' s0 and
A11: r0 in A and
A12: s0 in B by A8;
consider r09,t0 being Element of RAT+ such that
A13: t1 = r09 *' t0 and
A14: r09 in A and
A15: t0 in C by A9;
per cases;
suppose
r0 <=' r09;
then r0 *' s0 <=' r09 *' s0 by ARYTM_3:82;
then consider s09 being Element of RAT+ such that
A16: r0 *' s0 = r09 *' s09 and
A17: s09 <=' s0 by ARYTM_3:79;
s09 in B by A12,A17,Lm16;
then
A18: s09 + t0 in B + C by A15;
e = r09 *' (s09 + t0) by A7,A10,A13,A16,ARYTM_3:57;
hence thesis by A14,A18;
end;
suppose
r09 <=' r0;
then r09 *' t0 <=' r0 *' t0 by ARYTM_3:82;
then consider t09 being Element of RAT+ such that
A19: r09 *' t0 = r0 *' t09 and
A20: t09 <=' t0 by ARYTM_3:79;
t09 in C by A15,A20,Lm16;
then
A21: s0 + t09 in B + C by A12;
e = r0 *' (s0 + t09) by A7,A10,A13,A19,ARYTM_3:57;
hence thesis by A11,A21;
end;
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;
end;
suppose
A2: y = {};
hence x *' (y + z) = x *' z by Def8
.= y + x *' z by A2,Def8
.= (x *' y) + (x *' z) by A2,Th4;
end;
suppose
A3: z = {};
hence x *' (y + z) = x *' y by Def8
.= x *' y + z by A3,Def8
.= (x *' y) + (x *' z) by A3,Th4;
end;
suppose that
A4: x <> {} and
A5: y <> {} & z <> {};
A6: x *' y <> {} & x *' z <> {} by A4,A5,Lm40;
thus x *' (y + z) = GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT GLUED(
DEDEKIND_CUT y + DEDEKIND_CUT z)) by A5,Def8
.= GLUED(DEDEKIND_CUT x *' (DEDEKIND_CUT y + DEDEKIND_CUT z)) by Lm12
.= GLUED((DEDEKIND_CUT x *' DEDEKIND_CUT y) + (DEDEKIND_CUT x *'
DEDEKIND_CUT z)) by Lm41
.= GLUED((DEDEKIND_CUT x *' DEDEKIND_CUT y) + DEDEKIND_CUT (x*'z)) by
Lm12
.= GLUED(DEDEKIND_CUT(x*'y) + DEDEKIND_CUT (x*'z)) by Lm12
.= (x *' y) + (x *' z) by A6,Def8;
end;
end;
Lm42: 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:4;
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 and
r3 in A and
A10: r1 <> r2 and
r2 <> r3 and
r3 <> r1 by A5,A6,A8,ARYTM_3:75;
r1 <> {} or r2 <> {} by A10;
hence thesis by A3,A9;
end;
Lm43:for rone be Element of REAL+ st rone=one
for A being Element of DEDEKIND_CUTS st A <> {} ex B being Element of
DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone
proof
let rone be Element of REAL+ such that A0: rone=one;
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:54;
set B = { s : s < s0 };
B c= RAT+
proof
let e be object;
assume e in B;
then ex s st s = e & s < s0;
hence thesis;
end;
then reconsider B as Subset of 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
A5: ex s st s = r & s < s0;
then consider t such that
A6: r < t and
A7: t < s0 by ARYTM_3:93;
thus for s st s <=' r holds s in B
proof
let s;
assume s <=' r;
then s < s0 by A5,ARYTM_3:69;
hence thesis;
end;
take t;
thus t in B by A7;
thus thesis by A6;
end;
then
A8: B in IR;
not ex s st s = s0 & s < s0;
then not s0 in B;
then B <> RAT+;
then reconsider B as Element of DEDEKIND_CUTS by A8,ZFMISC_1:56;
A9: A *' B = { s : s < r0 *' s0 }
proof
thus A *' B c= { s : s < r0 *' s0 }
proof
let e be object;
assume e in A *' B;
then consider r1,s1 being Element of RAT+ such that
A10: e = r1 *' s1 and
A11: r1 in A and
A12: s1 in B;
ex s st s = r1 & s < r0 by A2,A11;
then
A13: r1 *' s1 <=' r0 *' s1 by ARYTM_3:82;
A14: ex s st s = s1 & s < s0 by A12;
then s1 <> s0;
then
A15: r0 *' s1 <> r0 *' s0 by A3,ARYTM_3:56;
r0 *' s1 <=' r0 *' s0 by A14,ARYTM_3:82;
then r0 *' s1 < r0 *' s0 by A15,ARYTM_3:68;
then r1 *' s1 < r0 *' s0 by A13,ARYTM_3:69;
hence thesis by A10;
end;
let e be object;
assume e in { s : s < r0 *' s0 };
then consider s1 being Element of RAT+ such that
A16: e = s1 and
A17: s1 < r0 *' s0;
consider t0 being Element of RAT+ such that
A18: s1 = r0 *' t0 and
A19: t0 <=' s0 by A17,ARYTM_3:79;
t0 <> s0 by A17,A18;
then t0 < s0 by A19,ARYTM_3:68;
then t0 in B;
then consider t1 being Element of RAT+ such that
A20: t1 in B and
A21: t0 < t1 by Lm7;
r0 *' t0 <=' t1 *' r0 by A21,ARYTM_3:82;
then consider r1 being Element of RAT+ such that
A22: r0 *' t0 = t1 *' r1 and
A23: r1 <=' r0 by ARYTM_3:79;
t0 <> t1 by A21;
then r1 <> r0 by A3,A22,ARYTM_3:56;
then r1 < r0 by A23,ARYTM_3:68;
then r1 in A by A2;
hence thesis by A16,A18,A20,A22;
end;
ex t0 being Element of RAT+ st t0 = rone & DEDEKIND_CUT rone = { s :
s < t0 } by Def3,A0;
hence thesis by A4,A9,A0;
end;
suppose
A24: not A in RA;
set B = { y9 : ex x9 st not x9 in A & x9 *' y9 <=' one };
A25: B c= RAT+
proof
let e be object;
assume e in B;
then ex y9 st y9 = e & ex x9 st not x9 in A & x9 *' y9 <=' one;
hence thesis;
end;
A26: A <> RAT+ by ZFMISC_1:56;
then consider x0 being Element of RAT+ such that
A27: not x0 in A by SUBSET_1:28;
x0 *' {} = {} by ARYTM_3:48;
then x0 *' {} <=' one by ARYTM_3:64;
then
A28: {} in B by A27;
then reconsider B as non empty Subset of RAT+ by A25;
A29: A in IR by ZFMISC_1:56;
ex x9 st x9 in A by A1,SUBSET_1:4;
then
A30: {} in A by A29,Lm29,ARYTM_3:64;
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 y9 st r = y9 & ex x9 st not x9 in A & x9 *' y9 <=' one;
then consider x9 such that
A31: not x9 in A and
A32: x9 *' r <=' one;
thus for s st s <=' r holds s in B
proof
let s;
assume s <=' r;
then x9 *' s <=' x9 *' r by ARYTM_3:82;
then x9 *' s <=' one by A32,ARYTM_3:67;
hence thesis by A31;
end;
A in DEDEKIND_CUTS \ RA by A24,XBOOLE_0:def 5;
then consider x99 being Element of RAT+ such that
A33: not x99 in A and
A34: x99 < x9 by A1,A31,Lm18;
consider s such that
A35: one = x99 *' s by A30,A33,ARYTM_3:55;
take s;
x99 *' s <=' one by A35;
hence s in B by A33;
A36: s <> {} by A35,ARYTM_3:48;
x99 *' r <=' x9 *' r by A34,ARYTM_3:82;
then x99 *' r <=' x99 *' s by A32,A35,ARYTM_3:67;
then
A37: r <=' s by A30,A33,ARYTM_3:80;
x99 <> x9 & x99 *' s <=' x9 *' s by A34,ARYTM_3:82;
then r <> s by A32,A35,A36,ARYTM_3:56,66;
hence thesis by A37,ARYTM_3:68;
end;
then
A38: B in IR;
consider x9 such that
A39: x9 in A and
A40: x9 <> {} by A1,A29,Lm42;
consider y9 such that
A41: x9 *' y9 = one by A40,ARYTM_3:55;
now
assume y9 in B;
then
A42: ex s st s = y9 & ex x9 st not x9 in A & x9 *' s <=' one;
y9 <> {} by A41,ARYTM_3:48;
hence contradiction by A29,A39,A41,A42,Lm29,ARYTM_3:80;
end;
then B <> RAT+;
then not B in {RAT+} by TARSKI:def 1;
then reconsider B as Element of DEDEKIND_CUTS by A38,XBOOLE_0:def 5;
take B;
for r holds r in A *' B iff r < one
proof
let r;
hereby
assume r in A *' B;
then consider s,t such that
A43: r = s *' t and
A44: s in A and
A45: t in B;
ex z9 st z9 = t & ex x9 st not x9 in A & x9 *' z9 <=' one by A45;
then consider x9 such that
A46: not x9 in A and
A47: x9 *' t <=' one;
s <=' x9 by A29,A44,A46,Lm29;
then
A48: s *' t <=' x9 *' t by ARYTM_3:82;
A49: now
assume
A50: r = one;
then t <> {} by A43,ARYTM_3:48;
hence contradiction by A43,A44,A46,A47,A48,A50,ARYTM_3:56,66;
end;
r <=' one by A43,A47,A48,ARYTM_3:67;
hence r < one by A49,ARYTM_3:68;
end;
assume
A51: r < one;
then
A52: r <> one;
per cases;
suppose
r = {};
then r = {}*'{} by ARYTM_3:48;
hence thesis by A28,A30;
end;
suppose
r <> {};
then consider r9 being Element of RAT+ such that
A53: r *' r9 = one by ARYTM_3:55;
{ r *' s : s in A } c= RAT+
proof
let e be object;
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+;
consider dr being Element of RAT+ such that
A54: r + dr = one by A51,ARYTM_3:def 13;
consider xx being Element of RAT+ such that
A55: not xx in A by A26,SUBSET_1:28;
set rr = x9 *' dr;
dr <> {} by A52,A54,ARYTM_3:50;
then consider n0 being Element of RAT+ such that
A56: n0 in omega and
A57: xx <=' n0 *' rr by A40,ARYTM_3:78,95;
defpred P[Element of RAT+] means $1 *' rr in A;
A58: P[{}] by A30,ARYTM_3:48;
A59: not P[n0] by A29,A55,A57,Lm29;
consider n1 being Element of RAT+ such that
n1 in omega and
A60: P[n1] and
A61: not P[n1 + one] from ARYTM_3:sch 1(Lm32,Lm33,A56,A58,A59);
set s0 = n1 *' rr;
A62: now
assume n1 *' rr in rA;
then consider s0 being Element of RAT+ such that
A63: r *' s0 = n1 *' rr and
A64: s0 in A;
A65: (n1 + one) *' rr = n1 *' rr + one *' rr by ARYTM_3:57
.= r *' s0 + dr *' x9 by A63,ARYTM_3:53;
s0 <=' x9 or x9 <=' s0;
then consider s1 being Element of RAT+ such that
A66: s1 = s0 & x9 <=' s1 or s1 = x9 & s0 <=' s1;
dr *' x9 <=' dr *' s1 by A66,ARYTM_3:82;
then
A67: r *' s1 + dr *' x9 <=' r *' s1 + dr *' s1 by ARYTM_3:76;
r *' s0 <=' r *' s1 by A66,ARYTM_3:82;
then
A68: r *' s0 + dr *' x9 <=' r *' s1 + dr *' x9 by ARYTM_3:76;
r *' s1 + dr *' s1 = (r + dr) *' s1 by ARYTM_3:57
.= s1 by A54,ARYTM_3:53;
hence contradiction by A29,A39,A61,A64,A65,A66,A68,A67,Lm29;
end;
A69: now
assume
A70: s0 *' r9 in A;
r *' (s0 *' r9) = one *' s0 by A53,ARYTM_3:52
.= s0 by ARYTM_3:53;
hence contradiction by A62,A70;
end;
r *' {} = {} by ARYTM_3:48;
then {} in rA by A30;
then consider s9 being Element of RAT+ such that
A71: s0 *' s9 = one by A62,ARYTM_3:55;
A72: s0 *' (r *' s9) = s0 *' s9 *' r by ARYTM_3:52
.= r by A71,ARYTM_3:53;
s0 *' r9 *' (r *' s9) = s0 *' r9 *' r *' s9 by ARYTM_3:52
.= s0 *' one *' s9 by A53,ARYTM_3:52
.= one by A71,ARYTM_3:53;
then s0 *' r9 *' (r *' s9) <=' one;
then r *' s9 in B by A69;
hence thesis by A60,A72;
end;
end;
then DEDEKIND_CUT GLUED(A *' B) = DEDEKIND_CUT rone by A0,Def4;
hence thesis by Lm12;
end;
end;
theorem
x <> {} implies ex y st x *' y = one
proof
reconsider rone =one as Element of REAL+ by Th1;
assume x <> {};
then DEDEKIND_CUT x <> {} by Lm10;
then consider B being Element of DEDEKIND_CUTS such that
A1: DEDEKIND_CUT x *' B = DEDEKIND_CUT rone by Lm43;
take y = GLUED B;
thus x *' y = GLUED DEDEKIND_CUT rone by A1,Lm12
.= one by Lm23;
end;
Lm44: 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 };
thus A *' B c= B
proof
let e be object;
assume e in A *' B;
then consider r,s such that
A2: e = r *' s and
A3: r in A and
A4: s in B;
ex t st t = r & t < one by A1,A3;
then r *' s <=' one *' s by ARYTM_3:82;
then r *' s <=' s by ARYTM_3:53;
hence thesis by A2,A4,Lm16;
end;
let e be object;
assume
A5: e in B;
then reconsider s = e as Element of RAT+;
consider s1 being Element of RAT+ such that
A6: s1 in B and
A7: s < s1 by A5,Lm7;
s1 <> {} by A7,ARYTM_3:64;
then consider s2 being Element of RAT+ such that
A8: s1 *' s2 = s by ARYTM_3:55;
A9: now
assume s2 = one;
then s = s1 by A8,ARYTM_3:53;
hence contradiction by A7;
end;
one *' s = s2 *' s1 by A8,ARYTM_3:53;
then s2 <=' one by A7,ARYTM_3:83;
then s2 < one by A9,ARYTM_3:68;
then s2 in A by A1;
hence thesis by A6,A8;
end;
theorem
x = one implies x *' y = y
proof
assume
A1: x = one;
then ex r st x = r & DEDEKIND_CUT x = { s : s < r } by Def3;
hence x *' y = GLUED DEDEKIND_CUT y by A1,Lm44
.= y by Lm23;
end;
Lm45: for i,j being Element of omega, x9,y9 st i = x9 & j = y9 holds i +^ j =
x9 + y9
proof
let i,j be Element of omega, x9,y9;
set a = (denominator x9)*^(denominator y9), b = (numerator x9)*^(denominator
y9)+^(numerator y9)*^(denominator x9);
assume
A1: i = x9;
then
A2: denominator x9 = one by ARYTM_3:def 9;
assume
A3: j = y9;
then
A4: denominator y9 = one by ARYTM_3:def 9;
then
A5: a = one by A2,ORDINAL2:39;
then
A6: RED(a,b) = one by ARYTM_3:24;
b = (numerator x9)*^one+^(numerator y9) by A2,A4,ORDINAL2:39
.= (numerator x9)+^(numerator y9) by ORDINAL2:39
.= i+^(numerator y9) by A1,ARYTM_3:def 8
.= i +^ j by A3,ARYTM_3:def 8;
hence i +^ j = RED(b,a) by A5,ARYTM_3:24
.= x9 + y9 by A6,ARYTM_3:def 10;
end;
Lm46: z9 < x9 + y9 & x9 <> {} & y9 <> {} implies ex r,s st z9 = r + s & r < x9
& s < y9
proof
assume that
A1: z9 < x9 + y9 and
A2: x9 <> {} and
A3: y9 <> {};
consider r0,t0 being Element of RAT+ such that
A4: z9 = r0 + t0 and
A5: r0 <=' x9 and
A6: t0 <=' y9 & t0 <> y9 by A1,A3,ARYTM_3:90;
per cases;
suppose
A7: r0 = {};
take {},t0;
thus z9 = {} + t0 by A4,A7;
{} <=' x9 by ARYTM_3:64;
hence {} < x9 by A2,ARYTM_3:68;
thus thesis by A6,ARYTM_3:68;
end;
suppose
A8: r0 <> {};
t0 < y9 by A6,ARYTM_3:68;
then consider t1 being Element of RAT+ such that
A9: t0 < t1 and
A10: t1 < y9 by ARYTM_3:93;
z9 < t1 + r0 by A4,A9,ARYTM_3:76;
then consider t2,r1 being Element of RAT+ such that
A11: z9 = t2 + r1 and
A12: t2 <=' t1 and
A13: r1 <=' r0 & r1 <> r0 by A8,ARYTM_3:90;
take r1,t2;
thus z9 = r1 + t2 by A11;
r1 < r0 by A13,ARYTM_3:68;
hence r1 < x9 by A5,ARYTM_3:69;
thus thesis by A10,A12,ARYTM_3:69;
end;
end;
Lm47: x in RAT+ & y in RAT+ implies ex x9,y9 st x = x9 & y = y9 & x + y = x9 +
y9
proof
assume that
A1: x in RAT+ and
A2: y in RAT+;
per cases;
suppose
A3: x = {};
reconsider y9 = y as Element of RAT+ by A2;
take {},y9;
thus x = {} by A3;
thus y = y9;
thus x + y = y by A3,Def8
.= {} + y9 by ARYTM_3:50;
end;
suppose
A4: y = {};
reconsider x9 = x as Element of RAT+ by A1;
take x9,{};
thus x = x9;
thus y = {} by A4;
thus x + y = x by A4,Def8
.= x9 + {} by ARYTM_3:50;
end;
suppose that
A5: y <> {} & x <> {};
set A = DEDEKIND_CUT x, B = DEDEKIND_CUT y;
consider x9 such that
A6: x = x9 and
A7: DEDEKIND_CUT x = { s : s < x9 } by A1,Def3;
consider y9 such that
A8: y = y9 and
A9: DEDEKIND_CUT y = { s : s < y9 } by A2,Def3;
A10: for s holds s in DEDEKIND_CUT x + DEDEKIND_CUT y iff s < x9 + y9
proof
let s2 be Element of RAT+;
thus s2 in A + B implies s2 < x9 + y9
proof
assume s2 in A + B;
then consider r1,s1 being Element of RAT+ such that
A11: s2 = r1 + s1 and
A12: r1 in A and
A13: s1 in B;
ex s st s = r1 & s < x9 by A7,A12;
then
A14: r1 + s1 <=' x9 + s1 by ARYTM_3:76;
ex s st s = s1 & s < y9 by A9,A13;
then x9 + s1 < x9 + y9 by ARYTM_3:76;
hence thesis by A11,A14,ARYTM_3:69;
end;
assume s2 < x9 + y9;
then consider t2,t0 being Element of RAT+ such that
A15: s2 = t2 + t0 and
A16: t2 < x9 & t0 < y9 by A5,A6,A8,Lm46;
t0 in B & t2 in A by A7,A9,A16;
hence thesis by A15;
end;
then consider r such that
A17: GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) = r and
A18: for s holds s in DEDEKIND_CUT x + DEDEKIND_CUT y iff s < r by Def4;
A19: for s holds s < x9 + y9 iff s < r by A10,A18;
take x9,y9;
thus x = x9 & y = y9 by A6,A8;
thus x + y = GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y) by A5,Def8
.= x9 + y9 by A17,A19,Lm6;
end;
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 x9,y9 being Element of RAT+ such that
A2: x = x9 & y = y9 and
A3: x + y = x9 + y9 by A1,Lm5,Lm47;
x9 + y9 = x0 +^ y0 by A2,Lm45;
hence thesis by A3,ORDINAL1:def 12;
end;
theorem
for A being Subset of REAL+ st 0 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[0] and
A2: for x,y st x in A & y = one holds x + y in A;
let e be object;
assume e in omega;
then reconsider a = e as natural Ordinal;
A3: for a being natural Ordinal st P[a] holds P[succ a]
proof
reconsider rone = one as Element of REAL+ by Th1;
let a be natural Ordinal;
assume
A4: a in A;
reconsider i = a as Element of omega by ORDINAL1:def 12;
A5: a in omega by ORDINAL1:def 12;
then a in RAT+ by Lm5;
then reconsider x = a as Element of REAL+ by Th1;
consider x9, y9 being Element of RAT+ such that
A6: x = x9 & rone = y9 and
A7: x + rone = x9 + y9 by A5,Lm5,Lm47;
x9 + y9 = i +^ 1 by A6,Lm45
.= succ i by ORDINAL2:31;
hence thesis by A2,A4,A7;
end;
P[a] from ORDINAL2:sch 17(A1,A3);
hence thesis;
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 reconsider m = x as Element of omega;
reconsider x9 = x as Element of RAT+ by A1,Lm5;
let y;
A2: x c= omega by A1,ORDINAL1:def 2;
hereby
assume
A3: y in x;
then reconsider n = y as Element of omega by A2;
thus y in omega by A2,A3;
then reconsider y9 = y as Element of RAT+ by Lm5;
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:27;
C c= m by A4,ORDINAL3:24;
then reconsider C as Element of omega by ORDINAL1:12;
reconsider z9 = C as Element of RAT+ by Lm5;
x9 = y9 + z9 by A4,Lm45;
then y9 <=' x9;
hence y <=' x by Lm14;
end;
assume
A5: y in omega;
then reconsider y9 = y as Element of RAT+ by Lm5;
reconsider n = y as Element of omega by A5;
assume
A6: y <> x;
assume y <=' x;
then y9 <=' x9 by Lm14;
then consider z9 such that
A7: y9 + z9 = x9;
reconsider k = z9 as Element of omega by A1,A5,A7,ARYTM_3:71;
n +^ k = m by A7,Lm45;
then n c= m by ORDINAL3:24;
then n c< m by A6;
hence thesis by ORDINAL1:11;
end;
theorem
x = y + z implies z <=' x
proof
reconsider zz = {} as Element of REAL+ by Th1;
assume
A1: x = y + z;
assume
A2: not z <=' x;
then consider y0 being Element of REAL+ such that
A3: x + y0 = z by Th9;
x = x + (y + y0) by A1,A3,Th6;
then x + zz = x + (y + y0) by Def8;
then y0 = {} by Th5,Th11;
then z = x by A3,Def8;
hence thesis by A2;
end;
theorem
{} in REAL+ & one in REAL+
by Th1;
theorem
x in RAT+ & y in RAT+ implies ex x9,y9 st x = x9 & y = y9 & x *' y = x9 *' y9
proof
assume that
A1: x in RAT+ and
A2: y in RAT+;
per cases;
suppose
A3: x = {};
reconsider y9 = y as Element of RAT+ by A2;
take {},y9;
thus x = {} by A3;
thus y = y9;
thus x *' y = {} by A3,Th4
.= {} *' y9 by ARYTM_3:48;
end;
suppose
A4: y = {};
reconsider x9 = x as Element of RAT+ by A1;
take x9,{};
thus x = x9;
thus y = {} by A4;
thus x *' y = {} by A4,Th4
.= x9 *' {} by ARYTM_3:48;
end;
suppose that
y <> {} and
A5: x <> {};
consider y9 such that
A6: y = y9 and
A7: DEDEKIND_CUT y = { s : s < y9 } by A2,Def3;
set A = DEDEKIND_CUT x, B = DEDEKIND_CUT y;
consider x9 such that
A8: x = x9 and
A9: DEDEKIND_CUT x = { s : s < x9 } by A1,Def3;
A10: for s holds s in DEDEKIND_CUT x *' DEDEKIND_CUT y iff s < x9 *' y9
proof
let s2 be Element of RAT+;
thus s2 in A *' B implies s2 < x9 *' y9
proof
assume s2 in A *' B;
then consider r1,s1 being Element of RAT+ such that
A11: s2 = r1 *' s1 and
A12: r1 in A and
A13: s1 in B;
ex s st s = r1 & s < x9 by A9,A12;
then
A14: r1 *' s1 <=' x9 *' s1 by ARYTM_3:82;
A15: ex s st s = s1 & s < y9 by A7,A13;
then s1 <> y9;
then
A16: x9 *' s1 <> x9 *' y9 by A5,A8,ARYTM_3:56;
x9 *' s1 <=' x9 *' y9 by A15,ARYTM_3:82;
then x9 *' s1 < x9 *' y9 by A16,ARYTM_3:68;
hence thesis by A11,A14,ARYTM_3:69;
end;
assume
A17: s2 < x9 *' y9;
then consider t0 being Element of RAT+ such that
A18: s2 = x9 *' t0 and
A19: t0 <=' y9 by ARYTM_3:79;
t0 <> y9 by A17,A18;
then t0 < y9 by A19,ARYTM_3:68;
then consider t1 being Element of RAT+ such that
A20: t0 < t1 and
A21: t1 < y9 by ARYTM_3:93;
s2 <=' t1 *' x9 by A18,A20,ARYTM_3:82;
then consider t2 being Element of RAT+ such that
A22: s2 = t1 *' t2 and
A23: t2 <=' x9 by ARYTM_3:79;
now
assume t2 = x9;
then t0 = t1 by A5,A8,A18,A22,ARYTM_3:56;
hence contradiction by A20;
end;
then t2 < x9 by A23,ARYTM_3:68;
then
A24: t2 in A by A9;
t1 in B by A7,A21;
hence thesis by A22,A24;
end;
then consider r such that
A25: GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT y) = r and
A26: for s holds s in DEDEKIND_CUT x *' DEDEKIND_CUT y iff s < r by Def4;
take x9,y9;
thus x = x9 & y = y9 by A8,A6;
for s holds s < x9 *' y9 iff s < r by A10,A26;
hence thesis by A25,Lm6;
end;
end;