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
and
A3:
A <> B
; :: thesis: ex C being Element of DEDEKIND_CUTS st A + C = B
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 ) } ;
not B c= A
by A2, A3, XBOOLE_0:def 10;
then consider s1 being Element of RAT+ such that
A4:
s1 in B
and
A5:
not s1 in A
by SUBSET_1:7;
s1 + {} = s1
by ARYTM_3:92;
then A6:
{} in { 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 A4, A5;
{ 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+
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 A6;
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
x' being
Element of
RAT+ st
(
x' = t & ex
r,
s being
Element of
RAT+ st
( not
r in A &
s in B &
r + x' = s ) )
;
then consider r0,
s0 being
Element of
RAT+ such that A7:
not
r0 in A
and A8:
s0 in B
and A9:
r0 + t = s0
;
thus
for
s 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 A10:
s + p = t
by ARYTM_3:def 13;
A11:
p <=' t
by A10, ARYTM_3:85;
t <=' s0
by A9, ARYTM_3:85;
then
p <=' s0
by A11, ARYTM_3:74;
then consider q being
Element of
RAT+ such that A12:
p + q = s0
by ARYTM_3:def 13;
(r0 + s) + p = q + p
by A9, A10, A12, ARYTM_3:57;
then A13:
r0 + s = q
by ARYTM_3:69;
q in B
by A8, A12, Lm16, ARYTM_3:85;
hence
s in DIF
by A7, A13;
:: thesis: verum
end;
consider s1 being
Element of
RAT+ such that A14:
s1 in B
and A15:
s0 < s1
by A8, Lm7;
consider q being
Element of
RAT+ such that A16:
s0 + q = s1
by A15, ARYTM_3:def 13;
take
t + q
;
:: thesis: ( t + q in DIF & t < t + q )
A17:
r0 + (t + q) = s1
by A9, A16, ARYTM_3:57;
hence
t + q in DIF
by A7, A14;
:: thesis: t < t + q
A18:
t <=' t + q
by ARYTM_3:85;
t <> t + q
by A9, A15, A17;
hence
t < t + q
by A18, ARYTM_3:75;
:: thesis: verum
end;
then A19:
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:64;
then consider s2 being Element of RAT+ such that
A20:
not s2 in B
by SUBSET_1:49;
then
DIF <> RAT+
;
then reconsider DIF = DIF as Element of DEDEKIND_CUTS by A19, ZFMISC_1:64;
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= Bproof
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 A21:
e in B
;
:: thesis: e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) }
then reconsider y' =
e as
Element of
RAT+ ;
per cases
( y' in A or not y' in A )
;
suppose A23:
not
y' 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 A24:
s0 in B
and A25:
y' < s0
by A21, Lm7;
A26:
not
s0 in A
by A23, A25, Lm16;
set Z =
{ r where r is Element of RAT+ : ex x' being Element of RAT+ st
( not x' in A & x' + r = s0 ) } ;
A27:
s0 + {} = s0
by ARYTM_3:92;
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 x' being Element of RAT+ st
( not x' in A & x' + 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 x' being Element of RAT+ st
( not x' in A & x' + r = s0 ) } & r2 = s + t ) )
assume A28:
r2 < s0
;
:: thesis: ex s, t being Element of RAT+ st
( s in A & t in { r where r is Element of RAT+ : ex x' being Element of RAT+ st
( not x' in A & x' + r = s0 ) } & r2 = s + t )
then A29:
(
r2 <=' s0 &
r2 <> s0 )
;
per cases
( r2 in A or not r2 in A )
;
suppose A31:
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 x' being Element of RAT+ st
( not x' in A & x' + r = s0 ) } & r2 = s + t )consider q being
Element of
RAT+ such that A32:
r2 + q = s0
by A28, ARYTM_3:def 13;
q <> {}
by A29, A32, ARYTM_3:92;
then consider n being
Element of
RAT+ such that A33:
n in omega
and A34:
s0 <=' n *' q
by ARYTM_3:103;
defpred S1[
Element of
RAT+ ]
means $1
*' q in A;
A35:
not
S1[
n]
by A26, A34, Lm16;
consider y0 being
Element of
RAT+ such that A36:
y0 in A
by A1, SUBSET_1:10;
{} *' q = {}
by ARYTM_3:54;
then A37:
S1[
{} ]
by A36, Lm17;
consider n0 being
Element of
RAT+ such that
n0 in omega
and A38:
S1[
n0]
and A39:
not
S1[
n0 + one ]
from ARYTM_3:sch 1(Lm32, Lm33, A33, A37, A35);
A40:
(n0 + one ) *' q =
(n0 *' q) + (one *' q)
by ARYTM_3:63
.=
(n0 *' q) + q
by ARYTM_3:59
;
n0 *' q <=' r2
by A31, A38, Lm16;
then
(n0 *' q) + q <=' s0
by A32, ARYTM_3:83;
then consider t being
Element of
RAT+ such that A41:
((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 x' being Element of RAT+ st
( not x' in A & x' + r = s0 ) } & r2 = (n0 *' q) + t )take
t
;
:: thesis: ( n0 *' q in A & t in { r where r is Element of RAT+ : ex x' being Element of RAT+ st
( not x' in A & x' + r = s0 ) } & r2 = (n0 *' q) + t )thus
n0 *' q in A
by A38;
:: thesis: ( t in { r where r is Element of RAT+ : ex x' being Element of RAT+ st
( not x' in A & x' + r = s0 ) } & r2 = (n0 *' q) + t )thus
t in { r where r is Element of RAT+ : ex x' being Element of RAT+ st
( not x' in A & x' + r = s0 ) }
by A39, A40, A41;
:: thesis: r2 = (n0 *' q) + t
((n0 *' q) + t) + q = r2 + q
by A32, A41, ARYTM_3:57;
hence
r2 = (n0 *' q) + t
by ARYTM_3:69;
:: thesis: verum end;
end; then consider s,
t being
Element of
RAT+ such that A42:
s in A
and A43:
t in { r where r is Element of RAT+ : ex x' being Element of RAT+ st
( not x' in A & x' + r = s0 ) }
and A44:
y' = s + t
by A25;
ex
r being
Element of
RAT+ st
(
t = r & ex
x' being
Element of
RAT+ st
( not
x' in A &
x' + r = s0 ) )
by A43;
then
t in DIF
by A24;
hence
e in { (r + t) where r, t is Element of RAT+ : ( r in A & t in DIF ) }
by A42, A44;
:: thesis: verum 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 A45:
e = s3 + t3
and A46:
s3 in A
and A47:
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 A47;
then consider r4,
s4 being
Element of
RAT+ such that A48:
not
r4 in A
and A49:
s4 in B
and A50:
r4 + t3 = s4
;
s3 <=' r4
by A46, A48, Lm16;
then
s3 + t3 <=' s4
by A50, ARYTM_3:83;
hence
e in B
by A45, A49, Lm16;
:: thesis: verum
end;
hence
A + DIF = B
; :: thesis: verum