let r be Real; :: thesis: for N being Nat
for p1, p2 being Point of (TOP-REAL N)
for u being Point of (Euclid N) st p1 in Ball (u,r) & p2 in Ball (u,r) holds
LSeg (p1,p2) c= Ball (u,r)
let N be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL N)
for u being Point of (Euclid N) st p1 in Ball (u,r) & p2 in Ball (u,r) holds
LSeg (p1,p2) c= Ball (u,r)
let p1, p2 be Point of (TOP-REAL N); :: thesis: for u being Point of (Euclid N) st p1 in Ball (u,r) & p2 in Ball (u,r) holds
LSeg (p1,p2) c= Ball (u,r)
let u be Point of (Euclid N); :: thesis: ( p1 in Ball (u,r) & p2 in Ball (u,r) implies LSeg (p1,p2) c= Ball (u,r) )
assume that
A1: p1 in Ball (u,r) and
A2: p2 in Ball (u,r) ; :: thesis: LSeg (p1,p2) c= Ball (u,r)
reconsider p9 = p1 as Point of (Euclid N) by A1;
A3: dist (p9,u) < r by A1, METRIC_1:11;
thus LSeg (p1,p2) c= Ball (u,r) :: thesis: verum
proof
p2 in { u4 where u4 is Point of (Euclid N) : dist (u,u4) < r } by A2, METRIC_1:17;
then A4: ex u4 being Point of (Euclid N) st
( u4 = p2 & dist (u,u4) < r ) ;
reconsider q29 = u as Element of REAL N ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in LSeg (p1,p2) or a in Ball (u,r) )
reconsider q2 = q29 as Point of (TOP-REAL N) by EUCLID:22;
assume a in LSeg (p1,p2) ; :: thesis: a in Ball (u,r)
then consider lambda being Real such that
A5: ((1 - lambda) * p1) + (lambda * p2) = a and
A6: 0 <= lambda and
A7: lambda <= 1 ;
A8: lambda = |.lambda.| by A6, ABSVALUE:def 1;
set p = ((1 - lambda) * p1) + (lambda * p2);
reconsider p9 = ((1 - lambda) * p1) + (lambda * p2), p19 = p1, p29 = p2 as Element of REAL N by EUCLID:22;
reconsider u5 = ((1 - lambda) * p1) + (lambda * p2) as Point of (Euclid N) by EUCLID:22;
A9: ( (Pitag_dist N) . (q29,p9) = |.(q29 - p9).| & (Pitag_dist N) . (u,u5) = dist (u,u5) ) by EUCLID:def 6, METRIC_1:def 1;
(Pitag_dist N) . (q29,p29) = |.(q29 - p29).| by EUCLID:def 6;
then A10: |.(q29 + (- p29)).| < r by A4, METRIC_1:def 1;
A11: 0 <= 1 - lambda by A7, XREAL_1:48;
then A12: 1 - lambda = |.(1 - lambda).| by ABSVALUE:def 1;
consider u3 being Point of (Euclid N) such that
A13: u3 = p1 and
A14: dist (u,u3) < r by A3;
A15: (Pitag_dist N) . (q29,p19) = |.(q29 - p19).| by EUCLID:def 6;
then A16: dist (u,u3) = |.(q29 - p19).| by A13, METRIC_1:def 1;
( ( |.(1 - lambda).| * |.(q29 + (- p19)).| < (1 - lambda) * r & |.lambda.| * |.(q29 + (- p29)).| <= lambda * r ) or ( |.(1 - lambda).| * |.(q29 + (- p19)).| <= (1 - lambda) * r & |.lambda.| * |.(q29 + (- p29)).| < lambda * r ) )
proof
per cases ( lambda = 0 or lambda > 0 ) by A6;
suppose lambda = 0 ; :: thesis: ( ( |.(1 - lambda).| * |.(q29 + (- p19)).| < (1 - lambda) * r & |.lambda.| * |.(q29 + (- p29)).| <= lambda * r ) or ( |.(1 - lambda).| * |.(q29 + (- p19)).| <= (1 - lambda) * r & |.lambda.| * |.(q29 + (- p29)).| < lambda * r ) )
hence ( ( |.(1 - lambda).| * |.(q29 + (- p19)).| < (1 - lambda) * r & |.lambda.| * |.(q29 + (- p29)).| <= lambda * r ) or ( |.(1 - lambda).| * |.(q29 + (- p19)).| <= (1 - lambda) * r & |.lambda.| * |.(q29 + (- p29)).| < lambda * r ) ) by A13, A14, A15, A12, A8, METRIC_1:def 1; :: thesis: verum
end;
suppose lambda > 0 ; :: thesis: ( ( |.(1 - lambda).| * |.(q29 + (- p19)).| < (1 - lambda) * r & |.lambda.| * |.(q29 + (- p29)).| <= lambda * r ) or ( |.(1 - lambda).| * |.(q29 + (- p19)).| <= (1 - lambda) * r & |.lambda.| * |.(q29 + (- p29)).| < lambda * r ) )
hence ( ( |.(1 - lambda).| * |.(q29 + (- p19)).| < (1 - lambda) * r & |.lambda.| * |.(q29 + (- p29)).| <= lambda * r ) or ( |.(1 - lambda).| * |.(q29 + (- p19)).| <= (1 - lambda) * r & |.lambda.| * |.(q29 + (- p29)).| < lambda * r ) ) by A14, A16, A10, A11, A12, A8, XREAL_1:64, XREAL_1:68; :: thesis: verum
end;
end;
end;
then A17: (|.(1 - lambda).| * |.(q29 + (- p19)).|) + (|.lambda.| * |.(q29 + (- p29)).|) < ((1 - lambda) * r) + (lambda * r) by XREAL_1:8;
q29 - p19 = q2 - p1 by EUCLID:69;
then A18: ( q29 - p9 = q2 - (((1 - lambda) * p1) + (lambda * p2)) & (1 - lambda) * (q29 - p19) = (1 - lambda) * (q2 - p1) ) by EUCLID:65, EUCLID:69;
q29 - p29 = q2 - p2 by EUCLID:69;
then A19: lambda * (q29 - p29) = lambda * (q2 - p2) by EUCLID:65;
q2 - (((1 - lambda) * p1) + (lambda * p2)) = (((1 - lambda) + lambda) * q2) - (((1 - lambda) * p1) + (lambda * p2)) by RLVECT_1:def 8
.= (((1 - lambda) * q2) + (lambda * q2)) - (((1 - lambda) * p1) + (lambda * p2)) by RLVECT_1:def 6
.= (((1 - lambda) * q2) + (lambda * q2)) + (- (((1 - lambda) * p1) + (lambda * p2)))
.= (((1 - lambda) * q2) + (lambda * q2)) + ((- ((1 - lambda) * p1)) - (lambda * p2)) by RLVECT_1:30
.= ((((1 - lambda) * q2) + (lambda * q2)) + (- ((1 - lambda) * p1))) + (- (lambda * p2)) by RLVECT_1:def 3
.= ((((1 - lambda) * q2) + (- ((1 - lambda) * p1))) + (lambda * q2)) + (- (lambda * p2)) by RLVECT_1:def 3
.= ((((1 - lambda) * q2) + ((1 - lambda) * (- p1))) + (lambda * q2)) + (- (lambda * p2)) by RLVECT_1:25
.= (((1 - lambda) * (q2 + (- p1))) + (lambda * q2)) + (- (lambda * p2)) by RLVECT_1:def 5
.= ((1 - lambda) * (q2 + (- p1))) + ((lambda * q2) + (- (lambda * p2))) by RLVECT_1:def 3
.= ((1 - lambda) * (q2 + (- p1))) + ((lambda * q2) + (lambda * (- p2))) by RLVECT_1:25
.= ((1 - lambda) * (q2 - p1)) + (lambda * (q2 - p2)) by RLVECT_1:def 5 ;
then q29 - p9 = ((1 - lambda) * (q29 - p19)) + (lambda * (q29 - p29)) by A18, A19, EUCLID:64;
then A20: |.(q29 - p9).| <= |.((1 - lambda) * (q29 - p19)).| + |.(lambda * (q29 - p29)).| by EUCLID:12;
|.((1 - lambda) * (q29 + (- p19))).| + |.(lambda * (q29 + (- p29))).| = (|.(1 - lambda).| * |.(q29 + (- p19)).|) + |.(lambda * (q29 + (- p29))).| by EUCLID:11
.= (|.(1 - lambda).| * |.(q29 + (- p19)).|) + (|.lambda.| * |.(q29 + (- p29)).|) by EUCLID:11 ;
then |.(q29 - p9).| < r by A20, A17, XXREAL_0:2;
then a in { u6 where u6 is Element of (Euclid N) : dist (u,u6) < r } by A5, A9;
hence a in Ball (u,r) by METRIC_1:17; :: thesis: verum
end;