let p, q be Point of (TOP-REAL 2); for r being Real st r <= 1 holds
dist (p,((r * p) + ((1 - r) * q))) = (1 - r) * (dist (p,q))
let r be Real; ( r <= 1 implies dist (p,((r * p) + ((1 - r) * q))) = (1 - r) * (dist (p,q)) )
assume
r <= 1
; dist (p,((r * p) + ((1 - r) * q))) = (1 - r) * (dist (p,q))
then
1 + r <= 1 + 1
by XREAL_1:6;
then
1 - r >= 1 - 1
by XREAL_1:21;
then A1:
|.(1 - r).| = 1 - r
by ABSVALUE:def 1;
thus dist (p,((r * p) + ((1 - r) * q))) =
dist (((r + (1 - r)) * p),((r * p) + ((1 - r) * q)))
by RLVECT_1:def 8
.=
dist (((r * p) + ((1 - r) * p)),((r * p) + ((1 - r) * q)))
by RLVECT_1:def 6
.=
dist (((1 - r) * p),((1 - r) * q))
by Th21
.=
(1 - r) * (dist (p,q))
by A1, Th26
; verum