let n be Element of 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 Th52;
A5:
0 <= 1 - r
by A3, XREAL_1:50;
p - p1 =
(((1 - r) * p1) - p1) + (r * p2)
by A4, EUCLID:30
.=
(((1 - r) * p1) - (1 * p1)) + (r * p2)
by EUCLID:33
.=
(((1 + (- r)) - 1) * p1) + (r * p2)
by EUCLID:54
.=
(r * p2) + (- (r * p1))
by EUCLID:44
.=
(r * p2) + (r * (- p1))
by EUCLID:44
.=
r * (p2 - p1)
by EUCLID:36
;
then |.(p - p1).| =
(abs r) * |.(p2 - p1).|
by TOPRNS_1:8
.=
(abs r) * |.(p1 - p2).|
by TOPRNS_1:28
.=
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, Th52;
p - p2 =
(((1 - r) * p2) + (- p2)) + (r * p1)
by A9, EUCLID:30
.=
(((1 - r) * p2) - (1 * p2)) + (r * p1)
by EUCLID:33
.=
(((1 + (- r)) - 1) * p2) + (r * p1)
by EUCLID:54
.=
(r * p1) + (- (r * p2))
by EUCLID:44
.=
(r * p1) + (r * (- p2))
by EUCLID:44
.=
r * (p1 - p2)
by EUCLID:36
;
then |.(p - p2).| =
(abs r) * |.(p1 - p2).|
by TOPRNS_1:8
.=
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:50;
hence
( |.(p - p1).| <= |.(p1 - p2).| & |.(p - p2).| <= |.(p1 - p2).| )
by A6, A5, A10, XREAL_1:51; verum