let r, s be Real; for V being RealLinearSpace
for v being VECTOR of V
for L1, L2 being Linear_Combination of V
for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds
ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )
let V be RealLinearSpace; for v being VECTOR of V
for L1, L2 being Linear_Combination of V
for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds
ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )
let v be VECTOR of V; for L1, L2 being Linear_Combination of V
for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds
ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )
let L1, L2 be Linear_Combination of V; for p being Real st ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v holds
ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )
let p be Real; ( ((r * L1) + ((1 - r) * L2)) . v <= p & p <= ((s * L1) + ((1 - s) * L2)) . v implies ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) ) )
set rv = ((r * L1) + ((1 - r) * L2)) . v;
set sv = ((s * L1) + ((1 - s) * L2)) . v;
set v1 = L1 . v;
set v2 = L2 . v;
A1: ((r * L1) + ((1 - r) * L2)) . v =
((r * L1) . v) + (((1 - r) * L2) . v)
by RLVECT_2:def 10
.=
(r * (L1 . v)) + (((1 - r) * L2) . v)
by RLVECT_2:def 11
.=
(r * (L1 . v)) + ((1 - r) * (L2 . v))
by RLVECT_2:def 11
;
A2: ((s * L1) + ((1 - s) * L2)) . v =
((s * L1) . v) + (((1 - s) * L2) . v)
by RLVECT_2:def 10
.=
(s * (L1 . v)) + (((1 - s) * L2) . v)
by RLVECT_2:def 11
.=
(s * (L1 . v)) + ((1 - s) * (L2 . v))
by RLVECT_2:def 11
;
assume that
A3:
((r * L1) + ((1 - r) * L2)) . v <= p
and
A4:
p <= ((s * L1) + ((1 - s) * L2)) . v
; ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )
per cases
( ((r * L1) + ((1 - r) * L2)) . v = ((s * L1) + ((1 - s) * L2)) . v or ((r * L1) + ((1 - r) * L2)) . v <> ((s * L1) + ((1 - s) * L2)) . v )
;
suppose A5:
((r * L1) + ((1 - r) * L2)) . v = ((s * L1) + ((1 - s) * L2)) . v
;
ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )take
r
;
( ((r * L1) + ((1 - r) * L2)) . v = p & ( r <= s implies ( r <= r & r <= s ) ) & ( s <= r implies ( s <= r & r <= r ) ) )thus
(
((r * L1) + ((1 - r) * L2)) . v = p & (
r <= s implies (
r <= r &
r <= s ) ) & (
s <= r implies (
s <= r &
r <= r ) ) )
by A3, A4, A5, XXREAL_0:1;
verum end; suppose
((r * L1) + ((1 - r) * L2)) . v <> ((s * L1) + ((1 - s) * L2)) . v
;
ex rs being Real st
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )then A6:
(((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v) <> 0
;
set y =
(p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v));
set x =
((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v));
take rs =
(r * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) + (s * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))));
( ((rs * L1) + ((1 - rs) * L2)) . v = p & ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )A7:
(
(r * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) + (r * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) = r * ((((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) &
(s * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) + (s * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) = s * ((((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) )
;
A8:
(((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) =
(((((s * L1) + ((1 - s) * L2)) . v) - p) + (p - (((r * L1) + ((1 - r) * L2)) . v))) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))
by XCMPLX_1:62
.=
1
by A6, XCMPLX_1:60
;
A9:
p - (((r * L1) + ((1 - r) * L2)) . v) >= (((r * L1) + ((1 - r) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)
by A3, XREAL_1:9;
thus p =
(p * ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))
by A6, XCMPLX_1:89
.=
(((((r * L1) + ((1 - r) * L2)) . v) * ((((s * L1) + ((1 - s) * L2)) . v) - p)) + ((((s * L1) + ((1 - s) * L2)) . v) * (p - (((r * L1) + ((1 - r) * L2)) . v)))) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))
.=
(((((r * L1) + ((1 - r) * L2)) . v) * ((((s * L1) + ((1 - s) * L2)) . v) - p)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + (((((s * L1) + ((1 - s) * L2)) . v) * (p - (((r * L1) + ((1 - r) * L2)) . v))) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))
by XCMPLX_1:62
.=
(((((r * L1) + ((1 - r) * L2)) . v) * ((((s * L1) + ((1 - s) * L2)) . v) - p)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + (((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) * (((s * L1) + ((1 - s) * L2)) . v))
by XCMPLX_1:74
.=
((((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) * ((r * (L1 . v)) + ((1 - r) * (L2 . v)))) + (((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) * ((s * (L1 . v)) + ((1 - s) * (L2 . v))))
by A1, A2, XCMPLX_1:74
.=
((rs * (L1 . v)) + (((((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) + ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))) * (L2 . v))) - (rs * (L2 . v))
.=
((rs * (L1 . v)) + (1 * (L2 . v))) - (rs * (L2 . v))
by A8
.=
(rs * (L1 . v)) + ((1 - rs) * (L2 . v))
.=
(rs * (L1 . v)) + (((1 - rs) * L2) . v)
by RLVECT_2:def 11
.=
((rs * L1) . v) + (((1 - rs) * L2) . v)
by RLVECT_2:def 11
.=
((rs * L1) + ((1 - rs) * L2)) . v
by RLVECT_2:def 10
;
( ( r <= s implies ( r <= rs & rs <= s ) ) & ( s <= r implies ( s <= rs & rs <= r ) ) )A10:
(
(((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v) >= (((s * L1) + ((1 - s) * L2)) . v) - p &
(((s * L1) + ((1 - s) * L2)) . v) - p >= p - p )
by A3, A4, XREAL_1:9, XREAL_1:10;
hereby ( s <= r implies ( s <= rs & rs <= r ) )
assume
r <= s
;
( r <= rs & rs <= s )then
(
r * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) <= s * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) &
r * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) <= s * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) )
by A9, A10, XREAL_1:64;
hence
(
r <= rs &
rs <= s )
by A7, A8, XREAL_1:6;
verum
end; assume A11:
s <= r
;
( s <= rs & rs <= r )then A12:
r * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) >= s * (((((s * L1) + ((1 - s) * L2)) . v) - p) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))
by A10, XREAL_1:64;
(((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v) >= p - (((r * L1) + ((1 - r) * L2)) . v)
by A4, XREAL_1:9;
then
r * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v))) >= s * ((p - (((r * L1) + ((1 - r) * L2)) . v)) / ((((s * L1) + ((1 - s) * L2)) . v) - (((r * L1) + ((1 - r) * L2)) . v)))
by A9, A11, XREAL_1:64;
hence
(
s <= rs &
rs <= r )
by A7, A8, A12, XREAL_1:6;
verum end;