let a, b, d be Real; ( 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)
; d = 0
set s = ((1 - d) * a) + (d * b);
assume
d <> 0
; 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; verum