let n be Element of NAT ; :: thesis: 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); :: thesis: ( p in LSeg p1,p2 implies ( |.(p - p1).| <= |.(p1 - p2).| & |.(p - p2).| <= |.(p1 - p2).| ) )
assume A1: p in LSeg p1,p2 ; :: thesis: ( |.(p - p1).| <= |.(p1 - p2).| & |.(p - p2).| <= |.(p1 - p2).| )
then consider r being Real such that
A2: ( 0 <= r & r <= 1 & p = ((1 - r) * p1) + (r * p2) ) by Th52;
p - p1 = (((1 - r) * p1) - p1) + (r * p2) by A2, 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 A3: |.(p1 - p2).| - |.(p - p1).| = (1 - r) * |.(p1 - p2).| ;
0 <= 1 - r by A2, XREAL_1:50;
then A4: |.(p1 - p2).| - |.(p - p1).| >= 0 by A3;
consider r being Real such that
A5: ( 0 <= r & r <= 1 & p = ((1 - r) * p2) + (r * p1) ) by A1, Th52;
p - p2 = (((1 - r) * p2) + (- p2)) + (r * p1) by A5, 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 A5, ABSVALUE:def 1 ;
then A6: |.(p1 - p2).| - |.(p - p2).| = (1 - r) * |.(p1 - p2).| ;
0 <= 1 - r by A5, XREAL_1:50;
then |.(p1 - p2).| - |.(p - p2).| >= 0 by A6;
hence ( |.(p - p1).| <= |.(p1 - p2).| & |.(p - p2).| <= |.(p1 - p2).| ) by A4, XREAL_1:51; :: thesis: verum