let N be Nat; for p, p1, p2 being Point of (TOP-REAL N) st p in LSeg (p1,p2) holds
( |.(p - p1).| <= |.(p1 - p2).| & |.(p - p2).| <= |.(p1 - p2).| )
let p, p1, p2 be Point of (TOP-REAL N); ( p in LSeg (p1,p2) implies ( |.(p - p1).| <= |.(p1 - p2).| & |.(p - p2).| <= |.(p1 - p2).| ) )
assume A1:
p in LSeg (p1,p2)
; ( |.(p - p1).| <= |.(p1 - p2).| & |.(p - p2).| <= |.(p1 - p2).| )
then consider r being Real such that
A2:
0 <= r
and
A3:
r <= 1
and
A4:
p = ((1 - r) * p1) + (r * p2)
by RLTOPSP1:76;
A5:
0 <= 1 - r
by A3, XREAL_1:48;
p - p1 =
(((1 - r) * p1) - p1) + (r * p2)
by A4, RLVECT_1:def 3
.=
(((1 - r) * p1) - (1 * p1)) + (r * p2)
by RLVECT_1:def 8
.=
(((1 + (- r)) - 1) * p1) + (r * p2)
by RLVECT_1:35
.=
(r * p2) + (- (r * p1))
by RLVECT_1:79
.=
(r * p2) + (r * (- p1))
by RLVECT_1:25
.=
r * (p2 - p1)
by RLVECT_1:def 5
;
then |.(p - p1).| =
|.r.| * |.(p2 - p1).|
by TOPRNS_1:7
.=
|.r.| * |.(p1 - p2).|
by TOPRNS_1:27
.=
r * |.(p1 - p2).|
by A2, ABSVALUE:def 1
;
then A6:
|.(p1 - p2).| - |.(p - p1).| = (1 - r) * |.(p1 - p2).|
;
consider r being Real such that
A7:
0 <= r
and
A8:
r <= 1
and
A9:
p = ((1 - r) * p2) + (r * p1)
by A1, RLTOPSP1:76;
p - p2 =
(((1 - r) * p2) + (- p2)) + (r * p1)
by A9, RLVECT_1:def 3
.=
(((1 - r) * p2) - (1 * p2)) + (r * p1)
by RLVECT_1:def 8
.=
(((1 + (- r)) - 1) * p2) + (r * p1)
by RLVECT_1:35
.=
(r * p1) + (- (r * p2))
by RLVECT_1:79
.=
(r * p1) + (r * (- p2))
by RLVECT_1:25
.=
r * (p1 - p2)
by RLVECT_1:def 5
;
then |.(p - p2).| =
|.r.| * |.(p1 - p2).|
by TOPRNS_1:7
.=
r * |.(p1 - p2).|
by A7, ABSVALUE:def 1
;
then A10:
|.(p1 - p2).| - |.(p - p2).| = (1 - r) * |.(p1 - p2).|
;
0 <= 1 - r
by A8, XREAL_1:48;
hence
( |.(p - p1).| <= |.(p1 - p2).| & |.(p - p2).| <= |.(p1 - p2).| )
by A6, A5, A10, XREAL_1:49; verum