let rone be Element of REAL+ ; ( rone = one implies for A being Element of DEDEKIND_CUTS st A <> {} holds
ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone )
assume A0:
rone = one
; for A being Element of DEDEKIND_CUTS st A <> {} holds
ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone
let A be Element of DEDEKIND_CUTS ; ( A <> {} implies ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone )
assume A1:
A <> {}
; ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT rone
per cases
( 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 <> {} }
;
ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT ronethen 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+
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 ) )
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 }
XBOOLE_0:def 10 { s where s is Element of RAT+ : s < r0 *' s0 } c= A *' B
let e be
object ;
TARSKI:def 3 ( 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 }
;
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;
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, A0;
hence
ex
B being
Element of
DEDEKIND_CUTS st
A *' B = DEDEKIND_CUT rone
by A4, A9, A0;
verum end; suppose A24:
not
A in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} }
;
ex B being Element of DEDEKIND_CUTS st A *' B = DEDEKIND_CUT roneset 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+
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+ ;
( 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
;
( ( 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
ex s being Element of RAT+ st
( s in B & r < s )
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
;
( s in B & r < s )
x99 *' s <=' one
by A35;
hence
s in B
by A33;
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;
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;
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
;
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+ ;
( r in A *' B iff r < one )
hereby ( r < one implies r in A *' B )
end;
assume A51:
r < one
;
r in A *' B
then A52:
r <> one
;
per cases
( r = {} or r <> {} )
;
suppose
r <> {}
;
r in A *' Bthen 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+
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 not n1 *' (x9 *' dr) in rAassume
n1 *' (x9 *' dr) in rA
;
contradictionthen 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;
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;
verum end; end;
end; then
DEDEKIND_CUT (GLUED (A *' B)) = DEDEKIND_CUT rone
by A0, Def4;
hence
A *' B = DEDEKIND_CUT rone
by Lm12;
verum end; end;