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