arytm_2.miz
begin
reserve r,s,t,x9,y9,z9,p,q for
Element of
RAT+ ;
definition
::
ARYTM_2:def1
func
DEDEKIND_CUTS ->
Subset-Family of
RAT+ equals ({ A where A be
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 be
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 be
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 be
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
::
ARYTM_2:def2
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 be
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 be
object st
[x, y]
in IR
proof
given x,y be
object such that
A1:
[x, y]
in IR;
consider A be
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 be
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 ::
ARYTM_2:1
Th1:
RAT+
c=
REAL+ by
Lm2,
XBOOLE_1: 7,
XBOOLE_1: 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 be
Element of
omega : (c,d)
are_coprime & d
<>
{} }
\ the set of all
[k, 1] where k be
Element of
omega )
\/
omega ) by
XBOOLE_1: 7;
theorem ::
ARYTM_2:2
omega
c=
REAL+ by
Lm5,
Th1;
registration
cluster
REAL+ -> non
empty;
coherence by
Th1;
end
definition
let x;
::
ARYTM_2:def3
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 be
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 be
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 ::
ARYTM_2:3
not ex y be
object st
[
{} , y]
in
REAL+
proof
given y be
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 ;
::
ARYTM_2:def4
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 be
Element of
RAT+ such that
A1: IT1
= r1 and
A2: for s holds s
in x iff s
< r1;
given r2 be
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 be
set st B
in
DEDEKIND_CUTS & r
in B holds 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 be
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 be
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 be
object st e
in { s : s
<
{} }
proof
given e be
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 be
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 be
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 be
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 be
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 be
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+ ;
::
ARYTM_2:def5
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 be
set st B
in
DEDEKIND_CUTS & B
<>
{} holds 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 be
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 be
Element of
RAT+ such that
A5: r0
in A by
SUBSET_1: 4;
consider r1 be
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 be
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 be
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 be
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 be
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 be
set st B
in (
DEDEKIND_CUTS
\ RA) & not r
in B & B
<>
{} holds 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 be
Element of
RAT+ such that
A7: y
= ry and
A8: (
DEDEKIND_CUT y)
= { s : s
< ry } by
A6,
Def3;
consider rx be
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 be
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 be
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 be
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 be
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 ;
::
ARYTM_2:def6
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 be
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 be
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 be
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 be
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 be
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 be
set st B
in
DEDEKIND_CUTS holds 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 ;
::
ARYTM_2:def7
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 be
object st e
in { (r
*' s) : r
in A & s
in B }
proof
given e be
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 be
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 be
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 be
Element of
RAT+ such that
A9: t0
in B and
A10: s0
< t0 by
A6,
Lm7;
per cases ;
suppose
A11: r0
=
{} ;
consider r1 be
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 be
Element of
RAT+ such that
A19: not r0
in A by
Lm24;
consider s0 be
Element of
RAT+ such that
A20: not s0
in B by
Lm24;
now
assume (r0
*' s0)
in C;
then
consider r1,s1 be
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+ ;
::
ARYTM_2:def8
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 ;
::
ARYTM_2:def9
func x
*' y ->
Element of
REAL+ equals (
GLUED ((
DEDEKIND_CUT x)
*' (
DEDEKIND_CUT y)));
coherence ;
commutativity ;
end
theorem ::
ARYTM_2:4
Th4: x
=
{} implies (x
*' y)
=
{}
proof
set A = (
DEDEKIND_CUT x), B = (
DEDEKIND_CUT y);
assume
A1: x
=
{} ;
not ex e be
object st e
in { (r
*' s) : r
in A & s
in B }
proof
given e be
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 ::
ARYTM_2:5
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 be
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 be
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 be
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 be
Element of
RAT+ such that
A1: e
= (r0
+ s0) & r0
in A and
A2: s0
in (B
+ C);
consider r1,s1 be
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 be
Element of
DEDEKIND_CUTS holds (A
+ (B
+ C))
= ((A
+ B)
+ C) by
Lm25;
Lm27: for A,B be
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 be
Element of
RAT+ such that
A2: r0
in A by
SUBSET_1: 4;
assume B
<>
{} ;
then
consider s0 be
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 ::
ARYTM_2:6
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 ::
ARYTM_2:7
{ A where A be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 ::
ARYTM_2:8
for X,Y be
Subset of
REAL+ st (ex x st x
in Y) & for x, y st x
in X & y
in Y holds x
<=' y holds 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 be
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 be
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 be
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 be
Element of
RAT+ st y9
= y99 & ex x, z st z
= y99 & x
in X & z
< x;
then
consider x1,y1 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
Element of
DEDEKIND_CUTS st A
<>
{} & A
c= B & A
<> B holds ex C be
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 be
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 be
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 be
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 be
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 be
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 be
Element of
RAT+ st r2
< s0 holds 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 be
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 be
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 be
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 be
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 be
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 ::
ARYTM_2:9
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 be
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 be
object st e
in { (r
+ s) : r
in C & s
in (
DEDEKIND_CUT x) }
proof
given e be
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 ::
ARYTM_2:10
Th10: ex z st (x
+ z)
= y or (y
+ z)
= x
proof
x
<=' y or y
<=' x;
hence thesis by
Th9;
end;
theorem ::
ARYTM_2:11
Th11: (x
+ y)
= (x
+ z) implies y
= z
proof
assume
A1: (x
+ y)
= (x
+ z);
consider q be
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 be
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 be
Element of
RAT+ such that
A1: e
= (r0
*' s0) & r0
in A and
A2: s0
in (B
*' C);
consider r1,s1 be
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 be
Element of
DEDEKIND_CUTS holds (A
*' (B
*' C))
= ((A
*' B)
*' C) by
Lm38;
theorem ::
ARYTM_2:12
(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 be
Element of
RAT+ such that
A2: r0
in (
DEDEKIND_CUT x) by
SUBSET_1: 4;
assume (
DEDEKIND_CUT y)
<>
{} ;
then
consider s0 be
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 be
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 be
Element of
RAT+ such that
A1: e
= (r0
*' v0) and
A2: r0
in A and
A3: v0
in (B
+ C);
consider s0,t0 be
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 be
Element of
RAT+ such that
A7: e
= (s1
+ t1) and
A8: s1
in (A
*' B) and
A9: t1
in (A
*' C);
consider r0,s0 be
Element of
RAT+ such that
A10: s1
= (r0
*' s0) and
A11: r0
in A and
A12: s0
in B by
A8;
consider r09,t0 be
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 be
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 be
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 ::
ARYTM_2:13
(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 be
set st B
in IR & B
<>
{} holds ex r st r
in B & r
<>
{}
proof
let B be
set such that
A1: B
in IR and
A2: B
<>
{} ;
consider A be
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 be
Element of
RAT+ such that
A5: r0
in A by
A2,
A3,
SUBSET_1: 4;
consider r1 be
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 be
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 holds for A be
Element of
DEDEKIND_CUTS st A
<>
{} holds ex B be
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 be
Element of
RAT+ such that
A2: A
= { s : s
< r0 } and
A3: r0
<>
{} ;
consider s0 be
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 be
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 be
Element of
RAT+ such that
A16: e
= s1 and
A17: s1
< (r0
*' s0);
consider t0 be
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 be
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 be
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 be
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 be
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 be
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,
ARYTM_3: 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,
ARYTM_3: 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 be
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 be
Element of
RAT+ such that
A54: (r
+ dr)
=
one by
A51,
ARYTM_3:def 13;
consider xx be
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 be
Element of
RAT+ such that
A56: n0
in
omega and
A57: xx
<=' (n0
*' rr) by
A40,
ARYTM_3: 78,
ARYTM_3: 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 be
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 be
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 be
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 be
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 ::
ARYTM_2:14
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 be
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 be
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 be
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 be
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 ::
ARYTM_2:15
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 be
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 be
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 be
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 be
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 be
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 be
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 ::
ARYTM_2:16
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 be
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 ::
ARYTM_2:17
for A be
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 be
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 be
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 ::
ARYTM_2:18
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 be
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 ::
ARYTM_2:19
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 be
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 ::
ARYTM_2:20
{}
in
REAL+ &
one
in
REAL+ by
Th1;
theorem ::
ARYTM_2:21
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 be
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 be
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 be
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 be
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;