let a, b, g1, M be Real; :: thesis: ( a < b & 0 < g1 & 0 < M implies ex r being Real st
( a < r & r < b & (b - r) * M < g1 ) )
assume that
A1: a < b and
A2: 0 < g1 and
A3: 0 < M ; :: thesis: ex r being Real st
( a < r & r < b & (b - r) * M < g1 )
set r3 = max (a,(b - (g1 / M)));
b - (g1 / M) < b by A2, A3, XREAL_1:44, XREAL_1:139;
then max (a,(b - (g1 / M))) < b by A1, XXREAL_0:16;
then consider q being Real such that
A4: max (a,(b - (g1 / M))) < q and
A5: q < b by XREAL_1:5;
reconsider r = q as Real ;
take r ; :: thesis: ( a < r & r < b & (b - r) * M < g1 )
b - (g1 / M) <= max (a,(b - (g1 / M))) by XXREAL_0:25;
then b - (g1 / M) < r by A4, XXREAL_0:2;
then (b - (g1 / M)) - (r - (g1 / M)) < r - (r - (g1 / M)) by XREAL_1:14;
then (b - r) * 1 < g1 / M ;
then ( a <= max (a,(b - (g1 / M))) & (b - r) * M < g1 / 1 ) by A3, XREAL_1:111, XXREAL_0:25;
hence ( a < r & r < b & (b - r) * M < g1 ) by A4, A5, XXREAL_0:2; :: thesis: verum