let p1, p2, p be Point of (TOP-REAL 2); :: thesis: for a being Real st p in LSeg (p1,p2) & p1 `1 < a & p2 `1 < a holds
p `1 < a
let a be Real; :: thesis: ( p in LSeg (p1,p2) & p1 `1 < a & p2 `1 < a implies p `1 < a )
assume that
A1: p in LSeg (p1,p2) and
A2: p1 `1 < a and
A3: p2 `1 < a ; :: thesis: p `1 < a
consider r being Real such that
A4: p = ((1 - r) * p1) + (r * p2) and
A5: 0 <= r and
A6: r <= 1 by A1;
A7: p `1 = (((1 - r) * p1) `1) + ((r * p2) `1) by A4, TOPREAL3:2
.= (((1 - r) * p1) `1) + (r * (p2 `1)) by TOPREAL3:4
.= ((1 - r) * (p1 `1)) + (r * (p2 `1)) by TOPREAL3:4 ;
per cases ( 0 = r or 0 <> r ) ;
suppose 0 = r ; :: thesis: p `1 < a
then p = p1 + (0 * p2) by A4, RLVECT_1:def 8
.= p1 + (0. (TOP-REAL 2)) by RLVECT_1:10
.= p1 by RLVECT_1:4 ;
hence p `1 < a by A2; :: thesis: verum
end;
suppose A8: 0 <> r ; :: thesis: p `1 < a
A9: ((1 - r) * a) + (r * a) = a ;
1 - r >= 0 by A6, XREAL_1:48;
then A10: (1 - r) * (p1 `1) <= (1 - r) * a by A2, XREAL_1:64;
r * (p2 `1) < r * a by A3, A5, A8, XREAL_1:68;
hence p `1 < a by A7, A10, A9, XREAL_1:8; :: thesis: verum
end;
end;