:: ARYTM_2 semantic presentation
begin
definition
func DEDEKIND_CUTS -> Subset-Family of RAT+ equals :: ARYTM_2:def 1
{ A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } \ {RAT+};
coherence
{ A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } \ {RAT+} is Subset-Family of RAT+
proof
set C = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
{ A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } c= bool RAT+
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } or e in bool RAT+ )
assume e in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; ::_thesis: e in bool RAT+
then ex A being Subset of RAT+ st
( e = A & ( for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) ) ) ;
hence e in bool RAT+ ; ::_thesis: verum
end;
hence { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } \ {RAT+} is Subset-Family of RAT+ by XBOOLE_1:1; ::_thesis: verum
end;
end;
:: deftheorem defines DEDEKIND_CUTS ARYTM_2:def_1_:_
DEDEKIND_CUTS = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } \ {RAT+};
registration
cluster DEDEKIND_CUTS -> non empty ;
coherence
not DEDEKIND_CUTS is empty
proof
set X = { s where s is Element of RAT+ : s < one } ;
A1: { s where s is Element of RAT+ : s < one } c= RAT+
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { s where s is Element of RAT+ : s < one } or e in RAT+ )
assume e in { s where s is Element of RAT+ : s < one } ; ::_thesis: e in RAT+
then ex s being Element of RAT+ st
( s = e & s < one ) ;
hence e in RAT+ ; ::_thesis: verum
end;
now__::_thesis:_not_one_in__{__s_where_s_is_Element_of_RAT+_:_s_<_one__}_
assume one in { s where s is Element of RAT+ : s < one } ; ::_thesis: contradiction
then ex s being Element of RAT+ st
( s = one & s < one ) ;
hence contradiction ; ::_thesis: verum
end;
then A2: { s where s is Element of RAT+ : s < one } <> RAT+ ;
{} <=' one by ARYTM_3:64;
then {} < one by ARYTM_3:68;
then {} in { s where s is Element of RAT+ : s < one } ;
then reconsider X = { s where s is Element of RAT+ : s < one } as non empty Subset of RAT+ by A1;
for r being Element of RAT+ st r in X holds
( ( for s being Element of RAT+ st s <=' r holds
s in X ) & ex s being Element of RAT+ st
( s in X & r < s ) )
proof
let r be Element of RAT+ ; ::_thesis: ( r in X implies ( ( for s being Element of RAT+ st s <=' r holds
s in X ) & ex s being Element of RAT+ st
( s in X & r < s ) ) )
assume r in X ; ::_thesis: ( ( for s being Element of RAT+ st s <=' r holds
s in X ) & ex s being Element of RAT+ st
( s in X & r < s ) )
then A3: ex s being Element of RAT+ st
( s = r & s < one ) ;
thus for s being Element of RAT+ st s <=' r holds
s in X ::_thesis: ex s being Element of RAT+ st
( s in X & r < s )
proof
let s be Element of RAT+ ; ::_thesis: ( s <=' r implies s in X )
assume s <=' r ; ::_thesis: s in X
then s < one by A3, ARYTM_3:67;
hence s in X ; ::_thesis: verum
end;
consider s being Element of RAT+ such that
A4: r < s and
A5: s < one by A3, ARYTM_3:93;
take s ; ::_thesis: ( s in X & r < s )
thus s in X by A5; ::_thesis: r < s
thus r < s by A4; ::_thesis: verum
end;
then X in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
hence not DEDEKIND_CUTS is empty by A2, ZFMISC_1:56; ::_thesis: verum
end;
end;
definition
func REAL+ -> set equals :: ARYTM_2:def 2
(RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ;
coherence
(RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } is set ;
end;
:: deftheorem defines REAL+ ARYTM_2:def_2_:_
REAL+ = (RAT+ \/ DEDEKIND_CUTS) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ;
set IR = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
set RA = { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ;
Lm1: for x, y being set holds not [x,y] in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
proof
given x, y being set such that A1: [x,y] in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; ::_thesis: contradiction
consider A being Subset of RAT+ such that
A2: [x,y] = A and
A3: for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) by A1;
( {x} in A & ( for r, s being Element of RAT+ 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; ::_thesis: verum
end;
Lm2: RAT+ misses { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} }
proof
assume RAT+ meets { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; ::_thesis: contradiction
then consider e being set such that
A1: e in RAT+ and
A2: e in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by XBOOLE_0:3;
consider t being Element of RAT+ such that
A3: e = { s where s is Element of RAT+ : 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not u in e or u in RAT+ )
assume u in e ; ::_thesis: u in RAT+
then ex s being Element of RAT+ st
( s = u & s < t ) by A3;
hence u in RAT+ ; ::_thesis: verum
end;
then reconsider e = e as non empty Subset of RAT+ by A5;
consider s being Element of RAT+ such that
A6: s in e and
A7: for r being Element of RAT+ st r in e holds
r <=' s by A1, ARYTM_3:91;
ex r being Element of RAT+ st
( r = s & r < t ) by A3, A6;
then consider r being Element of RAT+ such that
A8: s < r and
A9: r < t by ARYTM_3:93;
r in e by A3, A9;
hence contradiction by A7, A8; ::_thesis: verum
end;
theorem Th1: :: ARYTM_2:1
RAT+ c= REAL+ by Lm2, XBOOLE_1:7, XBOOLE_1:86;
RAT+ \/ DEDEKIND_CUTS c= RAT+ \/ { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by XBOOLE_1:9;
then Lm3: REAL+ c= RAT+ \/ { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
by XBOOLE_1:1;
REAL+ = RAT+ \/ (( { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } \ {RAT+}) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } )
by Lm2, XBOOLE_1:87;
then Lm4: DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } c= REAL+
by XBOOLE_1:7;
Lm5: omega c= ( { [c,d] where c, d is Element of omega : ( c,d are_relative_prime & d <> {} ) } \ { [k,1] where k is Element of omega : verum } ) \/ omega
by XBOOLE_1:7;
theorem :: ARYTM_2:2
omega c= REAL+ by Lm5, Th1, XBOOLE_1:1;
registration
cluster REAL+ -> non empty ;
coherence
not REAL+ is empty by Th1;
end;
definition
let x be Element of REAL+ ;
func DEDEKIND_CUT x -> Element of DEDEKIND_CUTS means :Def3: :: ARYTM_2:def 3
ex r being Element of RAT+ st
( x = r & it = { s where s is Element of RAT+ : s < r } ) if x in RAT+
otherwise it = x;
existence
( ( x in RAT+ implies ex b1 being Element of DEDEKIND_CUTS ex r being Element of RAT+ st
( x = r & b1 = { s where s is Element of RAT+ : s < r } ) ) & ( not x in RAT+ implies ex b1 being Element of DEDEKIND_CUTS st b1 = x ) )
proof
thus ( x in RAT+ implies ex IT being Element of DEDEKIND_CUTS ex r being Element of RAT+ st
( x = r & IT = { s where s is Element of RAT+ : s < r } ) ) ::_thesis: ( not x in RAT+ implies ex b1 being Element of DEDEKIND_CUTS st b1 = x )
proof
assume x in RAT+ ; ::_thesis: ex IT being Element of DEDEKIND_CUTS ex r being Element of RAT+ st
( x = r & IT = { s where s is Element of RAT+ : s < r } )
then reconsider r = x as Element of RAT+ ;
set IT = { s where s is Element of RAT+ : s < r } ;
A1: { s where s is Element of RAT+ : s < r } c= RAT+
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { s where s is Element of RAT+ : s < r } or e in RAT+ )
assume e in { s where s is Element of RAT+ : s < r } ; ::_thesis: e in RAT+
then ex s being Element of RAT+ st
( s = e & s < r ) ;
hence e in RAT+ ; ::_thesis: verum
end;
for s being Element of RAT+ holds
( not s = r or not s < r ) ;
then not r in { s where s is Element of RAT+ : s < r } ;
then A2: { s where s is Element of RAT+ : s < r } <> RAT+ ;
reconsider IT = { s where s is Element of RAT+ : s < r } as Subset of RAT+ by A1;
for t being Element of RAT+ st t in IT holds
( ( for s being Element of RAT+ st s <=' t holds
s in IT ) & ex s being Element of RAT+ st
( s in IT & t < s ) )
proof
let t be Element of RAT+ ; ::_thesis: ( t in IT implies ( ( for s being Element of RAT+ st s <=' t holds
s in IT ) & ex s being Element of RAT+ st
( s in IT & t < s ) ) )
assume t in IT ; ::_thesis: ( ( for s being Element of RAT+ st s <=' t holds
s in IT ) & ex s being Element of RAT+ st
( s in IT & t < s ) )
then A3: ex s being Element of RAT+ 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 being Element of RAT+ st s <=' t holds
s in IT ::_thesis: ex s being Element of RAT+ st
( s in IT & t < s )
proof
let s be Element of RAT+ ; ::_thesis: ( s <=' t implies s in IT )
assume s <=' t ; ::_thesis: s in IT
then s < r by A3, ARYTM_3:69;
hence s in IT ; ::_thesis: verum
end;
take s0 ; ::_thesis: ( s0 in IT & t < s0 )
thus s0 in IT by A5; ::_thesis: t < s0
thus t < s0 by A4; ::_thesis: verum
end;
then IT in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
then reconsider IT = IT as Element of DEDEKIND_CUTS by A2, ZFMISC_1:56;
take IT ; ::_thesis: ex r being Element of RAT+ st
( x = r & IT = { s where s is Element of RAT+ : s < r } )
take r ; ::_thesis: ( x = r & IT = { s where s is Element of RAT+ : s < r } )
thus ( x = r & IT = { s where s is Element of RAT+ : s < r } ) ; ::_thesis: verum
end;
A6: x in REAL+ ;
assume not x in RAT+ ; ::_thesis: ex b1 being Element of DEDEKIND_CUTS st b1 = x
then x in DEDEKIND_CUTS by A6, XBOOLE_0:def_3;
hence ex b1 being Element of DEDEKIND_CUTS st b1 = x ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of DEDEKIND_CUTS holds
( ( x in RAT+ & ex r being Element of RAT+ st
( x = r & b1 = { s where s is Element of RAT+ : s < r } ) & ex r being Element of RAT+ st
( x = r & b2 = { s where s is Element of RAT+ : s < r } ) implies b1 = b2 ) & ( not x in RAT+ & b1 = x & b2 = x implies b1 = b2 ) ) ;
consistency
for b1 being Element of DEDEKIND_CUTS holds verum ;
end;
:: deftheorem Def3 defines DEDEKIND_CUT ARYTM_2:def_3_:_
for x being Element of REAL+
for b2 being Element of DEDEKIND_CUTS holds
( ( x in RAT+ implies ( b2 = DEDEKIND_CUT x iff ex r being Element of RAT+ st
( x = r & b2 = { s where s is Element of RAT+ : s < r } ) ) ) & ( not x in RAT+ implies ( b2 = DEDEKIND_CUT x iff b2 = x ) ) );
theorem :: ARYTM_2:3
for y being set holds not [{},y] in REAL+
proof
given y being set such that A1: [{},y] in REAL+ ; ::_thesis: contradiction
percases ( [{},y] in RAT+ or [{},y] in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ) by A1, Lm3, XBOOLE_0:def_3;
suppose [{},y] in RAT+ ; ::_thesis: contradiction
hence contradiction by ARYTM_3:61; ::_thesis: verum
end;
suppose [{},y] in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; ::_thesis: contradiction
hence contradiction by Lm1; ::_thesis: verum
end;
end;
end;
Lm6: for s, t being Element of RAT+ st ( for r being Element of RAT+ holds
( r < s iff r < t ) ) holds
s = t
proof
let s, t be Element of RAT+ ; ::_thesis: ( ( for r being Element of RAT+ holds
( r < s iff r < t ) ) implies s = t )
assume A1: for r being Element of RAT+ holds
( r < s iff r < t ) ; ::_thesis: s = t
s <=' s ;
then A2: t <=' s by A1;
t <=' t ;
then s <=' t by A1;
hence s = t by A2, ARYTM_3:66; ::_thesis: verum
end;
definition
let x be Element of DEDEKIND_CUTS ;
func GLUED x -> Element of REAL+ means :Def4: :: ARYTM_2:def 4
ex r being Element of RAT+ st
( it = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) ) if ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in x iff s < r )
otherwise it = x;
uniqueness
for b1, b2 being Element of REAL+ holds
( ( ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in x iff s < r ) & ex r being Element of RAT+ st
( b1 = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) ) & ex r being Element of RAT+ st
( b2 = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) ) implies b1 = b2 ) & ( ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ) & b1 = x & b2 = x implies b1 = b2 ) )
proof
let IT1, IT2 be Element of REAL+ ; ::_thesis: ( ( ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in x iff s < r ) & ex r being Element of RAT+ st
( IT1 = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) ) & ex r being Element of RAT+ st
( IT2 = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) ) implies IT1 = IT2 ) & ( ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ) & IT1 = x & IT2 = x implies IT1 = IT2 ) )
hereby ::_thesis: ( ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ) & IT1 = x & IT2 = x implies IT1 = IT2 )
assume ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in x iff s < r ) ; ::_thesis: ( ex r1 being Element of RAT+ st
( IT1 = r1 & ( for s being Element of RAT+ holds
( s in x iff s < r1 ) ) ) & ex r2 being Element of RAT+ st
( IT2 = r2 & ( for s being Element of RAT+ holds
( s in x iff s < r2 ) ) ) implies IT1 = IT2 )
given r1 being Element of RAT+ such that A1: IT1 = r1 and
A2: for s being Element of RAT+ holds
( s in x iff s < r1 ) ; ::_thesis: ( ex r2 being Element of RAT+ st
( IT2 = r2 & ( for s being Element of RAT+ holds
( s in x iff s < r2 ) ) ) implies IT1 = IT2 )
given r2 being Element of RAT+ such that A3: IT2 = r2 and
A4: for s being Element of RAT+ holds
( s in x iff s < r2 ) ; ::_thesis: IT1 = IT2
for s being Element of RAT+ holds
( s < r1 iff s < r2 )
proof
let s be Element of RAT+ ; ::_thesis: ( s < r1 iff s < r2 )
( s in x iff s < r1 ) by A2;
hence ( s < r1 iff s < r2 ) by A4; ::_thesis: verum
end;
hence IT1 = IT2 by A1, A3, Lm6; ::_thesis: verum
end;
thus ( ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ) & IT1 = x & IT2 = x implies IT1 = IT2 ) ; ::_thesis: verum
end;
existence
( ( ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in x iff s < r ) implies ex b1 being Element of REAL+ ex r being Element of RAT+ st
( b1 = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) ) ) & ( ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ) implies ex b1 being Element of REAL+ st b1 = x ) )
proof
hereby ::_thesis: ( ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ) implies ex b1 being Element of REAL+ st b1 = x )
given r being Element of RAT+ such that A5: for s being Element of RAT+ holds
( s in x iff s < r ) ; ::_thesis: ex y being Element of REAL+ ex r being Element of RAT+ st
( y = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) )
r in RAT+ ;
then reconsider y = r as Element of REAL+ by Th1;
take y = y; ::_thesis: ex r being Element of RAT+ st
( y = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) )
take r = r; ::_thesis: ( y = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) )
thus y = r ; ::_thesis: for s being Element of RAT+ holds
( s in x iff s < r )
thus for s being Element of RAT+ holds
( s in x iff s < r ) by A5; ::_thesis: verum
end;
assume A6: for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ; ::_thesis: ex b1 being Element of REAL+ st b1 = x
now__::_thesis:_not_x_in__{___{__s_where_s_is_Element_of_RAT+_:_s_<_t__}__where_t_is_Element_of_RAT+_:_t_<>_{}__}_
assume x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; ::_thesis: contradiction
then consider t being Element of RAT+ such that
A7: x = { s where s is Element of RAT+ : s < t } and
t <> {} ;
for s being Element of RAT+ holds
( s in x iff s < t )
proof
let s be Element of RAT+ ; ::_thesis: ( s in x iff s < t )
hereby ::_thesis: ( s < t implies s in x )
assume s in x ; ::_thesis: s < t
then ex r being Element of RAT+ st
( s = r & r < t ) by A7;
hence s < t ; ::_thesis: verum
end;
thus ( s < t implies s in x ) by A7; ::_thesis: verum
end;
hence contradiction by A6; ::_thesis: verum
end;
then x in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by XBOOLE_0:def_5;
then reconsider y = x as Element of REAL+ by Lm4;
take y ; ::_thesis: y = x
thus y = x ; ::_thesis: verum
end;
consistency
for b1 being Element of REAL+ holds verum ;
end;
:: deftheorem Def4 defines GLUED ARYTM_2:def_4_:_
for x being Element of DEDEKIND_CUTS
for b2 being Element of REAL+ holds
( ( ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in x iff s < r ) implies ( b2 = GLUED x iff ex r being Element of RAT+ st
( b2 = r & ( for s being Element of RAT+ holds
( s in x iff s < r ) ) ) ) ) & ( ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in x iff s < r ) ) implies ( b2 = GLUED x iff b2 = x ) ) );
Lm7: for r being Element of RAT+
for B being set st B in DEDEKIND_CUTS & r in B holds
ex s being Element of RAT+ st
( s in B & r < s )
proof
let r be Element of RAT+ ; ::_thesis: for B being set st B in DEDEKIND_CUTS & r in B holds
ex s being Element of RAT+ st
( s in B & r < s )
let B be set ; ::_thesis: ( B in DEDEKIND_CUTS & r in B implies ex s being Element of RAT+ st
( s in B & r < s ) )
assume B in DEDEKIND_CUTS ; ::_thesis: ( not r in B or ex s being Element of RAT+ st
( s in B & r < s ) )
then B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
then ex A being Subset of RAT+ st
( B = A & ( for t being Element of RAT+ st t in A holds
( ( for s being Element of RAT+ st s <=' t holds
s in A ) & ex s being Element of RAT+ st
( s in A & t < s ) ) ) ) ;
hence ( not r in B or ex s being Element of RAT+ st
( s in B & r < s ) ) ; ::_thesis: verum
end;
Lm8: {} in DEDEKIND_CUTS
proof
reconsider B = {} as Subset of RAT+ by XBOOLE_1:2;
for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) ) ;
then {} in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
hence {} in DEDEKIND_CUTS by ZFMISC_1:56; ::_thesis: verum
end;
Lm9: DEDEKIND_CUTS /\ RAT+ = {{}}
proof
now__::_thesis:_for_e_being_set_holds_
(_(_e_in_DEDEKIND_CUTS_/\_RAT+_implies_e_=_{}_)_&_(_e_=_{}_implies_e_in_DEDEKIND_CUTS_/\_RAT+_)_)
let e be set ; ::_thesis: ( ( e in DEDEKIND_CUTS /\ RAT+ implies e = {} ) & ( e = {} implies e in DEDEKIND_CUTS /\ RAT+ ) )
thus ( e in DEDEKIND_CUTS /\ RAT+ implies e = {} ) ::_thesis: ( e = {} implies e in DEDEKIND_CUTS /\ RAT+ )
proof
assume that
A1: e in DEDEKIND_CUTS /\ RAT+ and
A2: e <> {} ; ::_thesis: contradiction
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 being Element of RAT+ st
( s in A & ( for r being Element of RAT+ 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; ::_thesis: verum
end;
thus ( e = {} implies e in DEDEKIND_CUTS /\ RAT+ ) by Lm8, XBOOLE_0:def_4; ::_thesis: verum
end;
hence DEDEKIND_CUTS /\ RAT+ = {{}} by TARSKI:def_1; ::_thesis: verum
end;
Lm10: for x being Element of REAL+ holds
( DEDEKIND_CUT x = {} iff x = {} )
proof
let x be Element of REAL+ ; ::_thesis: ( DEDEKIND_CUT x = {} iff x = {} )
A1: for e being set holds not e in { s where s is Element of RAT+ : s < {} }
proof
given e being set such that A2: e in { s where s is Element of RAT+ : s < {} } ; ::_thesis: contradiction
ex s being Element of RAT+ st
( s = e & s < {} ) by A2;
hence contradiction by ARYTM_3:64; ::_thesis: verum
end;
thus ( DEDEKIND_CUT x = {} implies x = {} ) ::_thesis: ( x = {} implies DEDEKIND_CUT x = {} )
proof
assume A3: DEDEKIND_CUT x = {} ; ::_thesis: x = {}
percases ( x in RAT+ or not x in RAT+ ) ;
supposeA4: x in RAT+ ; ::_thesis: x = {}
assume A5: x <> {} ; ::_thesis: contradiction
consider r being Element of RAT+ such that
A6: x = r and
A7: DEDEKIND_CUT x = { s where s is Element of RAT+ : 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; ::_thesis: verum
end;
suppose not x in RAT+ ; ::_thesis: x = {}
hence x = {} by A3, Def3; ::_thesis: verum
end;
end;
end;
assume x = {} ; ::_thesis: DEDEKIND_CUT x = {}
then ex r being Element of RAT+ st
( {} = r & DEDEKIND_CUT x = { s where s is Element of RAT+ : s < r } ) by Def3;
hence DEDEKIND_CUT x = {} by A1, XBOOLE_0:def_1; ::_thesis: verum
end;
Lm11: for A being Element of DEDEKIND_CUTS holds
( GLUED A = {} iff A = {} )
proof
let A be Element of DEDEKIND_CUTS ; ::_thesis: ( GLUED A = {} iff A = {} )
thus ( GLUED A = {} implies A = {} ) ::_thesis: ( A = {} implies GLUED A = {} )
proof
assume A1: GLUED A = {} ; ::_thesis: A = {}
percases ( ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in A iff s < r ) or for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in A iff s < r ) ) ;
supposeA2: ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in A iff s < r ) ; ::_thesis: A = {}
assume A <> {} ; ::_thesis: contradiction
then consider r being Element of RAT+ such that
A3: r in A by SUBSET_1:4;
ex r being Element of RAT+ st
( GLUED A = r & ( for s being Element of RAT+ holds
( s in A iff s < r ) ) ) by A2, Def4;
then r < {} by A1, A3;
hence contradiction by ARYTM_3:64; ::_thesis: verum
end;
suppose for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in A iff s < r ) ; ::_thesis: A = {}
hence A = {} by A1, Def4; ::_thesis: verum
end;
end;
end;
assume A4: A = {} ; ::_thesis: GLUED A = {}
then for s being Element of RAT+ holds
( s in A iff s < {} ) by ARYTM_3:64;
then consider r being Element of RAT+ such that
A5: GLUED A = r and
A6: for s being Element of RAT+ holds
( s in A iff s < r ) by Def4;
assume A7: GLUED A <> {} ; ::_thesis: contradiction
{} <=' r by ARYTM_3:64;
then {} < r by A5, A7, ARYTM_3:68;
hence contradiction by A4, A6; ::_thesis: verum
end;
Lm12: for A being Element of DEDEKIND_CUTS holds DEDEKIND_CUT (GLUED A) = A
proof
let A be Element of DEDEKIND_CUTS ; ::_thesis: DEDEKIND_CUT (GLUED A) = A
percases ( ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in A iff s < r ) or A = {} or ( A <> {} & ( for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in A iff s < r ) ) ) ) ;
suppose ex r being Element of RAT+ st
for s being Element of RAT+ holds
( s in A iff s < r ) ; ::_thesis: DEDEKIND_CUT (GLUED A) = A
then consider r being Element of RAT+ such that
A1: r = GLUED A and
A2: for s being Element of RAT+ holds
( s in A iff s < r ) by Def4;
consider s being Element of RAT+ such that
A3: r = s and
A4: DEDEKIND_CUT (GLUED A) = { t where t is Element of RAT+ : t < s } by A1, Def3;
thus DEDEKIND_CUT (GLUED A) c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= DEDEKIND_CUT (GLUED A)
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in DEDEKIND_CUT (GLUED A) or e in A )
assume e in DEDEKIND_CUT (GLUED A) ; ::_thesis: e in A
then ex t being Element of RAT+ st
( t = e & t < s ) by A4;
hence e in A by A2, A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in DEDEKIND_CUT (GLUED A) )
assume A5: e in A ; ::_thesis: e in DEDEKIND_CUT (GLUED A)
then reconsider s = e as Element of RAT+ ;
s < r by A2, A5;
hence e in DEDEKIND_CUT (GLUED A) by A3, A4; ::_thesis: verum
end;
supposeA6: A = {} ; ::_thesis: DEDEKIND_CUT (GLUED A) = A
then GLUED A = {} by Lm11;
hence DEDEKIND_CUT (GLUED A) = A by A6, Lm10; ::_thesis: verum
end;
supposethat A7: A <> {} and
A8: for r being Element of RAT+ holds
not for s being Element of RAT+ holds
( s in A iff s < r ) ; ::_thesis: DEDEKIND_CUT (GLUED A) = A
A9: GLUED A = A by A8, Def4;
now__::_thesis:_not_GLUED_A_in_RAT+
assume GLUED A in RAT+ ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence DEDEKIND_CUT (GLUED A) = A by A9, Def3; ::_thesis: verum
end;
end;
end;
Lm13: for x, y being set st x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & not x c= y holds
y c= x
proof
let x, y be set ; ::_thesis: ( x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & not x c= y implies y c= x )
assume x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; ::_thesis: ( not y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } or x c= y or y c= x )
then A1: ex A9 being Subset of RAT+ st
( x = A9 & ( for r being Element of RAT+ st r in A9 holds
( ( for s being Element of RAT+ st s <=' r holds
s in A9 ) & ex s being Element of RAT+ st
( s in A9 & r < s ) ) ) ) ;
assume y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; ::_thesis: ( x c= y or y c= x )
then A2: ex B9 being Subset of RAT+ st
( y = B9 & ( for r being Element of RAT+ st r in B9 holds
( ( for s being Element of RAT+ st s <=' r holds
s in B9 ) & ex s being Element of RAT+ st
( s in B9 & r < s ) ) ) ) ;
assume not x c= y ; ::_thesis: y c= x
then consider s being set such that
A3: s in x and
A4: not s in y by TARSKI:def_3;
reconsider s = s as Element of RAT+ by A1, A3;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in y or e in x )
assume A5: e in y ; ::_thesis: e in x
then reconsider r = e as Element of RAT+ by A2;
r <=' s by A2, A4, A5;
hence e in x by A1, A3; ::_thesis: verum
end;
definition
let x, y be Element of REAL+ ;
predx <=' y means :Def5: :: ARYTM_2:def 5
ex x9, y9 being Element of RAT+ 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
( ( x in RAT+ & y in RAT+ & x in RAT+ & not y in RAT+ implies ( ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x9 <=' y9 ) iff x in y ) ) & ( x in RAT+ & y in RAT+ & not x in RAT+ & y in RAT+ implies ( ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x9 <=' y9 ) iff not y in x ) ) & ( x in RAT+ & not y in RAT+ & not x in RAT+ & y in RAT+ implies ( x in y iff not y in x ) ) ) ;
connectedness
for x, y being Element of REAL+ st ( ( x in RAT+ & y in RAT+ & ( for x9, y9 being Element of RAT+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in RAT+ & not y in RAT+ & not x in y ) or ( not x in RAT+ & y in RAT+ & y in x ) or ( ( not x in RAT+ or not y in RAT+ ) & ( not x in RAT+ or y in RAT+ ) & ( x in RAT+ or not y in RAT+ ) & not x c= y ) ) holds
( ( y in RAT+ & x in RAT+ implies ex x9, y9 being Element of RAT+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) )
proof
let x, y be Element of REAL+ ; ::_thesis: ( ( ( x in RAT+ & y in RAT+ & ( for x9, y9 being Element of RAT+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in RAT+ & not y in RAT+ & not x in y ) or ( not x in RAT+ & y in RAT+ & y in x ) or ( ( not x in RAT+ or not y in RAT+ ) & ( not x in RAT+ or y in RAT+ ) & ( x in RAT+ or not y in RAT+ ) & not x c= y ) ) implies ( ( y in RAT+ & x in RAT+ implies ex x9, y9 being Element of RAT+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) ) )
assume A1: ( ( x in RAT+ & y in RAT+ & ( for x9, y9 being Element of RAT+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in RAT+ & not y in RAT+ & not x in y ) or ( not x in RAT+ & y in RAT+ & y in x ) or ( not ( x in RAT+ & y in RAT+ ) & not ( x in RAT+ & not y in RAT+ ) & not ( not x in RAT+ & y in RAT+ ) & not x c= y ) ) ; ::_thesis: ( ( y in RAT+ & x in RAT+ implies ex x9, y9 being Element of RAT+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) )
thus ( y in RAT+ & x in RAT+ implies ex y9, x9 being Element of RAT+ st
( y = y9 & x = x9 & y9 <=' x9 ) ) ::_thesis: ( ( y in RAT+ & not x in RAT+ implies y in x ) & ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) )
proof
assume ( y in RAT+ & x in RAT+ ) ; ::_thesis: ex y9, x9 being Element of RAT+ st
( y = y9 & x = x9 & y9 <=' x9 )
then reconsider y9 = y, x9 = x as Element of RAT+ ;
y9 <=' x9 by A1;
hence ex y9, x9 being Element of RAT+ st
( y = y9 & x = x9 & y9 <=' x9 ) ; ::_thesis: verum
end;
thus ( y in RAT+ & not x in RAT+ implies y in x ) by A1; ::_thesis: ( ( not y in RAT+ & x in RAT+ implies not x in y ) & ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x ) )
thus ( not y in RAT+ & x in RAT+ implies not x in y ) by A1; ::_thesis: ( ( not y in RAT+ or not x in RAT+ ) & ( not y in RAT+ or x in RAT+ ) & ( y in RAT+ or not x in RAT+ ) implies y c= x )
assume A2: ( not ( y in RAT+ & x in RAT+ ) & not ( y in RAT+ & not x in RAT+ ) & not ( not y in RAT+ & x in RAT+ ) ) ; ::_thesis: y c= x
y in REAL+ ;
then A3: y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A2, Lm3, XBOOLE_0:def_3;
x in REAL+ ;
then x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A2, Lm3, XBOOLE_0:def_3;
hence y c= x by A1, A2, A3, Lm13; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines <=' ARYTM_2:def_5_:_
for x, y being Element of REAL+ holds
( ( x in RAT+ & y in RAT+ implies ( x <=' y iff ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x9 <=' y9 ) ) ) & ( x in RAT+ & not y in RAT+ implies ( x <=' y iff x in y ) ) & ( not x in RAT+ & y in RAT+ implies ( x <=' y iff not y in x ) ) & ( ( not x in RAT+ or not y in RAT+ ) & ( not x in RAT+ or y in RAT+ ) & ( x in RAT+ or not y in RAT+ ) implies ( x <=' y iff x c= y ) ) );
notation
let x, y be Element of REAL+ ;
antonym y < x for x <=' y;
end;
Lm14: for x9, y9 being Element of RAT+
for x, y being Element of REAL+ st x = x9 & y = y9 holds
( x <=' y iff x9 <=' y9 )
proof
let x9, y9 be Element of RAT+ ; ::_thesis: for x, y being Element of REAL+ st x = x9 & y = y9 holds
( x <=' y iff x9 <=' y9 )
let x, y be Element of REAL+ ; ::_thesis: ( x = x9 & y = y9 implies ( x <=' y iff x9 <=' y9 ) )
assume A1: ( x = x9 & y = y9 ) ; ::_thesis: ( x <=' y iff x9 <=' y9 )
hereby ::_thesis: ( x9 <=' y9 implies x <=' y )
assume x <=' y ; ::_thesis: x9 <=' y9
then ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x9 <=' y9 ) by A1, Def5;
hence x9 <=' y9 by A1; ::_thesis: verum
end;
thus ( x9 <=' y9 implies x <=' y ) by A1, Def5; ::_thesis: verum
end;
Lm15: for B being set st B in DEDEKIND_CUTS & B <> {} holds
ex r being Element of RAT+ st
( r in B & r <> {} )
proof
let B be set ; ::_thesis: ( B in DEDEKIND_CUTS & B <> {} implies ex r being Element of RAT+ st
( r in B & r <> {} ) )
assume that
A1: B in DEDEKIND_CUTS and
A2: B <> {} ; ::_thesis: ex r being Element of RAT+ st
( r in B & r <> {} )
B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A1;
then consider A being Subset of RAT+ such that
A3: B = A and
A4: for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) ;
reconsider A = 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 being Element of RAT+ 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 ex r being Element of RAT+ st
( r in B & r <> {} ) by A3, A9; ::_thesis: verum
end;
Lm16: for r, s being Element of RAT+
for B being set st B in DEDEKIND_CUTS & r in B & s <=' r holds
s in B
proof
let r, s be Element of RAT+ ; ::_thesis: for B being set st B in DEDEKIND_CUTS & r in B & s <=' r holds
s in B
let B be set ; ::_thesis: ( B in DEDEKIND_CUTS & r in B & s <=' r implies s in B )
assume that
A1: B in DEDEKIND_CUTS and
A2: ( r in B & s <=' r ) ; ::_thesis: s in B
B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A1;
then ex A being Subset of RAT+ st
( B = A & ( for t being Element of RAT+ st t in A holds
( ( for s being Element of RAT+ st s <=' t holds
s in A ) & ex s being Element of RAT+ st
( s in A & t < s ) ) ) ) ;
hence s in B by A2; ::_thesis: verum
end;
Lm17: for B being set st B in DEDEKIND_CUTS & B <> {} holds
{} in B
proof
let B be set ; ::_thesis: ( B in DEDEKIND_CUTS & B <> {} implies {} in B )
assume that
A1: B in DEDEKIND_CUTS and
A2: B <> {} ; ::_thesis: {} in B
reconsider B = B as non empty Subset of RAT+ by A1, A2;
ex r being Element of RAT+ st r in B by SUBSET_1:4;
hence {} in B by A1, Lm16, ARYTM_3:64; ::_thesis: verum
end;
Lm18: for r being Element of RAT+
for B being set st B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } & not r in B & B <> {} holds
ex s being Element of RAT+ st
( not s in B & s < r )
proof
let r be Element of RAT+ ; ::_thesis: for B being set st B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } & not r in B & B <> {} holds
ex s being Element of RAT+ st
( not s in B & s < r )
let B be set ; ::_thesis: ( B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } & not r in B & B <> {} implies ex s being Element of RAT+ st
( not s in B & s < r ) )
assume that
A1: B in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } and
A2: not r in B and
A3: B <> {} ; ::_thesis: ex s being Element of RAT+ st
( not s in B & s < r )
A4: B in DEDEKIND_CUTS by A1, XBOOLE_0:def_5;
assume A5: for s being Element of RAT+ st not s in B holds
not s < r ; ::_thesis: contradiction
A6: B = { s where s is Element of RAT+ : s < r }
proof
thus B c= { s where s is Element of RAT+ : s < r } :: according to XBOOLE_0:def_10 ::_thesis: { s where s is Element of RAT+ : s < r } c= B
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in B or e in { s where s is Element of RAT+ : s < r } )
assume A7: e in B ; ::_thesis: e in { s where s is Element of RAT+ : s < r }
reconsider B = 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 e in { s where s is Element of RAT+ : s < r } ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { s where s is Element of RAT+ : s < r } or e in B )
assume e in { s where s is Element of RAT+ : s < r } ; ::_thesis: e in B
then ex s being Element of RAT+ st
( s = e & s < r ) ;
hence e in B by A5; ::_thesis: verum
end;
r <> {} by A2, A3, A4, Lm17;
then B in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A6;
hence contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
Lm19: for x being Element of REAL+ st DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } holds
x in RAT+
proof
let x be Element of REAL+ ; ::_thesis: ( DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } implies x in RAT+ )
assume A1: DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; ::_thesis: x in RAT+
assume not x in RAT+ ; ::_thesis: contradiction
then DEDEKIND_CUT x = x by Def3;
hence contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
Lm20: for x, y being Element of REAL+ st DEDEKIND_CUT x c= DEDEKIND_CUT y holds
x <=' y
proof
let x, y be Element of REAL+ ; ::_thesis: ( DEDEKIND_CUT x c= DEDEKIND_CUT y implies x <=' y )
assume A1: DEDEKIND_CUT x c= DEDEKIND_CUT y ; ::_thesis: x <=' y
percases ( ( x = {} & not y in RAT+ ) or y = {} or ( x in RAT+ & y in RAT+ ) or ( x in RAT+ & not y in RAT+ & x <> {} ) or ( not x in RAT+ & y in RAT+ & y <> {} ) or ( not x in RAT+ & not y in RAT+ ) ) ;
supposethat A2: x = {} and
A3: not y in RAT+ ; ::_thesis: x <=' y
( DEDEKIND_CUT y = y & y <> {} ) by A3, Def3;
then x in y by A2, Lm17;
hence x <=' y by A2, A3, Def5; ::_thesis: verum
end;
supposeA4: y = {} ; ::_thesis: x <=' y
then DEDEKIND_CUT y = {} by Lm10;
then DEDEKIND_CUT x = {} by A1;
then x = {} by Lm10;
hence x <=' y by A4; ::_thesis: verum
end;
supposethat A5: x in RAT+ and
A6: y in RAT+ ; ::_thesis: x <=' y
consider ry being Element of RAT+ such that
A7: y = ry and
A8: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < ry } by A6, Def3;
consider rx being Element of RAT+ such that
A9: x = rx and
A10: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < rx } by A5, Def3;
assume y < x ; ::_thesis: contradiction
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 being Element of RAT+ st
( s = ry & s < ry ) by A8;
hence contradiction ; ::_thesis: verum
end;
supposethat A11: x in RAT+ and
A12: not y in RAT+ and
A13: x <> {} ; ::_thesis: x <=' y
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 where s is Element of RAT+ : s < rx } by A11, Def3;
DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } 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, XBOOLE_0:def_10;
then consider r0 being Element of RAT+ such that
A17: r0 in y and
A18: not r0 in DEDEKIND_CUT x by A14, SUBSET_1:2;
rx <=' r0 by A16, A18;
then x in y by A15, A14, A17, Lm16;
hence x <=' y by A11, A12, Def5; ::_thesis: verum
end;
supposethat A19: not x in RAT+ and
A20: y in RAT+ and
A21: y <> {} ; ::_thesis: x <=' y
consider ry being Element of RAT+ such that
A22: y = ry and
A23: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < ry } by A20, Def3;
A24: DEDEKIND_CUT y in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A21, A22, A23;
A25: DEDEKIND_CUT x = x by A19, Def3;
then not x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } 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, SUBSET_1:2;
ex s being Element of RAT+ st
( s = r0 & s < ry ) by A23, A26;
then not y in x by A22, A25, A27, Lm16;
hence x <=' y by A19, A20, Def5; ::_thesis: verum
end;
supposeA28: ( not x in RAT+ & not y in RAT+ ) ; ::_thesis: x <=' y
( x = DEDEKIND_CUT x & y = DEDEKIND_CUT y ) by A28, Def3;
hence x <=' y by A1, A28, Def5; ::_thesis: verum
end;
end;
end;
Lm21: for x, y being Element of REAL+ st x <=' y & y <=' x holds
x = y
proof
let x, y be Element of REAL+ ; ::_thesis: ( x <=' y & y <=' x implies x = y )
assume that
A1: x <=' y and
A2: y <=' x ; ::_thesis: x = y
percases ( ( x in RAT+ & y in RAT+ ) or ( x in RAT+ & not y in RAT+ ) or ( not x in RAT+ & y in RAT+ ) or ( not x in RAT+ & not y in RAT+ ) ) ;
suppose ( x in RAT+ & y in RAT+ ) ; ::_thesis: x = y
then reconsider x9 = x, y9 = y as Element of RAT+ ;
( x9 <=' y9 & y9 <=' x9 ) by A1, A2, Lm14;
hence x = y by ARYTM_3:66; ::_thesis: verum
end;
supposeA3: ( x in RAT+ & not y in RAT+ ) ; ::_thesis: x = y
x in y by A1, A3, Def5;
hence x = y by A2, A3, Def5; ::_thesis: verum
end;
supposeA4: ( not x in RAT+ & y in RAT+ ) ; ::_thesis: x = y
y in x by A2, A4, Def5;
hence x = y by A1, A4, Def5; ::_thesis: verum
end;
suppose ( not x in RAT+ & not y in RAT+ ) ; ::_thesis: x = y
then ( x c= y & y c= x ) by A1, A2, Def5;
hence x = y by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
end;
Lm22: for x, y being Element of REAL+ st DEDEKIND_CUT x = DEDEKIND_CUT y holds
x = y
proof
let x, y be Element of REAL+ ; ::_thesis: ( DEDEKIND_CUT x = DEDEKIND_CUT y implies x = y )
assume DEDEKIND_CUT x = DEDEKIND_CUT y ; ::_thesis: x = y
then ( x <=' y & y <=' x ) by Lm20;
hence x = y by Lm21; ::_thesis: verum
end;
Lm23: for x being Element of REAL+ holds GLUED (DEDEKIND_CUT x) = x
proof
let x be Element of REAL+ ; ::_thesis: GLUED (DEDEKIND_CUT x) = x
DEDEKIND_CUT (GLUED (DEDEKIND_CUT x)) = DEDEKIND_CUT x by Lm12;
hence GLUED (DEDEKIND_CUT x) = x by Lm22; ::_thesis: verum
end;
definition
let A, B be Element of DEDEKIND_CUTS ;
funcA + B -> Element of DEDEKIND_CUTS equals :Def6: :: ARYTM_2:def 6
{ (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;
coherence
{ (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS
proof
{ (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } in DEDEKIND_CUTS
proof
set C = { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } ;
{ (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } c= RAT+
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } or e in RAT+ )
assume e in { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } ; ::_thesis: e in RAT+
then ex s, t being Element of RAT+ st
( e = s + t & s in A & t in B ) ;
hence e in RAT+ ; ::_thesis: verum
end;
then reconsider C = { (s + t) where s, t is Element of RAT+ : ( s in A & t in B ) } 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;
for r being Element of RAT+ st r in C holds
( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) )
proof
let r be Element of RAT+ ; ::_thesis: ( r in C implies ( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) ) )
assume r in C ; ::_thesis: ( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) )
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 being Element of RAT+ st s <=' r holds
s in C ::_thesis: ex s being Element of RAT+ st
( s in C & r < s )
proof
let s be Element of RAT+ ; ::_thesis: ( s <=' r implies s in C )
assume s <=' r ; ::_thesis: s in C
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 s in C by A5; ::_thesis: verum
end;
consider s1 being Element of RAT+ such that
A7: s1 in A and
A8: s0 < s1 by A3, Lm7;
take t2 = s1 + t0; ::_thesis: ( t2 in C & r < t2 )
thus t2 in C by A4, A7; ::_thesis: r < t2
thus r < t2 by A2, A8, ARYTM_3:76; ::_thesis: verum
end;
then A9: C in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
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__::_thesis:_not_a0_+_b0_in_C
assume a0 + b0 in C ; ::_thesis: contradiction
then consider s, t being Element of RAT+ 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; ::_thesis: verum
end;
then C <> RAT+ ;
hence { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } in DEDEKIND_CUTS by A9, ZFMISC_1:56; ::_thesis: verum
end;
hence { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS ; ::_thesis: verum
end;
commutativity
for b1, A, B being Element of DEDEKIND_CUTS st b1 = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } holds
b1 = { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) }
proof
let IT, A, B be Element of DEDEKIND_CUTS ; ::_thesis: ( IT = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } implies IT = { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } )
set C = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;
set D = { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ;
A13: { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } c= { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } or e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } )
assume e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ; ::_thesis: e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) }
then ex r, s being Element of RAT+ st
( e = r + s & r in B & s in A ) ;
hence e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; ::_thesis: verum
end;
{ (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } c= { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } or e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } )
assume e in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; ::_thesis: e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) }
then ex r, s being Element of RAT+ st
( e = r + s & r in A & s in B ) ;
hence e in { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ; ::_thesis: verum
end;
hence ( IT = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } implies IT = { (r + s) where r, s is Element of RAT+ : ( r in B & s in A ) } ) by A13, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines + ARYTM_2:def_6_:_
for A, B being Element of DEDEKIND_CUTS holds A + B = { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;
Lm24: for B being set st B in DEDEKIND_CUTS holds
ex r being Element of RAT+ st not r in B
proof
let B be set ; ::_thesis: ( B in DEDEKIND_CUTS implies ex r being Element of RAT+ st not r in B )
assume A1: B in DEDEKIND_CUTS ; ::_thesis: not for r being Element of RAT+ holds r in B
then reconsider B = B as Subset of RAT+ ;
B <> RAT+ by A1, ZFMISC_1:56;
hence not for r being Element of RAT+ holds r in B by SUBSET_1:28; ::_thesis: verum
end;
definition
let A, B be Element of DEDEKIND_CUTS ;
funcA *' B -> Element of DEDEKIND_CUTS equals :: ARYTM_2:def 7
{ (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;
coherence
{ (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS
proof
percases ( A = {} or A <> {} ) ;
supposeA1: A = {} ; ::_thesis: { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS
for e being set holds not e in { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) }
proof
given e being set such that A2: e in { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; ::_thesis: contradiction
ex r, s being Element of RAT+ st
( e = r *' s & r in A & s in B ) by A2;
hence contradiction by A1; ::_thesis: verum
end;
hence { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS by Lm8, XBOOLE_0:def_1; ::_thesis: verum
end;
supposeA3: A <> {} ; ::_thesis: { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS
set C = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;
{ (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } c= RAT+
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } or e in RAT+ )
assume e in { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; ::_thesis: e in RAT+
then ex r, s being Element of RAT+ st
( r *' s = e & r in A & s in B ) ;
hence e in RAT+ ; ::_thesis: verum
end;
then reconsider C = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } as Subset of RAT+ ;
for r being Element of RAT+ st r in C holds
( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) )
proof
let r be Element of RAT+ ; ::_thesis: ( r in C implies ( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) ) )
assume r in C ; ::_thesis: ( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) )
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 being Element of RAT+ st s <=' r holds
s in C ::_thesis: ex s being Element of RAT+ st
( s in C & r < s )
proof
let s be Element of RAT+ ; ::_thesis: ( s <=' r implies s in C )
assume s <=' r ; ::_thesis: s in C
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 s in C by A5, A7; ::_thesis: verum
end;
consider t0 being Element of RAT+ such that
A9: t0 in B and
A10: s0 < t0 by A6, Lm7;
percases ( r0 = {} or r0 <> {} ) ;
supposeA11: r0 = {} ; ::_thesis: ex s being Element of RAT+ st
( s in C & r < s )
consider r1 being Element of RAT+ such that
A12: r1 in A and
A13: r1 <> {} by A3, Lm15;
take r1 *' t0 ; ::_thesis: ( r1 *' t0 in C & r < r1 *' t0 )
thus r1 *' t0 in C by A9, A12; ::_thesis: r < r1 *' t0
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 r < r1 *' t0 by A15, A14, ARYTM_3:68; ::_thesis: verum
end;
supposeA16: r0 <> {} ; ::_thesis: ex s being Element of RAT+ st
( s in C & r < s )
s0 <> t0 by A10;
then A17: r <> r0 *' t0 by A4, A16, ARYTM_3:56;
take r0 *' t0 ; ::_thesis: ( r0 *' t0 in C & r < r0 *' t0 )
thus r0 *' t0 in C by A5, A9; ::_thesis: r < r0 *' t0
r <=' r0 *' t0 by A4, A10, ARYTM_3:82;
hence r < r0 *' t0 by A17, ARYTM_3:68; ::_thesis: verum
end;
end;
end;
then A18: C in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
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__::_thesis:_not_r0_*'_s0_in_C
assume r0 *' s0 in C ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then C <> RAT+ ;
hence { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } is Element of DEDEKIND_CUTS by A18, ZFMISC_1:56; ::_thesis: verum
end;
end;
end;
commutativity
for b1, A, B being Element of DEDEKIND_CUTS st b1 = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } holds
b1 = { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) }
proof
let D, A, B be Element of DEDEKIND_CUTS ; ::_thesis: ( D = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } implies D = { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } )
assume A23: D = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ; ::_thesis: D = { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) }
now__::_thesis:_for_e_being_set_holds_
(_e_in_D_iff_e_in__{__(r_*'_s)_where_r,_s_is_Element_of_RAT+_:_(_r_in_B_&_s_in_A_)__}__)
let e be set ; ::_thesis: ( e in D iff e in { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } )
( e in D iff ex r, s being Element of RAT+ st
( e = r *' s & r in A & s in B ) ) by A23;
then ( e in D iff ex r, s being Element of RAT+ st
( e = r *' s & r in B & s in A ) ) ;
hence ( e in D iff e in { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } ) ; ::_thesis: verum
end;
hence D = { (r *' s) where r, s is Element of RAT+ : ( r in B & s in A ) } by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem defines *' ARYTM_2:def_7_:_
for A, B being Element of DEDEKIND_CUTS holds A *' B = { (r *' s) where r, s is Element of RAT+ : ( r in A & s in B ) } ;
definition
let x, y be Element of REAL+ ;
funcx + y -> Element of REAL+ equals :Def8: :: ARYTM_2:def 8
x if y = {}
y if x = {}
otherwise GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y));
coherence
( ( y = {} implies x is Element of REAL+ ) & ( x = {} implies y is Element of REAL+ ) & ( not y = {} & not x = {} implies GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) is Element of REAL+ ) ) ;
consistency
for b1 being Element of REAL+ st y = {} & x = {} holds
( b1 = x iff b1 = y ) ;
commutativity
for b1, x, y being Element of REAL+ st ( y = {} implies b1 = x ) & ( x = {} implies b1 = y ) & ( not y = {} & not x = {} implies b1 = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) ) holds
( ( x = {} implies b1 = y ) & ( y = {} implies b1 = x ) & ( not x = {} & not y = {} implies b1 = GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT x)) ) ) ;
funcx *' y -> Element of REAL+ equals :: ARYTM_2:def 9
GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y));
coherence
GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) is Element of REAL+ ;
commutativity
for b1, x, y being Element of REAL+ st b1 = GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) holds
b1 = GLUED ((DEDEKIND_CUT y) *' (DEDEKIND_CUT x)) ;
end;
:: deftheorem Def8 defines + ARYTM_2:def_8_:_
for x, y being Element of REAL+ holds
( ( y = {} implies x + y = x ) & ( x = {} implies x + y = y ) & ( not y = {} & not x = {} implies x + y = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) ) );
:: deftheorem defines *' ARYTM_2:def_9_:_
for x, y being Element of REAL+ holds x *' y = GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y));
theorem Th4: :: ARYTM_2:4
for x, y being Element of REAL+ st x = {} holds
x *' y = {}
proof
let x, y be Element of REAL+ ; ::_thesis: ( x = {} implies x *' y = {} )
set A = DEDEKIND_CUT x;
set B = DEDEKIND_CUT y;
assume A1: x = {} ; ::_thesis: x *' y = {}
for e being set holds not e in { (r *' s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) }
proof
given e being set such that A2: e in { (r *' s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) } ; ::_thesis: contradiction
ex r, s being Element of RAT+ st
( e = r *' s & r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) by A2;
hence contradiction by A1, Lm10; ::_thesis: verum
end;
then { (r *' s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) } = {} by XBOOLE_0:def_1;
hence x *' y = {} by Lm11; ::_thesis: verum
end;
theorem Th5: :: ARYTM_2:5
for x, y being Element of REAL+ st x + y = {} holds
x = {}
proof
let x, y be Element of REAL+ ; ::_thesis: ( x + y = {} implies x = {} )
assume A1: x + y = {} ; ::_thesis: x = {}
percases ( y = {} or y <> {} ) ;
suppose y = {} ; ::_thesis: x = {}
hence x = {} by A1, Def8; ::_thesis: verum
end;
supposeA2: y <> {} ; ::_thesis: x = {}
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 <> {} ; ::_thesis: contradiction
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) where r, s is Element of RAT+ : ( 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; ::_thesis: verum
end;
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 ; ::_thesis: A + (B + C) c= (A + B) + C
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A + (B + C) or e in (A + B) + C )
assume e in A + (B + C) ; ::_thesis: 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 e in (A + B) + C by A4; ::_thesis: verum
end;
Lm26: for A, B, C being Element of DEDEKIND_CUTS holds A + (B + C) = (A + B) + C
proof
let A, B, C be Element of DEDEKIND_CUTS ; ::_thesis: A + (B + C) = (A + B) + C
( A + (B + C) c= (A + B) + C & (A + B) + C c= A + (B + C) ) by Lm25;
hence A + (B + C) = (A + B) + C by XBOOLE_0:def_10; ::_thesis: verum
end;
Lm27: for A, B being Element of DEDEKIND_CUTS holds
( not A + B = {} or A = {} or B = {} )
proof
let A, B be Element of DEDEKIND_CUTS ; ::_thesis: ( not A + B = {} or A = {} or B = {} )
assume A1: A + B = {} ; ::_thesis: ( A = {} or B = {} )
assume A <> {} ; ::_thesis: B = {}
then consider r0 being Element of RAT+ such that
A2: r0 in A by SUBSET_1:4;
assume B <> {} ; ::_thesis: contradiction
then consider s0 being Element of RAT+ such that
A3: s0 in B by SUBSET_1:4;
r0 + s0 in { (r + s) where r, s is Element of RAT+ : ( r in A & s in B ) } by A2, A3;
hence contradiction by A1; ::_thesis: verum
end;
theorem Th6: :: ARYTM_2:6
for x, y, z being Element of REAL+ holds x + (y + z) = (x + y) + z
proof
let x, y, z be Element of REAL+ ; ::_thesis: x + (y + z) = (x + y) + z
percases ( x = {} or y = {} or z = {} or ( x <> {} & y <> {} & z <> {} ) ) ;
supposeA1: x = {} ; ::_thesis: x + (y + z) = (x + y) + z
hence x + (y + z) = y + z by Def8
.= (x + y) + z by A1, Def8 ;
::_thesis: verum
end;
supposeA2: y = {} ; ::_thesis: x + (y + z) = (x + y) + z
hence x + (y + z) = x + z by Def8
.= (x + y) + z by A2, Def8 ;
::_thesis: verum
end;
supposeA3: z = {} ; ::_thesis: x + (y + z) = (x + y) + z
hence x + (y + z) = x + y by Def8
.= (x + y) + z by A3, Def8 ;
::_thesis: verum
end;
supposethat A4: x <> {} and
A5: y <> {} and
A6: z <> {} ; ::_thesis: x + (y + z) = (x + y) + z
A7: now__::_thesis:_not_GLUED_((DEDEKIND_CUT_y)_+_(DEDEKIND_CUT_z))_=_{}
assume GLUED ((DEDEKIND_CUT y) + (DEDEKIND_CUT z)) = {} ; ::_thesis: contradiction
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; ::_thesis: verum
end;
A8: now__::_thesis:_not_GLUED_((DEDEKIND_CUT_x)_+_(DEDEKIND_CUT_y))_=_{}
assume GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) = {} ; ::_thesis: contradiction
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; ::_thesis: verum
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 ; ::_thesis: verum
end;
end;
end;
theorem :: ARYTM_2:7
{ A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } is c=-linear
proof
set IR = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
let x, y be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } or not y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } or x,y are_c=-comparable )
assume x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; ::_thesis: ( not y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } or x,y are_c=-comparable )
then A1: ex A9 being Subset of RAT+ st
( x = A9 & ( for r being Element of RAT+ st r in A9 holds
( ( for s being Element of RAT+ st s <=' r holds
s in A9 ) & ex s being Element of RAT+ st
( s in A9 & r < s ) ) ) ) ;
assume y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; ::_thesis: x,y are_c=-comparable
then A2: ex B9 being Subset of RAT+ st
( y = B9 & ( for r being Element of RAT+ st r in B9 holds
( ( for s being Element of RAT+ st s <=' r holds
s in B9 ) & ex s being Element of RAT+ st
( s in B9 & r < s ) ) ) ) ;
assume not x c= y ; :: according to XBOOLE_0:def_9 ::_thesis: y c= x
then consider s being set such that
A3: s in x and
A4: not s in y by TARSKI:def_3;
reconsider s = s as Element of RAT+ by A1, A3;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in y or e in x )
assume A5: e in y ; ::_thesis: e in x
then reconsider r = e as Element of RAT+ by A2;
r <=' s by A2, A4, A5;
hence e in x by A1, A3; ::_thesis: verum
end;
Lm28: for e being set st e in REAL+ holds
e <> RAT+
proof
let e be set ; ::_thesis: ( e in REAL+ implies e <> RAT+ )
assume e in REAL+ ; ::_thesis: e <> RAT+
then ( e in RAT+ or e in DEDEKIND_CUTS ) by XBOOLE_0:def_3;
hence e <> RAT+ by ZFMISC_1:56; ::_thesis: verum
end;
Lm29: for r, s being Element of RAT+
for B being set st B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & r in B & s <=' r holds
s in B
proof
let r, s be Element of RAT+ ; ::_thesis: for B being set st B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & r in B & s <=' r holds
s in B
let B be set ; ::_thesis: ( B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & r in B & s <=' r implies s in B )
assume that
A1: B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } and
A2: ( r in B & s <=' r ) ; ::_thesis: s in B
ex A being Subset of RAT+ st
( B = A & ( for t being Element of RAT+ st t in A holds
( ( for s being Element of RAT+ st s <=' t holds
s in A ) & ex s being Element of RAT+ st
( s in A & t < s ) ) ) ) by A1;
hence s in B by A2; ::_thesis: verum
end;
Lm30: for y, x being Element of REAL+ st y < x holds
ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )
proof
let y, x be Element of REAL+ ; ::_thesis: ( y < x implies ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z ) )
assume A1: y < x ; ::_thesis: ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )
percases ( ( x in RAT+ & y in RAT+ ) or ( not x in RAT+ & y in RAT+ ) or ( x in RAT+ & not y in RAT+ ) or ( not x in RAT+ & not y in RAT+ ) ) ;
suppose ( x in RAT+ & y in RAT+ ) ; ::_thesis: ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )
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;
z9 in RAT+ ;
then reconsider z = z9 as Element of REAL+ by Th1;
take z ; ::_thesis: ( z in RAT+ & z < x & y < z )
thus ( z in RAT+ & z < x & y < z ) by A2, Lm14; ::_thesis: verum
end;
supposethat A3: not x in RAT+ and
A4: y in RAT+ ; ::_thesis: ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )
reconsider y9 = y as Element of RAT+ by A4;
x in REAL+ ;
then x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A3, Lm3, XBOOLE_0:def_3;
then consider A being Subset of RAT+ such that
A5: x = A and
A6: for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) ;
y9 in x by A1, A3, Def5;
then consider s being Element of RAT+ such that
A7: s in A and
A8: y9 < s by A5, A6;
s in RAT+ ;
then reconsider z = s as Element of REAL+ by Th1;
take z ; ::_thesis: ( z in RAT+ & z < x & y < z )
thus z in RAT+ ; ::_thesis: ( z < x & y < z )
thus z < x by A3, A5, A7, Def5; ::_thesis: y < z
thus y < z by A8, Lm14; ::_thesis: verum
end;
supposethat A9: x in RAT+ and
A10: not y in RAT+ ; ::_thesis: ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )
reconsider x9 = x as Element of RAT+ by A9;
A11: not x9 in y by A1, A10, Def5;
y in REAL+ ;
then y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A10, Lm3, XBOOLE_0:def_3;
then consider B being Subset of RAT+ such that
A12: y = B and
A13: for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ 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 being Element of RAT+ st
( z9 < x9 & not z9 in y )
proof
set C = { s where s is Element of RAT+ : s < x9 } ;
assume A16: for z9 being Element of RAT+ holds
( not z9 < x9 or z9 in y ) ; ::_thesis: contradiction
y = { s where s is Element of RAT+ : s < x9 }
proof
thus y c= { s where s is Element of RAT+ : s < x9 } :: according to XBOOLE_0:def_10 ::_thesis: { s where s is Element of RAT+ : s < x9 } c= y
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in y or e in { s where s is Element of RAT+ : s < x9 } )
assume A17: e in y ; ::_thesis: e in { s where s is Element of RAT+ : s < x9 }
then reconsider z9 = e as Element of RAT+ by A12;
not x9 <=' z9 by A12, A13, A11, A17;
hence e in { s where s is Element of RAT+ : s < x9 } ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { s where s is Element of RAT+ : s < x9 } or e in y )
assume e in { s where s is Element of RAT+ : s < x9 } ; ::_thesis: e in y
then ex s being Element of RAT+ st
( e = s & s < x9 ) ;
hence e in y by A16; ::_thesis: verum
end;
then y in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A15;
hence contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
then consider z9 being Element of RAT+ such that
A18: z9 < x9 and
A19: not z9 in y ;
z9 in RAT+ ;
then reconsider z = z9 as Element of REAL+ by Th1;
take z ; ::_thesis: ( z in RAT+ & z < x & y < z )
thus z in RAT+ ; ::_thesis: ( z < x & y < z )
thus z < x by A18, Lm14; ::_thesis: y < z
thus y < z by A10, A19, Def5; ::_thesis: verum
end;
supposethat A20: not x in RAT+ and
A21: not y in RAT+ ; ::_thesis: ex z being Element of REAL+ st
( z in RAT+ & z < x & y < z )
y in REAL+ ;
then y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A21, Lm3, XBOOLE_0:def_3;
then consider B being Subset of RAT+ such that
A22: y = B and
for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) ) ;
x in REAL+ ;
then x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A20, Lm3, XBOOLE_0:def_3;
then consider A being Subset of RAT+ such that
A23: x = A and
for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ 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, SUBSET_1:2;
z9 in RAT+ ;
then reconsider z = z9 as Element of REAL+ by Th1;
take z ; ::_thesis: ( z in RAT+ & z < x & y < z )
thus z in RAT+ ; ::_thesis: ( z < x & y < z )
thus z < x by A20, A23, A24, Def5; ::_thesis: y < z
thus y < z by A21, A22, A25, Def5; ::_thesis: verum
end;
end;
end;
Lm31: for x, y, z being Element of REAL+ st x <=' y & y <=' z holds
x <=' z
proof
let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y & y <=' z implies x <=' z )
assume that
A1: x <=' y and
A2: y <=' z ; ::_thesis: x <=' z
percases ( ( x in RAT+ & y in RAT+ & z in RAT+ ) or ( x in RAT+ & y in RAT+ & not z in RAT+ ) or ( x in RAT+ & not y in RAT+ & z in RAT+ ) or ( x in RAT+ & not y in RAT+ & not z in RAT+ ) or ( not x in RAT+ & y in RAT+ & z in RAT+ ) or ( not x in RAT+ & y in RAT+ & not z in RAT+ ) or ( not x in RAT+ & not y in RAT+ & z in RAT+ ) or ( not x in RAT+ & not y in RAT+ & not z in RAT+ ) ) ;
supposethat A3: x in RAT+ and
A4: y in RAT+ and
A5: z in RAT+ ; ::_thesis: x <=' z
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 x <=' z by Lm14; ::_thesis: verum
end;
supposethat A6: x in RAT+ and
A7: y in RAT+ and
A8: not z in RAT+ ; ::_thesis: x <=' z
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 { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A8, Lm3, XBOOLE_0:def_3;
then consider C being Subset of RAT+ such that
A10: z = C and
A11: for r being Element of RAT+ st r in C holds
( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) ) ;
y in C by A2, A7, A8, A10, Def5;
then x9 in C by A11, A9;
hence x <=' z by A8, A10, Def5; ::_thesis: verum
end;
supposethat A12: x in RAT+ and
A13: not y in RAT+ and
A14: z in RAT+ ; ::_thesis: x <=' z
reconsider z9 = z as Element of RAT+ by A14;
reconsider x9 = x as Element of RAT+ by A12;
y in REAL+ ;
then y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A13, Lm3, XBOOLE_0:def_3;
then consider B being Subset of RAT+ such that
A15: y = B and
A16: for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ 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 x <=' z by Lm14; ::_thesis: verum
end;
supposethat A17: x in RAT+ and
A18: not y in RAT+ and
A19: not z in RAT+ ; ::_thesis: x <=' z
reconsider x9 = x as Element of RAT+ by A17;
y in REAL+ ;
then y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A18, Lm3, XBOOLE_0:def_3;
then consider B being Subset of RAT+ such that
A20: y = B and
for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) ) ;
A21: x9 in B by A1, A18, A20, Def5;
z in REAL+ ;
then z in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A19, Lm3, XBOOLE_0:def_3;
then consider C being Subset of RAT+ such that
A22: z = C and
for r being Element of RAT+ st r in C holds
( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) ) ;
B c= C by A2, A18, A19, A20, A22, Def5;
hence x <=' z by A19, A22, A21, Def5; ::_thesis: verum
end;
supposethat A23: not x in RAT+ and
A24: y in RAT+ and
A25: z in RAT+ ; ::_thesis: x <=' z
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 { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A23, Lm3, XBOOLE_0:def_3;
then consider A being Subset of RAT+ such that
A27: x = A and
A28: for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) ;
not y9 in A by A1, A23, A27, Def5;
then not z9 in A by A28, A26;
hence x <=' z by A23, A27, Def5; ::_thesis: verum
end;
supposethat A29: not x in RAT+ and
A30: y in RAT+ and
A31: not z in RAT+ ; ::_thesis: x <=' z
x in REAL+ ;
then x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A29, Lm3, XBOOLE_0:def_3;
then consider A being Subset of RAT+ such that
A32: x = A and
A33: for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ 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 { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A31, Lm3, XBOOLE_0:def_3;
then consider C being Subset of RAT+ such that
A35: z = C and
A36: for r being Element of RAT+ st r in C holds
( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) ) ;
A37: y in C by A2, A30, A31, A35, Def5;
A c= C
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A or e in C )
assume A38: e in A ; ::_thesis: e in C
then reconsider x9 = e as Element of RAT+ ;
x9 <=' y9 by A33, A34, A38;
hence e in C by A36, A37; ::_thesis: verum
end;
hence x <=' z by A29, A31, A32, A35, Def5; ::_thesis: verum
end;
supposethat A39: not x in RAT+ and
A40: not y in RAT+ and
A41: z in RAT+ ; ::_thesis: x <=' z
reconsider z9 = z as Element of RAT+ by A41;
x in REAL+ ;
then x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A39, Lm3, XBOOLE_0:def_3;
then consider A being Subset of RAT+ such that
A42: x = A and
for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) ;
y in REAL+ ;
then y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A40, Lm3, XBOOLE_0:def_3;
then consider B being Subset of RAT+ such that
A43: y = B and
for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ 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 x <=' z by A39, A42, Def5; ::_thesis: verum
end;
supposethat A44: not x in RAT+ and
A45: not y in RAT+ and
A46: not z in RAT+ ; ::_thesis: x <=' z
z in REAL+ ;
then z in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A46, Lm3, XBOOLE_0:def_3;
then consider C being Subset of RAT+ such that
A47: z = C and
for r being Element of RAT+ st r in C holds
( ( for s being Element of RAT+ st s <=' r holds
s in C ) & ex s being Element of RAT+ st
( s in C & r < s ) ) ;
y in REAL+ ;
then y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A45, Lm3, XBOOLE_0:def_3;
then consider B being Subset of RAT+ such that
A48: y = B and
for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) ) ;
A49: B c= C by A2, A45, A46, A48, A47, Def5;
x in REAL+ ;
then x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A44, Lm3, XBOOLE_0:def_3;
then consider A being Subset of RAT+ such that
A50: x = A and
for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) ;
A c= B by A1, A44, A45, A50, A48, Def5;
then A c= C by A49, XBOOLE_1:1;
hence x <=' z by A44, A46, A50, A47, Def5; ::_thesis: verum
end;
end;
end;
theorem :: ARYTM_2:8
for X, Y being Subset of REAL+ st ex x being Element of REAL+ st x in Y & ( for x, y being Element of REAL+ st x in X & y in Y holds
x <=' y ) holds
ex z being Element of REAL+ st
for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y )
proof
let X, Y be Subset of REAL+; ::_thesis: ( ex x being Element of REAL+ st x in Y & ( for x, y being Element of REAL+ st x in X & y in Y holds
x <=' y ) implies ex z being Element of REAL+ st
for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y ) )
given x1 being Element of REAL+ such that A1: x1 in Y ; ::_thesis: ( ex x, y being Element of REAL+ st
( x in X & y in Y & not x <=' y ) or ex z being Element of REAL+ st
for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y ) )
set Z = { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } ;
assume A2: for x, y being Element of REAL+ st x in X & y in Y holds
x <=' y ; ::_thesis: ex z being Element of REAL+ st
for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y )
percases ( ex z9 being Element of RAT+ st
for x9 being Element of RAT+ holds
( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < z9 ) or for z9 being Element of RAT+ holds
not for x9 being Element of RAT+ holds
( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < z9 ) ) ;
suppose ex z9 being Element of RAT+ st
for x9 being Element of RAT+ holds
( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < z9 ) ; ::_thesis: ex z being Element of REAL+ st
for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y )
then consider z9 being Element of RAT+ such that
A3: for x9 being Element of RAT+ holds
( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < z9 ) ;
z9 in RAT+ ;
then reconsider z = z9 as Element of REAL+ by Th1;
take z ; ::_thesis: for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y )
let x, y be Element of REAL+ ; ::_thesis: ( x in X & y in Y implies ( x <=' z & z <=' y ) )
assume that
A4: x in X and
A5: y in Y ; ::_thesis: ( x <=' z & z <=' y )
thus x <=' z ::_thesis: z <=' y
proof
assume z < x ; ::_thesis: contradiction
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 { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } ) by A4, A7, Lm14;
hence contradiction by A3; ::_thesis: verum
end;
assume y < z ; ::_thesis: contradiction
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 { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } by A3;
then ex y99 being Element of RAT+ st
( y9 = y99 & ex x, z being Element of REAL+ 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; ::_thesis: verum
end;
supposeA14: for z9 being Element of RAT+ holds
not for x9 being Element of RAT+ holds
( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < z9 ) ; ::_thesis: ex z being Element of REAL+ st
for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y )
A15: now__::_thesis:_not__{__z9_where_z9_is_Element_of_RAT+_:_ex_x,_z_being_Element_of_REAL+_st_
(_z_=_z9_&_x_in_X_&_z_<_x_)__}__in__{___{__s_where_s_is_Element_of_RAT+_:_s_<_t__}__where_t_is_Element_of_RAT+_:_t_<>_{}__}_
assume { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; ::_thesis: contradiction
then consider t being Element of RAT+ such that
A16: { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } = { s where s is Element of RAT+ : s < t } and
t <> {} ;
for x9 being Element of RAT+ holds
( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < t )
proof
let x9 be Element of RAT+ ; ::_thesis: ( x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } iff x9 < t )
hereby ::_thesis: ( x9 < t implies x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } )
assume x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } ; ::_thesis: x9 < t
then ex s being Element of RAT+ st
( s = x9 & s < t ) by A16;
hence x9 < t ; ::_thesis: verum
end;
thus ( x9 < t implies x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } ) by A16; ::_thesis: verum
end;
hence contradiction by A14; ::_thesis: verum
end;
A17: { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } c= RAT+
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } or e in RAT+ )
assume e in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } ; ::_thesis: e in RAT+
then ex z9 being Element of RAT+ st
( e = z9 & ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) ) ;
hence e in RAT+ ; ::_thesis: verum
end;
now__::_thesis:_not__{__z9_where_z9_is_Element_of_RAT+_:_ex_x,_z_being_Element_of_REAL+_st_
(_z_=_z9_&_x_in_X_&_z_<_x_)__}__=_{}
assume { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } = {} ; ::_thesis: contradiction
then A18: for x9 being Element of RAT+ st x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } holds
x9 < {} ;
for x9 being Element of RAT+ st x9 < {} holds
x9 in { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } by ARYTM_3:64;
hence contradiction by A14, A18; ::_thesis: verum
end;
then reconsider Z = { z9 where z9 is Element of RAT+ : ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) } as non empty Subset of RAT+ by A17;
A19: now__::_thesis:_not_Z_=_RAT+
assume A20: Z = RAT+ ; ::_thesis: contradiction
percases ( x1 in RAT+ or not x1 in RAT+ ) ;
suppose x1 in RAT+ ; ::_thesis: contradiction
then reconsider x9 = x1 as Element of RAT+ ;
x9 in Z by A20;
then ex z9 being Element of RAT+ st
( x9 = z9 & ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) ) ;
hence contradiction by A1, A2; ::_thesis: verum
end;
supposeA21: not x1 in RAT+ ; ::_thesis: contradiction
x1 in REAL+ ;
then x1 in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by A21, Lm3, XBOOLE_0:def_3;
then consider A being Subset of RAT+ such that
A22: x1 = A and
for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ 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;
x9 in RAT+ ;
then reconsider x2 = x9 as Element of REAL+ by Th1;
x2 in Z by A20;
then ex z9 being Element of RAT+ st
( x9 = z9 & ex x, z being Element of REAL+ st
( z = z9 & x in X & z < x ) ) ;
then consider x being Element of REAL+ 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; ::_thesis: verum
end;
end;
end;
for t being Element of RAT+ st t in Z holds
( ( for s being Element of RAT+ st s <=' t holds
s in Z ) & ex s being Element of RAT+ st
( s in Z & t < s ) )
proof
let t be Element of RAT+ ; ::_thesis: ( t in Z implies ( ( for s being Element of RAT+ st s <=' t holds
s in Z ) & ex s being Element of RAT+ st
( s in Z & t < s ) ) )
t in RAT+ ;
then reconsider y0 = t as Element of REAL+ by Th1;
assume t in Z ; ::_thesis: ( ( for s being Element of RAT+ st s <=' t holds
s in Z ) & ex s being Element of RAT+ st
( s in Z & t < s ) )
then ex z9 being Element of RAT+ st
( z9 = t & ex x, z being Element of REAL+ 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 being Element of RAT+ st s <=' t holds
s in Z ::_thesis: ex s being Element of RAT+ st
( s in Z & t < s )
proof
let s be Element of RAT+ ; ::_thesis: ( s <=' t implies s in Z )
s in RAT+ ;
then reconsider z = s as Element of REAL+ by Th1;
assume s <=' t ; ::_thesis: s in Z
then z <=' y0 by Lm14;
then z < x0 by A27, Lm31;
hence s in Z by A26; ::_thesis: verum
end;
consider z being Element of REAL+ 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 ; ::_thesis: ( z9 in Z & t < z9 )
thus z9 in Z by A26, A29; ::_thesis: t < z9
thus t < z9 by A30, Lm14; ::_thesis: verum
end;
then Z in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
then A31: Z in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } \ {RAT+} by A19, ZFMISC_1:56;
then Z in ( { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } \ {RAT+}) \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } by A15, XBOOLE_0:def_5;
then reconsider z = Z as Element of REAL+ by Lm4;
take z ; ::_thesis: for x, y being Element of REAL+ st x in X & y in Y holds
( x <=' z & z <=' y )
let x, y be Element of REAL+ ; ::_thesis: ( x in X & y in Y implies ( x <=' z & z <=' y ) )
assume that
A32: x in X and
A33: y in Y ; ::_thesis: ( x <=' z & z <=' y )
A34: now__::_thesis:_not_z_in_RAT+
assume z in RAT+ ; ::_thesis: contradiction
then z in {{}} by A31, Lm9, XBOOLE_0:def_4;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
hereby ::_thesis: z <=' y
assume z < x ; ::_thesis: contradiction
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; ::_thesis: verum
end;
assume y < z ; ::_thesis: contradiction
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 being Element of RAT+ st
( y9 = z9 & ex x, z being Element of REAL+ 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; ::_thesis: verum
end;
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 ; ::_thesis: ( A + B = A & A <> {} implies B = {} )
assume that
A1: A + B = A and
A2: A <> {} and
A3: B <> {} ; ::_thesis: contradiction
A4: ex A0 being Element of RAT+ st A0 in A by A2, SUBSET_1:4;
consider y9 being Element of RAT+ such that
A5: y9 in B and
A6: y9 <> {} by A3, Lm15;
defpred S1[ Element of RAT+ ] means $1 *' y9 in A;
{} *' y9 = {} by ARYTM_3:48;
then A7: S1[ {} ] by A4, Lm16, ARYTM_3:64;
A <> RAT+ by ZFMISC_1:56;
then consider r being Element of RAT+ 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 S1[n] by A8, A10, Lm16;
consider n0 being Element of RAT+ such that
n0 in omega and
A12: ( S1[n0] & not S1[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; ::_thesis: verum
end;
Lm35: for x, y being Element of REAL+ st x + y = x holds
y = {}
proof
let x, y be Element of REAL+ ; ::_thesis: ( x + y = x implies y = {} )
assume that
A1: x + y = x and
A2: y <> {} ; ::_thesis: contradiction
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; ::_thesis: verum
end;
Lm36: for A, B being Element of DEDEKIND_CUTS st A <> {} & A c= B & A <> B holds
ex C being Element of DEDEKIND_CUTS st A + C = B
proof
let A, B be Element of DEDEKIND_CUTS ; ::_thesis: ( A <> {} & A c= B & A <> B implies ex C being Element of DEDEKIND_CUTS st A + C = B )
assume that
A1: A <> {} and
A2: ( A c= B & A <> B ) ; ::_thesis: ex C being Element of DEDEKIND_CUTS st A + C = B
not B c= A by A2, XBOOLE_0:def_10;
then consider s1 being Element of RAT+ such that
A3: ( s1 in B & not s1 in A ) by SUBSET_1:2;
set DIF = { t where t is Element of RAT+ : ex r, s being Element of RAT+ st
( not r in A & s in B & r + t = s ) } ;
A4: { t where t is Element of RAT+ : ex r, s being Element of RAT+ st
( not r in A & s in B & r + t = s ) } c= RAT+
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { t where t is Element of RAT+ : ex r, s being Element of RAT+ st
( not r in A & s in B & r + t = s ) } or e in RAT+ )
assume e in { t where t is Element of RAT+ : ex r, s being Element of RAT+ st
( not r in A & s in B & r + t = s ) } ; ::_thesis: e in RAT+
then ex t being Element of RAT+ st
( t = e & ex r, s being Element of RAT+ st
( not r in A & s in B & r + t = s ) ) ;
hence e in RAT+ ; ::_thesis: verum
end;
s1 + {} = s1 by ARYTM_3:84;
then A5: {} in { t where t is Element of RAT+ : ex r, s being Element of RAT+ st
( not r in A & s in B & r + t = s ) } by A3;
then reconsider DIF = { t where t is Element of RAT+ : ex r, s being Element of RAT+ st
( not r in A & s in B & r + t = s ) } as non empty Subset of RAT+ by A4;
for t being Element of RAT+ st t in DIF holds
( ( for s being Element of RAT+ st s <=' t holds
s in DIF ) & ex s being Element of RAT+ st
( s in DIF & t < s ) )
proof
let t be Element of RAT+ ; ::_thesis: ( t in DIF implies ( ( for s being Element of RAT+ st s <=' t holds
s in DIF ) & ex s being Element of RAT+ st
( s in DIF & t < s ) ) )
assume t in DIF ; ::_thesis: ( ( for s being Element of RAT+ st s <=' t holds
s in DIF ) & ex s being Element of RAT+ st
( s in DIF & t < s ) )
then ex x9 being Element of RAT+ st
( x9 = t & ex r, s being Element of RAT+ 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 being Element of RAT+ st s <=' t holds
s in DIF ::_thesis: ex s being Element of RAT+ st
( s in DIF & t < s )
proof
let s be Element of RAT+ ; ::_thesis: ( s <=' t implies s in DIF )
assume s <=' t ; ::_thesis: s in DIF
then consider p being Element of RAT+ such that
A9: s + p = t by ARYTM_3:def_13;
A10: t <=' s0 by A8, ARYTM_3:77;
p <=' t by A9, ARYTM_3:77;
then p <=' s0 by A10, ARYTM_3:67;
then consider q being Element of RAT+ such that
A11: p + q = s0 by ARYTM_3:def_13;
(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 s in DIF by A6, A12; ::_thesis: verum
end;
consider s1 being Element of RAT+ such that
A13: s1 in B and
A14: s0 < s1 by A7, Lm7;
consider q being Element of RAT+ such that
A15: s0 + q = s1 by A14, ARYTM_3:def_13;
take t + q ; ::_thesis: ( t + q in DIF & t < t + q )
A16: r0 + (t + q) = s1 by A8, A15, ARYTM_3:51;
hence t + q in DIF by A6, A13; ::_thesis: t < t + q
( t <=' t + q & t <> t + q ) by A8, A14, A16, ARYTM_3:77;
hence t < t + q by ARYTM_3:68; ::_thesis: verum
end;
then A17: DIF in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
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__::_thesis:_not_s2_in_DIF
assume s2 in DIF ; ::_thesis: contradiction
then ex t being Element of RAT+ st
( t = s2 & ex r, s being Element of RAT+ st
( not r in A & s in B & r + t = s ) ) ;
hence contradiction by A18, Lm16, ARYTM_3:77; ::_thesis: verum
end;
then DIF <> RAT+ ;
then reconsider DIF = DIF as Element of DEDEKIND_CUTS by A17, ZFMISC_1:56;
take DIF ; ::_thesis: A + DIF = B
set C = { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } ;
B = { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) }
proof
thus B c= { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } :: according to XBOOLE_0:def_10 ::_thesis: { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } c= B
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in B or e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } )
assume A19: e in B ; ::_thesis: e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) }
then reconsider y9 = e as Element of RAT+ ;
percases ( y9 in A or not y9 in A ) ;
supposeA20: y9 in A ; ::_thesis: e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) }
y9 = y9 + {} by ARYTM_3:84;
hence e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } by A5, A20; ::_thesis: verum
end;
supposeA21: not y9 in A ; ::_thesis: e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) }
consider s0 being Element of RAT+ such that
A22: s0 in B and
A23: y9 < s0 by A19, Lm7;
set Z = { r where r is Element of RAT+ : ex x9 being Element of RAT+ 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 holds
ex s, t being Element of RAT+ st
( s in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } & r2 = s + t )
proof
let r2 be Element of RAT+ ; ::_thesis: ( r2 < s0 implies ex s, t being Element of RAT+ st
( s in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } & r2 = s + t ) )
assume A26: r2 < s0 ; ::_thesis: ex s, t being Element of RAT+ st
( s in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } & r2 = s + t )
then A27: r2 <> s0 ;
percases ( r2 in A or not r2 in A ) ;
supposeA28: r2 in A ; ::_thesis: ex s, t being Element of RAT+ st
( s in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } & r2 = s + t )
take r2 ; ::_thesis: ex t being Element of RAT+ st
( r2 in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } & r2 = r2 + t )
take {} ; ::_thesis: ( r2 in A & {} in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } & r2 = r2 + {} )
thus r2 in A by A28; ::_thesis: ( {} in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } & r2 = r2 + {} )
thus {} in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } by A24, A25; ::_thesis: r2 = r2 + {}
thus r2 = r2 + {} by ARYTM_3:84; ::_thesis: verum
end;
supposeA29: not r2 in A ; ::_thesis: ex s, t being Element of RAT+ st
( s in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } & r2 = s + t )
consider q being Element of RAT+ such that
A30: r2 + q = s0 by A26, ARYTM_3:def_13;
defpred S1[ Element of RAT+ ] means $1 *' q in A;
{} *' q = {} by ARYTM_3:48;
then A31: S1[ {} ] 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 S1[n] by A24, A33, Lm16;
consider n0 being Element of RAT+ such that
n0 in omega and
A35: S1[n0] and
A36: not S1[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 being Element of RAT+ such that
A37: ((n0 *' q) + q) + t = s0 by ARYTM_3:def_13;
take n0 *' q ; ::_thesis: ex t being Element of RAT+ st
( n0 *' q in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } & r2 = (n0 *' q) + t )
take t ; ::_thesis: ( n0 *' q in A & t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } & r2 = (n0 *' q) + t )
thus n0 *' q in A by A35; ::_thesis: ( t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } & r2 = (n0 *' q) + t )
(n0 + one) *' q = (n0 *' q) + (one *' q) by ARYTM_3:57
.= (n0 *' q) + q by ARYTM_3:53 ;
hence t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } by A36, A37; ::_thesis: r2 = (n0 *' q) + t
((n0 *' q) + t) + q = r2 + q by A30, A37, ARYTM_3:51;
hence r2 = (n0 *' q) + t by ARYTM_3:62; ::_thesis: verum
end;
end;
end;
then consider s, t being Element of RAT+ such that
A38: s in A and
A39: t in { r where r is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) } and
A40: y9 = s + t by A23;
ex r being Element of RAT+ st
( t = r & ex x9 being Element of RAT+ st
( not x9 in A & x9 + r = s0 ) ) by A39;
then t in DIF by A22;
hence e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } by A38, A40; ::_thesis: verum
end;
end;
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } or e in B )
assume e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) } ; ::_thesis: e in B
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 being Element of RAT+ st
( t3 = t & ex r, s being Element of RAT+ 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 e in B by A41, A45, Lm16; ::_thesis: verum
end;
hence A + DIF = B ; ::_thesis: verum
end;
Lm37: for x, y being Element of REAL+ st x <=' y holds
DEDEKIND_CUT x c= DEDEKIND_CUT y
proof
let x, y be Element of REAL+ ; ::_thesis: ( x <=' y implies DEDEKIND_CUT x c= DEDEKIND_CUT y )
assume A1: x <=' y ; ::_thesis: DEDEKIND_CUT x c= DEDEKIND_CUT y
assume A2: not DEDEKIND_CUT x c= DEDEKIND_CUT y ; ::_thesis: contradiction
( DEDEKIND_CUT x in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & DEDEKIND_CUT y in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ) by XBOOLE_0:def_5;
then DEDEKIND_CUT y c= DEDEKIND_CUT x by A2, Lm13;
then y <=' x by Lm20;
hence contradiction by A1, A2, Lm21; ::_thesis: verum
end;
theorem Th9: :: ARYTM_2:9
for x, y being Element of REAL+ st x <=' y holds
ex z being Element of REAL+ st x + z = y
proof
let x, y be Element of REAL+ ; ::_thesis: ( x <=' y implies ex z being Element of REAL+ st x + z = y )
assume A1: x <=' y ; ::_thesis: ex z being Element of REAL+ st x + z = y
percases ( x = {} or x = y or ( x <> {} & x <> y ) ) ;
supposeA2: x = {} ; ::_thesis: ex z being Element of REAL+ st x + z = y
take y ; ::_thesis: x + y = y
thus x + y = y by A2, Def8; ::_thesis: verum
end;
supposeA3: x = y ; ::_thesis: ex z being Element of REAL+ st x + z = y
{} in RAT+ ;
then reconsider z = {} as Element of REAL+ by Th1;
take z ; ::_thesis: x + z = y
thus x + z = y by A3, Def8; ::_thesis: verum
end;
supposethat A4: x <> {} and
A5: x <> y ; ::_thesis: ex z being Element of REAL+ st x + z = 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 ; ::_thesis: x + (GLUED C) = y
now__::_thesis:_not_C_=_{}
assume A8: C = {} ; ::_thesis: contradiction
for e being set holds not e in { (r + s) where r, s is Element of RAT+ : ( r in C & s in DEDEKIND_CUT x ) }
proof
given e being set such that A9: e in { (r + s) where r, s is Element of RAT+ : ( r in C & s in DEDEKIND_CUT x ) } ; ::_thesis: contradiction
ex r, s being Element of RAT+ st
( e = r + s & r in C & s in DEDEKIND_CUT x ) by A9;
hence contradiction by A8; ::_thesis: verum
end;
then { (r + s) where r, s is Element of RAT+ : ( 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; ::_thesis: verum
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 ;
::_thesis: verum
end;
end;
end;
theorem Th10: :: ARYTM_2:10
for x, y being Element of REAL+ ex z being Element of REAL+ st
( x + z = y or y + z = x )
proof
let x, y be Element of REAL+ ; ::_thesis: ex z being Element of REAL+ st
( x + z = y or y + z = x )
( x <=' y or y <=' x ) ;
hence ex z being Element of REAL+ st
( x + z = y or y + z = x ) by Th9; ::_thesis: verum
end;
theorem Th11: :: ARYTM_2:11
for x, y, z being Element of REAL+ st x + y = x + z holds
y = z
proof
let x, y, z be Element of REAL+ ; ::_thesis: ( x + y = x + z implies y = z )
assume A1: x + y = x + z ; ::_thesis: y = z
consider q being Element of REAL+ such that
A2: ( z + q = y or y + q = z ) by Th10;
percases ( z + q = y or y + q = z ) by A2;
supposeA3: z + q = y ; ::_thesis: y = z
then x + y = (x + y) + q by A1, Th6;
then q = {} by Lm35;
hence y = z by A3, Def8; ::_thesis: verum
end;
supposeA4: y + q = z ; ::_thesis: y = z
then x + z = (x + z) + q by A1, Th6;
then q = {} by Lm35;
hence y = z by A4, Def8; ::_thesis: verum
end;
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 ; ::_thesis: A *' (B *' C) c= (A *' B) *' C
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A *' (B *' C) or e in (A *' B) *' C )
assume e in A *' (B *' C) ; ::_thesis: 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 e in (A *' B) *' C by A4; ::_thesis: verum
end;
Lm39: for A, B, C being Element of DEDEKIND_CUTS holds A *' (B *' C) = (A *' B) *' C
proof
let A, B, C be Element of DEDEKIND_CUTS ; ::_thesis: A *' (B *' C) = (A *' B) *' C
( A *' (B *' C) c= (A *' B) *' C & (A *' B) *' C c= A *' (B *' C) ) by Lm38;
hence A *' (B *' C) = (A *' B) *' C by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: ARYTM_2:12
for x, y, z being Element of REAL+ holds x *' (y *' z) = (x *' y) *' z
proof
let x, y, z be Element of REAL+ ; ::_thesis: x *' (y *' z) = (x *' y) *' z
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 ; ::_thesis: verum
end;
Lm40: for x, y being Element of REAL+ holds
( not x *' y = {} or x = {} or y = {} )
proof
let x, y be Element of REAL+ ; ::_thesis: ( not x *' y = {} or x = {} or y = {} )
assume A1: x *' y = {} ; ::_thesis: ( x = {} or y = {} )
( DEDEKIND_CUT x = {} or DEDEKIND_CUT y = {} )
proof
assume DEDEKIND_CUT x <> {} ; ::_thesis: DEDEKIND_CUT y = {}
then consider r0 being Element of RAT+ such that
A2: r0 in DEDEKIND_CUT x by SUBSET_1:4;
assume DEDEKIND_CUT y <> {} ; ::_thesis: contradiction
then consider s0 being Element of RAT+ such that
A3: s0 in DEDEKIND_CUT y by SUBSET_1:4;
r0 *' s0 in { (r *' s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) } by A2, A3;
hence contradiction by A1, Lm11; ::_thesis: verum
end;
hence ( x = {} or y = {} ) by Lm10; ::_thesis: verum
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 ; ::_thesis: A *' (B + C) = (A *' B) + (A *' C)
thus A *' (B + C) c= (A *' B) + (A *' C) :: according to XBOOLE_0:def_10 ::_thesis: (A *' B) + (A *' C) c= A *' (B + C)
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A *' (B + C) or e in (A *' B) + (A *' C) )
assume e in A *' (B + C) ; ::_thesis: e in (A *' B) + (A *' 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 e in (A *' B) + (A *' C) by A6; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (A *' B) + (A *' C) or e in A *' (B + C) )
assume e in (A *' B) + (A *' C) ; ::_thesis: e in A *' (B + 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;
percases ( r0 <=' r09 or r09 <=' r0 ) ;
suppose r0 <=' r09 ; ::_thesis: e in A *' (B + C)
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 e in A *' (B + C) by A14, A18; ::_thesis: verum
end;
suppose r09 <=' r0 ; ::_thesis: e in A *' (B + C)
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 e in A *' (B + C) by A11, A21; ::_thesis: verum
end;
end;
end;
theorem :: ARYTM_2:13
for x, y, z being Element of REAL+ holds x *' (y + z) = (x *' y) + (x *' z)
proof
let x, y, z be Element of REAL+ ; ::_thesis: x *' (y + z) = (x *' y) + (x *' z)
percases ( x = {} or y = {} or z = {} or ( x <> {} & y <> {} & z <> {} ) ) ;
supposeA1: x = {} ; ::_thesis: x *' (y + z) = (x *' y) + (x *' z)
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 ;
::_thesis: verum
end;
supposeA2: y = {} ; ::_thesis: x *' (y + z) = (x *' y) + (x *' z)
hence x *' (y + z) = x *' z by Def8
.= y + (x *' z) by A2, Def8
.= (x *' y) + (x *' z) by A2, Th4 ;
::_thesis: verum
end;
supposeA3: z = {} ; ::_thesis: x *' (y + z) = (x *' y) + (x *' z)
hence x *' (y + z) = x *' y by Def8
.= (x *' y) + z by A3, Def8
.= (x *' y) + (x *' z) by A3, Th4 ;
::_thesis: verum
end;
supposethat A4: x <> {} and
A5: ( y <> {} & z <> {} ) ; ::_thesis: x *' (y + z) = (x *' y) + (x *' 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 ; ::_thesis: verum
end;
end;
end;
one in RAT+
;
then reconsider rone = one as Element of REAL+ by Th1;
Lm42: for B being set st B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & B <> {} holds
ex r being Element of RAT+ st
( r in B & r <> {} )
proof
let B be set ; ::_thesis: ( B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } & B <> {} implies ex r being Element of RAT+ st
( r in B & r <> {} ) )
assume that
A1: B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } and
A2: B <> {} ; ::_thesis: ex r being Element of RAT+ st
( r in B & r <> {} )
consider A being Subset of RAT+ such that
A3: B = A and
A4: for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ 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 being Element of RAT+ 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 ex r being Element of RAT+ st
( r in B & r <> {} ) by A3, A9; ::_thesis: verum
end;
Lm43: for A being Element of DEDEKIND_CUTS st A <> {} holds
ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone
proof
let A be Element of DEDEKIND_CUTS ; ::_thesis: ( A <> {} implies ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone )
assume A1: A <> {} ; ::_thesis: ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone
percases ( A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } or not A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ) ;
suppose A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; ::_thesis: ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone
then consider r0 being Element of RAT+ such that
A2: A = { s where s is Element of RAT+ : 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 where s is Element of RAT+ : s < s0 } ;
{ s where s is Element of RAT+ : s < s0 } c= RAT+
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { s where s is Element of RAT+ : s < s0 } or e in RAT+ )
assume e in { s where s is Element of RAT+ : s < s0 } ; ::_thesis: e in RAT+
then ex s being Element of RAT+ st
( s = e & s < s0 ) ;
hence e in RAT+ ; ::_thesis: verum
end;
then reconsider B = { s where s is Element of RAT+ : s < s0 } as Subset of RAT+ ;
for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) )
proof
let r be Element of RAT+ ; ::_thesis: ( r in B implies ( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) ) )
assume r in B ; ::_thesis: ( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) )
then A5: ex s being Element of RAT+ st
( s = r & s < s0 ) ;
then consider t being Element of RAT+ such that
A6: r < t and
A7: t < s0 by ARYTM_3:93;
thus for s being Element of RAT+ st s <=' r holds
s in B ::_thesis: ex s being Element of RAT+ st
( s in B & r < s )
proof
let s be Element of RAT+ ; ::_thesis: ( s <=' r implies s in B )
assume s <=' r ; ::_thesis: s in B
then s < s0 by A5, ARYTM_3:69;
hence s in B ; ::_thesis: verum
end;
take t ; ::_thesis: ( t in B & r < t )
thus t in B by A7; ::_thesis: r < t
thus r < t by A6; ::_thesis: verum
end;
then A8: B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
for s being Element of RAT+ holds
( not s = s0 or not s < s0 ) ;
then not s0 in B ;
then B <> RAT+ ;
then reconsider B = B as Element of DEDEKIND_CUTS by A8, ZFMISC_1:56;
A9: A *' B = { s where s is Element of RAT+ : s < r0 *' s0 }
proof
thus A *' B c= { s where s is Element of RAT+ : s < r0 *' s0 } :: according to XBOOLE_0:def_10 ::_thesis: { s where s is Element of RAT+ : s < r0 *' s0 } c= A *' B
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A *' B or e in { s where s is Element of RAT+ : s < r0 *' s0 } )
assume e in A *' B ; ::_thesis: e in { s where s is Element of RAT+ : s < r0 *' s0 }
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 being Element of RAT+ st
( s = r1 & s < r0 ) by A2, A11;
then A13: r1 *' s1 <=' r0 *' s1 by ARYTM_3:82;
A14: ex s being Element of RAT+ 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 e in { s where s is Element of RAT+ : s < r0 *' s0 } by A10; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { s where s is Element of RAT+ : s < r0 *' s0 } or e in A *' B )
assume e in { s where s is Element of RAT+ : s < r0 *' s0 } ; ::_thesis: e in A *' B
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 e in A *' B by A16, A18, A20, A22; ::_thesis: verum
end;
ex t0 being Element of RAT+ st
( t0 = rone & DEDEKIND_CUT rone = { s where s is Element of RAT+ : s < t0 } ) by Def3;
hence ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone by A4, A9; ::_thesis: verum
end;
supposeA24: not A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; ::_thesis: ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone
set B = { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) } ;
A25: { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) } c= RAT+
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) } or e in RAT+ )
assume e in { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) } ; ::_thesis: e in RAT+
then ex y9 being Element of RAT+ st
( y9 = e & ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) ) ;
hence e in RAT+ ; ::_thesis: verum
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 { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) } by A27;
then reconsider B = { y9 where y9 is Element of RAT+ : ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) } as non empty Subset of RAT+ by A25;
A29: A in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } by ZFMISC_1:56;
ex x9 being Element of RAT+ st x9 in A by A1, SUBSET_1:4;
then A30: {} in A by A29, Lm29, ARYTM_3:64;
for r being Element of RAT+ st r in B holds
( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) )
proof
let r be Element of RAT+ ; ::_thesis: ( r in B implies ( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) ) )
assume r in B ; ::_thesis: ( ( for s being Element of RAT+ st s <=' r holds
s in B ) & ex s being Element of RAT+ st
( s in B & r < s ) )
then ex y9 being Element of RAT+ st
( r = y9 & ex x9 being Element of RAT+ st
( not x9 in A & x9 *' y9 <=' one ) ) ;
then consider x9 being Element of RAT+ such that
A31: not x9 in A and
A32: x9 *' r <=' one ;
thus for s being Element of RAT+ st s <=' r holds
s in B ::_thesis: ex s being Element of RAT+ st
( s in B & r < s )
proof
let s be Element of RAT+ ; ::_thesis: ( s <=' r implies s in B )
assume s <=' r ; ::_thesis: s in B
then x9 *' s <=' x9 *' r by ARYTM_3:82;
then x9 *' s <=' one by A32, ARYTM_3:67;
hence s in B by A31; ::_thesis: verum
end;
A in DEDEKIND_CUTS \ { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } 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 being Element of RAT+ such that
A35: one = x99 *' s by A30, A33, ARYTM_3:55;
take s ; ::_thesis: ( s in B & r < s )
x99 *' s <=' one by A35;
hence s in B by A33; ::_thesis: r < s
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 r < s by A37, ARYTM_3:68; ::_thesis: verum
end;
then A38: B in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
consider x9 being Element of RAT+ such that
A39: x9 in A and
A40: x9 <> {} by A1, A29, Lm42;
consider y9 being Element of RAT+ such that
A41: x9 *' y9 = one by A40, ARYTM_3:55;
now__::_thesis:_not_y9_in_B
assume y9 in B ; ::_thesis: contradiction
then A42: ex s being Element of RAT+ st
( s = y9 & ex x9 being Element of RAT+ 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; ::_thesis: verum
end;
then B <> RAT+ ;
then not B in {RAT+} by TARSKI:def_1;
then reconsider B = B as Element of DEDEKIND_CUTS by A38, XBOOLE_0:def_5;
take B ; ::_thesis: A *' B = DEDEKIND_CUT rone
for r being Element of RAT+ holds
( r in A *' B iff r < one )
proof
let r be Element of RAT+ ; ::_thesis: ( r in A *' B iff r < one )
hereby ::_thesis: ( r < one implies r in A *' B )
assume r in A *' B ; ::_thesis: r < one
then consider s, t being Element of RAT+ such that
A43: r = s *' t and
A44: s in A and
A45: t in B ;
ex z9 being Element of RAT+ st
( z9 = t & ex x9 being Element of RAT+ st
( not x9 in A & x9 *' z9 <=' one ) ) by A45;
then consider x9 being Element of RAT+ 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__::_thesis:_not_r_=_one
assume A50: r = one ; ::_thesis: contradiction
then t <> {} by A43, ARYTM_3:48;
hence contradiction by A43, A44, A46, A47, A48, A50, ARYTM_3:56, ARYTM_3:66; ::_thesis: verum
end;
r <=' one by A43, A47, A48, ARYTM_3:67;
hence r < one by A49, ARYTM_3:68; ::_thesis: verum
end;
assume A51: r < one ; ::_thesis: r in A *' B
then A52: r <> one ;
percases ( r = {} or r <> {} ) ;
suppose r = {} ; ::_thesis: r in A *' B
then r = {} *' {} by ARYTM_3:48;
hence r in A *' B by A28, A30; ::_thesis: verum
end;
suppose r <> {} ; ::_thesis: r in A *' B
then consider r9 being Element of RAT+ such that
A53: r *' r9 = one by ARYTM_3:55;
{ (r *' s) where s is Element of RAT+ : s in A } c= RAT+
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (r *' s) where s is Element of RAT+ : s in A } or e in RAT+ )
assume e in { (r *' s) where s is Element of RAT+ : s in A } ; ::_thesis: e in RAT+
then ex s being Element of RAT+ st
( e = r *' s & s in A ) ;
hence e in RAT+ ; ::_thesis: verum
end;
then reconsider rA = { (r *' s) where s is Element of RAT+ : 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 *' (x9 *' dr) by A40, ARYTM_3:78, ARYTM_3:95;
defpred S1[ Element of RAT+ ] means $1 *' (x9 *' dr) in A;
A58: S1[ {} ] by A30, ARYTM_3:48;
A59: not S1[n0] by A29, A55, A57, Lm29;
consider n1 being Element of RAT+ such that
n1 in omega and
A60: S1[n1] and
A61: not S1[n1 + one] from ARYTM_3:sch_1(Lm32, Lm33, A56, A58, A59);
set s0 = n1 *' (x9 *' dr);
A62: now__::_thesis:_not_n1_*'_(x9_*'_dr)_in_rA
assume n1 *' (x9 *' dr) in rA ; ::_thesis: contradiction
then consider s0 being Element of RAT+ such that
A63: r *' s0 = n1 *' (x9 *' dr) and
A64: s0 in A ;
A65: (n1 + one) *' (x9 *' dr) = (n1 *' (x9 *' dr)) + (one *' (x9 *' dr)) 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; ::_thesis: verum
end;
A69: now__::_thesis:_not_(n1_*'_(x9_*'_dr))_*'_r9_in_A
assume A70: (n1 *' (x9 *' dr)) *' r9 in A ; ::_thesis: contradiction
r *' ((n1 *' (x9 *' dr)) *' r9) = one *' (n1 *' (x9 *' dr)) by A53, ARYTM_3:52
.= n1 *' (x9 *' dr) by ARYTM_3:53 ;
hence contradiction by A62, A70; ::_thesis: verum
end;
r *' {} = {} by ARYTM_3:48;
then {} in rA by A30;
then consider s9 being Element of RAT+ such that
A71: (n1 *' (x9 *' dr)) *' s9 = one by A62, ARYTM_3:55;
A72: (n1 *' (x9 *' dr)) *' (r *' s9) = ((n1 *' (x9 *' dr)) *' s9) *' r by ARYTM_3:52
.= r by A71, ARYTM_3:53 ;
((n1 *' (x9 *' dr)) *' r9) *' (r *' s9) = (((n1 *' (x9 *' dr)) *' r9) *' r) *' s9 by ARYTM_3:52
.= ((n1 *' (x9 *' dr)) *' one) *' s9 by A53, ARYTM_3:52
.= one by A71, ARYTM_3:53 ;
then ((n1 *' (x9 *' dr)) *' r9) *' (r *' s9) <=' one ;
then r *' s9 in B by A69;
hence r in A *' B by A60, A72; ::_thesis: verum
end;
end;
end;
then DEDEKIND_CUT (GLUED (A *' B)) = DEDEKIND_CUT rone by Def4;
hence A *' B = DEDEKIND_CUT rone by Lm12; ::_thesis: verum
end;
end;
end;
theorem :: ARYTM_2:14
for x being Element of REAL+ st x <> {} holds
ex y being Element of REAL+ st x *' y = one
proof
let x be Element of REAL+ ; ::_thesis: ( x <> {} implies ex y being Element of REAL+ st x *' y = one )
assume x <> {} ; ::_thesis: ex y being Element of REAL+ st x *' y = one
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; ::_thesis: x *' y = one
thus x *' y = GLUED (DEDEKIND_CUT rone) by A1, Lm12
.= one by Lm23 ; ::_thesis: verum
end;
Lm44: for A, B being Element of DEDEKIND_CUTS st A = { r where r is Element of RAT+ : r < one } holds
A *' B = B
proof
let A, B be Element of DEDEKIND_CUTS ; ::_thesis: ( A = { r where r is Element of RAT+ : r < one } implies A *' B = B )
assume A1: A = { r where r is Element of RAT+ : r < one } ; ::_thesis: A *' B = B
thus A *' B c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= A *' B
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in A *' B or e in B )
assume e in A *' B ; ::_thesis: e in B
then consider r, s being Element of RAT+ such that
A2: e = r *' s and
A3: r in A and
A4: s in B ;
ex t being Element of RAT+ 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 e in B by A2, A4, Lm16; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in B or e in A *' B )
assume A5: e in B ; ::_thesis: e in A *' 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__::_thesis:_not_s2_=_one
assume s2 = one ; ::_thesis: contradiction
then s = s1 by A8, ARYTM_3:53;
hence contradiction by A7; ::_thesis: verum
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 e in A *' B by A6, A8; ::_thesis: verum
end;
theorem :: ARYTM_2:15
for x, y being Element of REAL+ st x = one holds
x *' y = y
proof
let x, y be Element of REAL+ ; ::_thesis: ( x = one implies x *' y = y )
assume A1: x = one ; ::_thesis: x *' y = y
then ex r being Element of RAT+ st
( x = r & DEDEKIND_CUT x = { s where s is Element of RAT+ : s < r } ) by Def3;
hence x *' y = GLUED (DEDEKIND_CUT y) by A1, Lm44
.= y by Lm23 ;
::_thesis: verum
end;
Lm45: for i, j being Element of omega
for x9, y9 being Element of RAT+ st i = x9 & j = y9 holds
i +^ j = x9 + y9
proof
let i, j be Element of omega ; ::_thesis: for x9, y9 being Element of RAT+ st i = x9 & j = y9 holds
i +^ j = x9 + y9
let x9, y9 be Element of RAT+ ; ::_thesis: ( i = x9 & j = y9 implies i +^ j = x9 + y9 )
set a = (denominator x9) *^ (denominator y9);
set b = ((numerator x9) *^ (denominator y9)) +^ ((numerator y9) *^ (denominator x9));
assume A1: i = x9 ; ::_thesis: ( not j = y9 or i +^ j = x9 + y9 )
then A2: denominator x9 = one by ARYTM_3:def_9;
assume A3: j = y9 ; ::_thesis: i +^ j = x9 + y9
then A4: denominator y9 = one by ARYTM_3:def_9;
then A5: (denominator x9) *^ (denominator y9) = one by A2, ORDINAL2:39;
then A6: RED (((denominator x9) *^ (denominator y9)),(((numerator x9) *^ (denominator y9)) +^ ((numerator y9) *^ (denominator x9)))) = one by ARYTM_3:24;
((numerator x9) *^ (denominator y9)) +^ ((numerator y9) *^ (denominator x9)) = ((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 ((((numerator x9) *^ (denominator y9)) +^ ((numerator y9) *^ (denominator x9))),((denominator x9) *^ (denominator y9))) by A5, ARYTM_3:24
.= x9 + y9 by A6, ARYTM_3:def_10 ;
::_thesis: verum
end;
Lm46: for z9, x9, y9 being Element of RAT+ st z9 < x9 + y9 & x9 <> {} & y9 <> {} holds
ex r, s being Element of RAT+ st
( z9 = r + s & r < x9 & s < y9 )
proof
let z9, x9, y9 be Element of RAT+ ; ::_thesis: ( z9 < x9 + y9 & x9 <> {} & y9 <> {} implies ex r, s being Element of RAT+ st
( z9 = r + s & r < x9 & s < y9 ) )
assume that
A1: z9 < x9 + y9 and
A2: x9 <> {} and
A3: y9 <> {} ; ::_thesis: ex r, s being Element of RAT+ st
( z9 = r + s & r < x9 & s < 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;
percases ( r0 = {} or r0 <> {} ) ;
supposeA7: r0 = {} ; ::_thesis: ex r, s being Element of RAT+ st
( z9 = r + s & r < x9 & s < y9 )
take {} ; ::_thesis: ex s being Element of RAT+ st
( z9 = {} + s & {} < x9 & s < y9 )
take t0 ; ::_thesis: ( z9 = {} + t0 & {} < x9 & t0 < y9 )
thus z9 = {} + t0 by A4, A7; ::_thesis: ( {} < x9 & t0 < y9 )
{} <=' x9 by ARYTM_3:64;
hence {} < x9 by A2, ARYTM_3:68; ::_thesis: t0 < y9
thus t0 < y9 by A6, ARYTM_3:68; ::_thesis: verum
end;
supposeA8: r0 <> {} ; ::_thesis: ex r, s being Element of RAT+ st
( z9 = r + s & r < x9 & s < y9 )
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 ; ::_thesis: ex s being Element of RAT+ st
( z9 = r1 + s & r1 < x9 & s < y9 )
take t2 ; ::_thesis: ( z9 = r1 + t2 & r1 < x9 & t2 < y9 )
thus z9 = r1 + t2 by A11; ::_thesis: ( r1 < x9 & t2 < y9 )
r1 < r0 by A13, ARYTM_3:68;
hence r1 < x9 by A5, ARYTM_3:69; ::_thesis: t2 < y9
thus t2 < y9 by A10, A12, ARYTM_3:69; ::_thesis: verum
end;
end;
end;
Lm47: for x, y being Element of REAL+ st x in RAT+ & y in RAT+ holds
ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x + y = x9 + y9 )
proof
let x, y be Element of REAL+ ; ::_thesis: ( x in RAT+ & y in RAT+ implies ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x + y = x9 + y9 ) )
assume that
A1: x in RAT+ and
A2: y in RAT+ ; ::_thesis: ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x + y = x9 + y9 )
percases ( x = {} or y = {} or ( y <> {} & x <> {} ) ) ;
supposeA3: x = {} ; ::_thesis: ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x + y = x9 + y9 )
reconsider y9 = y as Element of RAT+ by A2;
take {} ; ::_thesis: ex y9 being Element of RAT+ st
( x = {} & y = y9 & x + y = {} + y9 )
take y9 ; ::_thesis: ( x = {} & y = y9 & x + y = {} + y9 )
thus x = {} by A3; ::_thesis: ( y = y9 & x + y = {} + y9 )
thus y = y9 ; ::_thesis: x + y = {} + y9
thus x + y = y by A3, Def8
.= {} + y9 by ARYTM_3:50 ; ::_thesis: verum
end;
supposeA4: y = {} ; ::_thesis: ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x + y = x9 + y9 )
reconsider x9 = x as Element of RAT+ by A1;
take x9 ; ::_thesis: ex y9 being Element of RAT+ st
( x = x9 & y = y9 & x + y = x9 + y9 )
take {} ; ::_thesis: ( x = x9 & y = {} & x + y = x9 + {} )
thus x = x9 ; ::_thesis: ( y = {} & x + y = x9 + {} )
thus y = {} by A4; ::_thesis: x + y = x9 + {}
thus x + y = x by A4, Def8
.= x9 + {} by ARYTM_3:50 ; ::_thesis: verum
end;
supposeA5: ( y <> {} & x <> {} ) ; ::_thesis: ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x + y = x9 + y9 )
set A = DEDEKIND_CUT x;
set B = DEDEKIND_CUT y;
consider x9 being Element of RAT+ such that
A6: x = x9 and
A7: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < x9 } by A1, Def3;
consider y9 being Element of RAT+ such that
A8: y = y9 and
A9: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < y9 } by A2, Def3;
A10: for s being Element of RAT+ holds
( s in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s < x9 + y9 )
proof
let s2 be Element of RAT+ ; ::_thesis: ( s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s2 < x9 + y9 )
thus ( s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) implies s2 < x9 + y9 ) ::_thesis: ( s2 < x9 + y9 implies s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) )
proof
assume s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) ; ::_thesis: s2 < x9 + y9
then consider r1, s1 being Element of RAT+ such that
A11: s2 = r1 + s1 and
A12: r1 in DEDEKIND_CUT x and
A13: s1 in DEDEKIND_CUT y ;
ex s being Element of RAT+ st
( s = r1 & s < x9 ) by A7, A12;
then A14: r1 + s1 <=' x9 + s1 by ARYTM_3:76;
ex s being Element of RAT+ st
( s = s1 & s < y9 ) by A9, A13;
then x9 + s1 < x9 + y9 by ARYTM_3:76;
hence s2 < x9 + y9 by A11, A14, ARYTM_3:69; ::_thesis: verum
end;
assume s2 < x9 + y9 ; ::_thesis: s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y)
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 DEDEKIND_CUT y & t2 in DEDEKIND_CUT x ) by A7, A9, A16;
hence s2 in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) by A15; ::_thesis: verum
end;
then consider r being Element of RAT+ such that
A17: GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) = r and
A18: for s being Element of RAT+ holds
( s in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s < r ) by Def4;
A19: for s being Element of RAT+ holds
( s < x9 + y9 iff s < r )
proof
let s be Element of RAT+ ; ::_thesis: ( s < x9 + y9 iff s < r )
( s in (DEDEKIND_CUT x) + (DEDEKIND_CUT y) iff s < x9 + y9 ) by A10;
hence ( s < x9 + y9 iff s < r ) by A18; ::_thesis: verum
end;
take x9 ; ::_thesis: ex y9 being Element of RAT+ st
( x = x9 & y = y9 & x + y = x9 + y9 )
take y9 ; ::_thesis: ( x = x9 & y = y9 & x + y = x9 + y9 )
thus ( x = x9 & y = y9 ) by A6, A8; ::_thesis: x + y = x9 + y9
thus x + y = GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) by A5, Def8
.= x9 + y9 by A17, A19, Lm6 ; ::_thesis: verum
end;
end;
end;
theorem :: ARYTM_2:16
for x, y being Element of REAL+ st x in omega & y in omega holds
y + x in omega
proof
let x, y be Element of REAL+ ; ::_thesis: ( x in omega & y in omega implies y + x in omega )
assume A1: ( x in omega & y in omega ) ; ::_thesis: y + x 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 y + x in omega by A3, ORDINAL1:def_12; ::_thesis: verum
end;
theorem :: ARYTM_2:17
for A being Subset of REAL+ st {} in A & ( for x, y being Element of REAL+ st x in A & y = one holds
x + y in A ) holds
omega c= A
proof
let A be Subset of REAL+; ::_thesis: ( {} in A & ( for x, y being Element of REAL+ st x in A & y = one holds
x + y in A ) implies omega c= A )
defpred S1[ set ] means $1 in A;
assume that
A1: S1[ {} ] and
A2: for x, y being Element of REAL+ st x in A & y = one holds
x + y in A ; ::_thesis: omega c= A
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in omega or e in A )
assume e in omega ; ::_thesis: e in A
then reconsider a = e as natural Ordinal ;
A3: for a being natural Ordinal st S1[a] holds
S1[ succ a]
proof
one in RAT+ ;
then reconsider rone = one as Element of REAL+ by Th1;
let a be natural Ordinal; ::_thesis: ( S1[a] implies S1[ succ a] )
assume A4: a in A ; ::_thesis: S1[ succ 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 S1[ succ a] by A2, A4, A7; ::_thesis: verum
end;
S1[a] from ORDINAL2:sch_17(A1, A3);
hence e in A ; ::_thesis: verum
end;
theorem :: ARYTM_2:18
for x being Element of REAL+ st x in omega holds
for y being Element of REAL+ holds
( y in x iff ( y in omega & y <> x & y <=' x ) )
proof
let x be Element of REAL+ ; ::_thesis: ( x in omega implies for y being Element of REAL+ holds
( y in x iff ( y in omega & y <> x & y <=' x ) ) )
assume A1: x in omega ; ::_thesis: for y being Element of REAL+ holds
( y in x iff ( y in omega & y <> x & y <=' x ) )
then reconsider m = x as Element of omega ;
reconsider x9 = x as Element of RAT+ by A1, Lm5;
let y be Element of REAL+ ; ::_thesis: ( y in x iff ( y in omega & y <> x & y <=' x ) )
A2: x c= omega by A1, ORDINAL1:def_2;
hereby ::_thesis: ( y in omega & y <> x & y <=' x implies y in x )
assume A3: y in x ; ::_thesis: ( y in omega & y <> x & y <=' x )
then reconsider n = y as Element of omega by A2;
thus y in omega by A2, A3; ::_thesis: ( y <> x & y <=' x )
then reconsider y9 = y as Element of RAT+ by Lm5;
thus y <> x by A3; ::_thesis: y <=' x
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 = C as Element of omega by ORDINAL1:12;
C in omega ;
then reconsider z9 = C as Element of RAT+ by Lm5;
x9 = y9 + z9 by A4, Lm45;
then y9 <=' x9 by ARYTM_3:def_13;
hence y <=' x by Lm14; ::_thesis: verum
end;
assume A5: y in omega ; ::_thesis: ( not y <> x or not y <=' x or y in x )
then reconsider y9 = y as Element of RAT+ by Lm5;
reconsider n = y as Element of omega by A5;
assume A6: y <> x ; ::_thesis: ( not y <=' x or y in x )
assume y <=' x ; ::_thesis: y in x
then y9 <=' x9 by Lm14;
then consider z9 being Element of RAT+ such that
A7: y9 + z9 = x9 by ARYTM_3:def_13;
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, XBOOLE_0:def_8;
hence y in x by ORDINAL1:11; ::_thesis: verum
end;
theorem :: ARYTM_2:19
for x, y, z being Element of REAL+ st x = y + z holds
z <=' x
proof
let x, y, z be Element of REAL+ ; ::_thesis: ( x = y + z implies z <=' x )
{} in RAT+ ;
then reconsider zz = {} as Element of REAL+ by Th1;
assume A1: x = y + z ; ::_thesis: z <=' x
assume A2: not z <=' x ; ::_thesis: contradiction
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 contradiction by A2; ::_thesis: verum
end;
theorem :: ARYTM_2:20
( {} in REAL+ & one in REAL+ )
proof
( {} in RAT+ & one in RAT+ ) ;
hence ( {} in REAL+ & one in REAL+ ) by Th1; ::_thesis: verum
end;
theorem :: ARYTM_2:21
for x, y being Element of REAL+ st x in RAT+ & y in RAT+ holds
ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x *' y = x9 *' y9 )
proof
let x, y be Element of REAL+ ; ::_thesis: ( x in RAT+ & y in RAT+ implies ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x *' y = x9 *' y9 ) )
assume that
A1: x in RAT+ and
A2: y in RAT+ ; ::_thesis: ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x *' y = x9 *' y9 )
percases ( x = {} or y = {} or ( y <> {} & x <> {} ) ) ;
supposeA3: x = {} ; ::_thesis: ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x *' y = x9 *' y9 )
reconsider y9 = y as Element of RAT+ by A2;
take {} ; ::_thesis: ex y9 being Element of RAT+ st
( x = {} & y = y9 & x *' y = {} *' y9 )
take y9 ; ::_thesis: ( x = {} & y = y9 & x *' y = {} *' y9 )
thus x = {} by A3; ::_thesis: ( y = y9 & x *' y = {} *' y9 )
thus y = y9 ; ::_thesis: x *' y = {} *' y9
thus x *' y = {} by A3, Th4
.= {} *' y9 by ARYTM_3:48 ; ::_thesis: verum
end;
supposeA4: y = {} ; ::_thesis: ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x *' y = x9 *' y9 )
reconsider x9 = x as Element of RAT+ by A1;
take x9 ; ::_thesis: ex y9 being Element of RAT+ st
( x = x9 & y = y9 & x *' y = x9 *' y9 )
take {} ; ::_thesis: ( x = x9 & y = {} & x *' y = x9 *' {} )
thus x = x9 ; ::_thesis: ( y = {} & x *' y = x9 *' {} )
thus y = {} by A4; ::_thesis: x *' y = x9 *' {}
thus x *' y = {} by A4, Th4
.= x9 *' {} by ARYTM_3:48 ; ::_thesis: verum
end;
supposethat y <> {} and
A5: x <> {} ; ::_thesis: ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x *' y = x9 *' y9 )
consider y9 being Element of RAT+ such that
A6: y = y9 and
A7: DEDEKIND_CUT y = { s where s is Element of RAT+ : s < y9 } by A2, Def3;
set A = DEDEKIND_CUT x;
set B = DEDEKIND_CUT y;
consider x9 being Element of RAT+ such that
A8: x = x9 and
A9: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < x9 } by A1, Def3;
A10: for s being Element of RAT+ holds
( s in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) iff s < x9 *' y9 )
proof
let s2 be Element of RAT+ ; ::_thesis: ( s2 in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) iff s2 < x9 *' y9 )
thus ( s2 in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) implies s2 < x9 *' y9 ) ::_thesis: ( s2 < x9 *' y9 implies s2 in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) )
proof
assume s2 in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) ; ::_thesis: s2 < x9 *' y9
then consider r1, s1 being Element of RAT+ such that
A11: s2 = r1 *' s1 and
A12: r1 in DEDEKIND_CUT x and
A13: s1 in DEDEKIND_CUT y ;
ex s being Element of RAT+ st
( s = r1 & s < x9 ) by A9, A12;
then A14: r1 *' s1 <=' x9 *' s1 by ARYTM_3:82;
A15: ex s being Element of RAT+ 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 s2 < x9 *' y9 by A11, A14, ARYTM_3:69; ::_thesis: verum
end;
assume A17: s2 < x9 *' y9 ; ::_thesis: s2 in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y)
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__::_thesis:_not_t2_=_x9
assume t2 = x9 ; ::_thesis: contradiction
then t0 = t1 by A5, A8, A18, A22, ARYTM_3:56;
hence contradiction by A20; ::_thesis: verum
end;
then t2 < x9 by A23, ARYTM_3:68;
then A24: t2 in DEDEKIND_CUT x by A9;
t1 in DEDEKIND_CUT y by A7, A21;
hence s2 in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) by A22, A24; ::_thesis: verum
end;
then consider r being Element of RAT+ such that
A25: GLUED ((DEDEKIND_CUT x) *' (DEDEKIND_CUT y)) = r and
A26: for s being Element of RAT+ holds
( s in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) iff s < r ) by Def4;
take x9 ; ::_thesis: ex y9 being Element of RAT+ st
( x = x9 & y = y9 & x *' y = x9 *' y9 )
take y9 ; ::_thesis: ( x = x9 & y = y9 & x *' y = x9 *' y9 )
thus ( x = x9 & y = y9 ) by A8, A6; ::_thesis: x *' y = x9 *' y9
for s being Element of RAT+ holds
( s < x9 *' y9 iff s < r )
proof
let s be Element of RAT+ ; ::_thesis: ( s < x9 *' y9 iff s < r )
( s in (DEDEKIND_CUT x) *' (DEDEKIND_CUT y) iff s < x9 *' y9 ) by A10;
hence ( s < x9 *' y9 iff s < r ) by A26; ::_thesis: verum
end;
hence x *' y = x9 *' y9 by A25, Lm6; ::_thesis: verum
end;
end;
end;