let x, y be Real; :: thesis: ( 0 <= x & x < y implies ex s0 being Real st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y ) )
assume that
A1: 0 <= x and
A2: x < y ; :: thesis: ex s0 being Real st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y )
ex s0 being Real st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y )
proof
consider s being Real such that
A3: x < s and
A4: s < y by A2, XREAL_1:5;
now :: thesis: ( ( 0 = x & 0 < s & x < y / (1 + s) & y / (1 + s) < y ) or ( 0 < x & 0 < (s / x) - 1 & x < y / (1 + ((s / x) - 1)) & y / (1 + ((s / x) - 1)) < y ) )
per cases ( 0 = x or 0 < x ) by A1;
case A5: 0 = x ; :: thesis: ( 0 < s & x < y / (1 + s) & y / (1 + s) < y )
set s0 = s;
y < y * (1 + s) by A1, A3, A4, XREAL_1:29, XREAL_1:155;
hence ( 0 < s & x < y / (1 + s) & y / (1 + s) < y ) by A3, A4, A5, XREAL_1:83, XREAL_1:139; :: thesis: verum
end;
case A6: 0 < x ; :: thesis: ( 0 < (s / x) - 1 & x < y / (1 + ((s / x) - 1)) & y / (1 + ((s / x) - 1)) < y )
set s0 = (s / x) - 1;
A7: (1 + ((s / x) - 1)) " = 1 / (1 + ((s / x) - 1)) by XCMPLX_1:215;
then A8: s * ((1 + ((s / x) - 1)) ") = (s * 1) / (1 + ((s / x) - 1)) by XCMPLX_1:74;
(1 + ((s / x) - 1)) * x = (x / x) * s by XCMPLX_1:75;
then (1 + ((s / x) - 1)) * x = 1 * s by A6, XCMPLX_1:60;
then A9: (((1 + ((s / x) - 1)) ") * (1 + ((s / x) - 1))) * x = s * ((1 + ((s / x) - 1)) ") ;
0 < 1 + ((s / x) - 1) by A3, A6, XREAL_1:187;
then A10: ((1 + ((s / x) - 1)) ") * (1 + ((s / x) - 1)) = 1 by A7, XCMPLX_1:106;
A11: 1 < 1 + ((s / x) - 1) by A3, A6, XREAL_1:187;
then y < y * (1 + ((s / x) - 1)) by A1, A2, XREAL_1:155;
hence ( 0 < (s / x) - 1 & x < y / (1 + ((s / x) - 1)) & y / (1 + ((s / x) - 1)) < y ) by A4, A11, A9, A10, A8, XREAL_1:50, XREAL_1:74, XREAL_1:83; :: thesis: verum
end;
end;
end;
hence ex s0 being Real st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y ) ; :: thesis: verum
end;
hence ex s0 being Real st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y ) ; :: thesis: verum