let n be Nat; :: thesis: for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds
LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2))
let p, p1, p2 be Point of (TOP-REAL n); :: thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) )
now :: thesis: ( p in LSeg (p1,p2) & p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) )
assume A1: p in LSeg (p1,p2) ; :: thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) )
then consider r being Real such that
A2: p = ((1 - r) * p1) + (r * p2) and
A3: 0 <= r and
A4: r <= 1 ;
now :: thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) )
per cases ( ( 0 <> r & r <> 1 ) or not 0 <> r or not r <> 1 ) ;
suppose A5: ( 0 <> r & r <> 1 ) ; :: thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) )
now :: thesis: for q being object st q in LSeg (p1,p2) holds
q in (LSeg (p1,p)) \/ (LSeg (p,p2))
let q be object ; :: thesis: ( q in LSeg (p1,p2) implies q in (LSeg (p1,p)) \/ (LSeg (p,p2)) )
assume q in LSeg (p1,p2) ; :: thesis: q in (LSeg (p1,p)) \/ (LSeg (p,p2))
then consider b being Real such that
A6: q = ((1 - b) * p1) + (b * p2) and
A7: 0 <= b and
A8: b <= 1 ;
now :: thesis: q in (LSeg (p1,p)) \/ (LSeg (p,p2))
per cases ( b <= r or not b <= r ) ;
suppose A9: b <= r ; :: thesis: q in (LSeg (p1,p)) \/ (LSeg (p,p2))
set x = b * (1 / r);
b * (1 / r) <= r * (1 / r) by A3, A9, XREAL_1:64;
then A10: b * (1 / r) <= 1 by A5, XCMPLX_1:106;
((1 - (b * (1 / r))) * p1) + ((b * (1 / r)) * p) = ((1 - (b * (1 / r))) * p1) + (((b * (1 / r)) * ((1 - r) * p1)) + ((b * (1 / r)) * (r * p2))) by A2, RLVECT_1:def 5
.= (((1 - (b * (1 / r))) * p1) + ((b * (1 / r)) * ((1 - r) * p1))) + ((b * (1 / r)) * (r * p2)) by RLVECT_1:def 3
.= (((1 - (b * (1 / r))) * p1) + (((b * (1 / r)) * (1 - r)) * p1)) + ((b * (1 / r)) * (r * p2)) by RLVECT_1:def 7
.= (((1 - (b * (1 / r))) * p1) + (((b * (1 / r)) * (1 - r)) * p1)) + (((b * (1 / r)) * r) * p2) by RLVECT_1:def 7
.= (((1 - (b * (1 / r))) + ((b * (1 / r)) * (1 - r))) * p1) + (((b * (1 / r)) * r) * p2) by RLVECT_1:def 6
.= ((1 - ((b * (1 / r)) * r)) * p1) + (b * p2) by A5, XCMPLX_1:109
.= q by A5, A6, XCMPLX_1:109 ;
then q in { (((1 - lambda) * p1) + (lambda * p)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A3, A7, A10;
hence q in (LSeg (p1,p)) \/ (LSeg (p,p2)) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose A11: not b <= r ; :: thesis: q in (LSeg (p1,p)) \/ (LSeg (p,p2))
set bp = 1 - b;
set rp = 1 - r;
set x = (1 - b) * (1 / (1 - r));
A12: 0 <> 1 - r by A5;
r - r = 0 ;
then A13: 0 <= 1 - r by A4, XREAL_1:9;
1 - b <= 1 - r by A11, XREAL_1:10;
then (1 - b) * (1 / (1 - r)) <= (1 - r) * (1 / (1 - r)) by A13, XREAL_1:64;
then A14: (1 - b) * (1 / (1 - r)) <= 1 by A12, XCMPLX_1:106;
A15: 0 <= 1 - b by A8, XREAL_1:48;
A16: 1 - 0 = 1 ;
((1 - ((1 - b) * (1 / (1 - r)))) * p2) + (((1 - b) * (1 / (1 - r))) * p) = ((1 - ((1 - b) * (1 / (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * ((1 - (1 - r)) * p2)) + (((1 - b) * (1 / (1 - r))) * ((1 - r) * p1))) by A2, RLVECT_1:def 5
.= (((1 - ((1 - b) * (1 / (1 - r)))) * p2) + (((1 - b) * (1 / (1 - r))) * ((1 - (1 - r)) * p2))) + (((1 - b) * (1 / (1 - r))) * ((1 - r) * p1)) by RLVECT_1:def 3
.= (((1 - ((1 - b) * (1 / (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * (1 - (1 - r))) * p2)) + (((1 - b) * (1 / (1 - r))) * ((1 - r) * p1)) by RLVECT_1:def 7
.= (((1 - ((1 - b) * (1 / (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * (1 - (1 - r))) * p2)) + ((((1 - b) * (1 / (1 - r))) * (1 - r)) * p1) by RLVECT_1:def 7
.= (((1 - ((1 - b) * (1 / (1 - r)))) + (((1 - b) * (1 / (1 - r))) * (1 - (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * (1 - r)) * p1) by RLVECT_1:def 6
.= ((1 - (((1 - b) * (1 / (1 - r))) * (1 - r))) * p2) + ((1 - b) * p1) by A5, A16, XCMPLX_1:109
.= ((1 - (1 - b)) * p2) + ((1 - b) * p1) by A12, XCMPLX_1:109
.= q by A6 ;
then q in { (((1 - lambda) * p2) + (lambda * p)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A15, A13, A14;
then q in LSeg (p,p2) by RLTOPSP1:def 2;
hence q in (LSeg (p1,p)) \/ (LSeg (p,p2)) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence q in (LSeg (p1,p)) \/ (LSeg (p,p2)) ; :: thesis: verum
end;
then A17: LSeg (p1,p2) c= (LSeg (p1,p)) \/ (LSeg (p,p2)) ;
A18: LSeg (p,p2) c= LSeg (p1,p2) by A1, Lm1;
LSeg (p1,p) c= LSeg (p1,p2) by A1, Lm1;
then (LSeg (p1,p)) \/ (LSeg (p,p2)) c= LSeg (p1,p2) by A18, XBOOLE_1:8;
hence ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) by A17; :: thesis: verum
end;
suppose A19: ( not 0 <> r or not r <> 1 ) ; :: thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) )
now :: thesis: LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2))
per cases ( r = 0 or r = 1 ) by A19;
suppose A20: r = 0 ; :: thesis: LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2))
A21: p in LSeg (p,p2) by RLTOPSP1:68;
A22: p = (1 * p1) + (0. (TOP-REAL n)) by A2, A20, RLVECT_1:10
.= p1 + (0. (TOP-REAL n)) by RLVECT_1:def 8
.= p1 by RLVECT_1:4 ;
then LSeg (p1,p) = {p} by RLTOPSP1:70;
then LSeg (p1,p) c= LSeg (p,p2) by A21, ZFMISC_1:31;
hence LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) by A22, XBOOLE_1:12; :: thesis: verum
end;
suppose A23: r = 1 ; :: thesis: LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2))
A24: p in LSeg (p1,p) by RLTOPSP1:68;
A25: p = (0. (TOP-REAL n)) + (1 * p2) by A2, A23, RLVECT_1:10
.= (0. (TOP-REAL n)) + p2 by RLVECT_1:def 8
.= p2 by RLVECT_1:4 ;
then LSeg (p,p2) = {p} by RLTOPSP1:70;
then LSeg (p,p2) c= LSeg (p1,p) by A24, ZFMISC_1:31;
hence LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) by A25, XBOOLE_1:12; :: thesis: verum
end;
end;
end;
hence ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) ; :: thesis: verum
end;
end;
end;
hence ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) ; :: thesis: verum
end;
hence ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) ; :: thesis: verum