let t, r1, r2 be Real; ( r1 <= r2 implies ( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) ) )
assume A1:
r1 <= r2
; ( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) )
per cases
( r1 = r2 or r1 < r2 )
by A1, XXREAL_0:1;
suppose A6:
r1 < r2
;
( t in [.r1,r2.] iff ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) )hereby ( ex s1 being Real st
( 0 <= s1 & s1 <= 1 & t = (s1 * r1) + ((1 - s1) * r2) ) implies t in [.r1,r2.] )
end; given s1 being
Real such that A9:
0 <= s1
and A10:
s1 <= 1
and A11:
t = (s1 * r1) + ((1 - s1) * r2)
;
t in [.r1,r2.]A12:
(s1 * r2) + ((1 - s1) * r2) = 1
* r2
;
1
- s1 >= 0
by A10, XREAL_1:48;
then A13:
(1 - s1) * r1 <= (1 - s1) * r2
by A6, XREAL_1:64;
s1 * r1 <= s1 * r2
by A6, A9, XREAL_1:64;
then A14:
t <= r2
by A11, A12, XREAL_1:6;
(s1 * r1) + ((1 - s1) * r1) = 1
* r1
;
then
r1 <= t
by A11, A13, XREAL_1:6;
hence
t in [.r1,r2.]
by A14, XXREAL_1:1;
verum end; end;