let a, b be Element of REAL ; not 0 ,1 --> a,b in REAL
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 f = 0 ,1 --> a,b;
A1:
now
0 ,1
--> a,
b = {[0 ,a],[1,b]}
by FUNCT_4:71;
then A2:
[1,b] in 0 ,1
--> a,
b
by TARSKI:def 2;
assume
0 ,1
--> a,
b in [:{{} },REAL+ :]
;
contradictionthen consider x,
y being
set such that A3:
x in {{} }
and
y in REAL+
and A4:
0 ,1
--> a,
b = [x,y]
by ZFMISC_1:103;
x = 0
by A3, TARSKI:def 1;
then
0 ,1
--> a,
b = {{0 ,y},{0 }}
by A4, TARSKI:def 5;
then A5:
(
[1,b] = {0 } or
[1,b] = {0 ,y} )
by A2, TARSKI:def 2;
end;
A6:
0 ,1 --> a,b = {[0 ,a],[1,b]}
by FUNCT_4:71;
now assume
0 ,1
--> a,
b in { [i,j] where i, j is Element of NAT : ( i,j are_relative_prime & j <> {} ) }
;
contradictionthen consider i,
j being
Element of
NAT such that A7:
0 ,1
--> a,
b = [i,j]
and
i,
j are_relative_prime
and
j <> {}
;
A8:
0 ,1
--> a,
b = {{i,j},{i}}
by A7, TARSKI:def 5;
then A9:
(
{i} in 0 ,1
--> a,
b &
{i,j} in 0 ,1
--> a,
b )
by TARSKI:def 2;
A10:
now assume
i = j
;
contradictionthen
{i} = {i,j}
by ENUMSET1:69;
then A11:
[i,j] = {{i}}
by A7, A8, ENUMSET1:69;
then
[1,b] in {{i}}
by A6, A7, TARSKI:def 2;
then A12:
[1,b] = {i}
by TARSKI:def 1;
[0 ,a] in {{i}}
by A6, A7, A11, TARSKI:def 2;
then
[0 ,a] = {i}
by TARSKI:def 1;
hence
contradiction
by A12, ZFMISC_1:33;
verum end; A13:
[1,b] = {{1,b},{1}}
by TARSKI:def 5;
A14:
[0 ,a] = {{0 ,a},{0 }}
by TARSKI:def 5;
per cases
( ( {i,j} = [0 ,a] & {i} = [0 ,a] ) or ( {i,j} = [0 ,a] & {i} = [1,b] ) or ( {i,j} = [1,b] & {i} = [0 ,a] ) or ( {i,j} = [1,b] & {i} = [1,b] ) )
by A6, A9, TARSKI:def 2;
end; end;
then A21:
not 0 ,1 --> a,b in { [i,j] where i, j is Element of NAT : ( i,j are_relative_prime & j <> {} ) } \ { [k,1] where k is Element of NAT : verum }
;
for x, y being set holds not {[0 ,x],[1,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 A22:
{[0 ,x],[1,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 ) ) }
;
contradiction
consider A being
Subset of
RAT+ such that A23:
{[0 ,x],[1,y]} = A
and A24:
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 A22;
(
[0 ,x] in A & ( for
r,
s being
Element of
RAT+ st
r in A &
s <=' r holds
s in A ) )
by A23, A24, TARSKI:def 2;
then consider r1,
r2,
r3 being
Element of
RAT+ such that A25:
r1 in A
and A26:
r2 in A
and A27:
(
r3 in A &
r1 <> r2 &
r2 <> r3 &
r3 <> r1 )
by ARYTM_3:82;
A28:
(
r2 = [0 ,x] or
r2 = [1,y] )
by A23, A26, TARSKI:def 2;
(
r1 = [0 ,x] or
r1 = [1,y] )
by A23, A25, TARSKI:def 2;
hence
contradiction
by A23, A27, A28, TARSKI:def 2;
verum
end;
then A29:
not 0 ,1 --> a,b in DEDEKIND_CUTS
by A6, ARYTM_2:def 1;
then
not 0 ,1 --> a,b in RAT+
by A21, XBOOLE_0:def 3;
then
not 0 ,1 --> a,b in REAL+
by A29, ARYTM_2:def 2, XBOOLE_0:def 3;
hence
not 0 ,1 --> a,b in REAL
by A1, NUMBERS:def 1, XBOOLE_0:def 3; verum