let a, b be Element of REAL ; :: thesis: 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 :: thesis: not (0,one) --> (a,b) in
(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 ; :: thesis: contradiction
then 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 ;
per cases = or {{one,b},} = {0,y} ) by ;
suppose {{one,b},} = ; :: thesis: contradiction
end;
suppose {{one,b},} = {0,y} ; :: thesis: contradiction
end;
end;
end;
A6: (0,one) --> (a,b) = {[0,a],[one,b]} by FUNCT_4:67;
now :: thesis: 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 <> {} ) } ; :: thesis: contradiction
then 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 ;
A9: now :: thesis: not i = jend;
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 ;
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 ) )
}
; :: thesis: 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 ;
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 ;
( r1 = [0,x] or r1 = [one,y] ) by ;
hence contradiction by A20, A24, A25, TARSKI:def 2; :: thesis: verum
end;
then A26: not (0,one) --> (a,b) in DEDEKIND_CUTS by ;
now :: thesis: not (0,one) --> (a,b) in omega
assume (0,one) --> (a,b) in omega ; :: thesis: contradiction
then {} in (0,one) --> (a,b) by ORDINAL3:8;
hence contradiction by A6, TARSKI:def 2; :: thesis: verum
end;
then not (0,one) --> (a,b) in RAT+ by ;
then not (0,one) --> (a,b) in REAL+ by ;
hence not (0,one) --> (a,b) in REAL by ; :: thesis: verum