let a, b be Element of REAL ; not (0,one) --> (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,one) --> (a,b);
A1:
now not (0,one) --> (a,b) in [:{{}},REAL+:]
(
0,
one)
--> (
a,
b)
= {[0,a],[one,b]}
by FUNCT_4:67;
then A2:
[one,b] in (
0,
one)
--> (
a,
b)
by TARSKI:def 2;
assume
(
0,
one)
--> (
a,
b)
in [:{{}},REAL+:]
;
contradictionthen consider x,
y being
object such that A3:
x in {{}}
and
y in REAL+
and A4:
(
0,
one)
--> (
a,
b)
= [x,y]
by ZFMISC_1:84;
A5:
x = 0
by A3, TARSKI:def 1;
end;
A6:
(0,one) --> (a,b) = {[0,a],[one,b]}
by FUNCT_4:67;
now not (0,one) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_coprime & j <> {} ) } assume
(
0,
one)
--> (
a,
b)
in { [i,j] where i, j is Element of NAT : ( i,j are_coprime & j <> {} ) }
;
contradictionthen consider i,
j being
Element of
NAT such that A7:
(
0,
one)
--> (
a,
b)
= [i,j]
and
i,
j are_coprime
and
j <> {}
;
A8:
(
{i} in (
0,
one)
--> (
a,
b) &
{i,j} in (
0,
one)
--> (
a,
b) )
by A7, TARSKI:def 2;
A9:
now not i = jassume
i = j
;
contradictionthen
{i} = {i,j}
by ENUMSET1:29;
then A10:
[i,j] = {{i}}
by ENUMSET1:29;
then
[one,b] in {{i}}
by A6, A7, TARSKI:def 2;
then A11:
[one,b] = {i}
by TARSKI:def 1;
[0,a] in {{i}}
by A6, A7, A10, TARSKI:def 2;
then
[0,a] = {i}
by TARSKI:def 1;
hence
contradiction
by A11, XTUPLE_0:1;
verum end; per cases
( ( {i,j} = [0,a] & {i} = [0,a] ) or ( {i,j} = [0,a] & {i} = [one,b] ) or ( {i,j} = [one,b] & {i} = [0,a] ) or ( {i,j} = [one,b] & {i} = [one,b] ) )
by A6, A8, TARSKI:def 2;
end; end;
then A18:
not (0,one) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_coprime & j <> {} ) } \ { [k,one] where k is Element of NAT : verum }
;
for x, y being set holds not {[0,x],[one,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 A19:
{[0,x],[one,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 A20:
{[0,x],[one,y]} = A
and A21:
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;
(
[0,x] in A & ( for
r,
s being
Element of
RAT+ st
r in A &
s <=' r holds
s in A ) )
by A20, A21, TARSKI:def 2;
then consider r1,
r2,
r3 being
Element of
RAT+ such that A22:
r1 in A
and A23:
r2 in A
and A24:
(
r3 in A &
r1 <> r2 &
r2 <> r3 &
r3 <> r1 )
by ARYTM_3:75;
A25:
(
r2 = [0,x] or
r2 = [one,y] )
by A20, A23, TARSKI:def 2;
(
r1 = [0,x] or
r1 = [one,y] )
by A20, A22, TARSKI:def 2;
hence
contradiction
by A20, A24, A25, TARSKI:def 2;
verum
end;
then A26:
not (0,one) --> (a,b) in DEDEKIND_CUTS
by A6, ARYTM_2:def 1;
then
not (0,one) --> (a,b) in RAT+
by A18, XBOOLE_0:def 3;
then
not (0,one) --> (a,b) in REAL+
by A26, ARYTM_2:def 2, XBOOLE_0:def 3;
hence
not (0,one) --> (a,b) in REAL
by A1, XBOOLE_0:def 3; verum