let a, b, d be Real; :: thesis: ( 0 <= d & d <= 1 & ((1 - d) * a) + (d * b) <= a & ((1 - d) * a) + (d * b) < b implies d = 0 )
assume that
A1: d >= 0 and
A2: d <= 1 and
A3: a >= ((1 - d) * a) + (d * b) and
A4: b > ((1 - d) * a) + (d * b) ; :: thesis: d = 0
set s = ((1 - d) * a) + (d * b);
assume d <> 0 ; :: thesis: contradiction
then A5: d * b > d * (((1 - d) * a) + (d * b)) by A1, A4, Lm13;
1 - d >= 0 by A2, Th48;
then A6: (1 - d) * a >= (1 - d) * (((1 - d) * a) + (d * b)) by A3, Lm12;
1 * (((1 - d) * a) + (d * b)) = ((1 - d) * (((1 - d) * a) + (d * b))) + (d * (((1 - d) * a) + (d * b))) ;
hence contradiction by A5, A6, Lm8; :: thesis: verum