let s1, s3, s4, l be Real; :: thesis: ( s1 <= s3 & s1 < s4 & 0 <= l & l <= 1 implies s1 <= ((1 - l) * s3) + (l * s4) )
assume that
A1: s1 <= s3 and
A2: s1 < s4 and
A3: 0 <= l and
A4: l <= 1 ; :: thesis: s1 <= ((1 - l) * s3) + (l * s4)
now :: thesis: s1 <= ((1 - l) * s3) + (l * s4)
per cases ( l = 0 or l = 1 or ( not l = 0 & not l = 1 ) ) ;
suppose l = 0 ; :: thesis: s1 <= ((1 - l) * s3) + (l * s4)
hence s1 <= ((1 - l) * s3) + (l * s4) by A1; :: thesis: verum
end;
suppose l = 1 ; :: thesis: s1 <= ((1 - l) * s3) + (l * s4)
hence s1 <= ((1 - l) * s3) + (l * s4) by A2; :: thesis: verum
end;
suppose A5: ( not l = 0 & not l = 1 ) ; :: thesis: s1 <= ((1 - l) * s3) + (l * s4)
then l < 1 by A4, XXREAL_0:1;
then 1 - l > 0 by XREAL_1:50;
then A6: (1 - l) * s1 <= (1 - l) * s3 by A1, XREAL_1:64;
A7: ((1 - l) * s1) + (l * s1) = 1 * s1 ;
l * s1 < l * s4 by A2, A3, A5, XREAL_1:68;
hence s1 <= ((1 - l) * s3) + (l * s4) by A6, A7, XREAL_1:8; :: thesis: verum
end;
end;
end;
hence s1 <= ((1 - l) * s3) + (l * s4) ; :: thesis: verum