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;
then consider s1 being Element of RAT+ such that
A3: ( s1 in B & not s1 in A ) ;
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 object ; :: 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 ;
A10: t <=' s0 by A8;
p <=' t by A9;
then p <=' s0 by A10, ARYTM_3:67;
then consider q being Element of RAT+ such that
A11: p + q = s0 ;
(r0 + s) + p = q + p by A8, A9, A11, ARYTM_3:51;
then A12: r0 + s = q by ARYTM_3:62;
q in B by A7, A11, Lm16, ARYTM_3:77;
hence 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;
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 object ; :: 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+ ;
per cases ( y9 in A or not y9 in A ) ;
suppose A20: 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;
suppose A21: 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 ;
per cases ( r2 in A or not r2 in A ) ;
suppose A28: 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;
suppose A29: 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 ;
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 object ; :: 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