let r be Real; 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; 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); 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); ( 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)
; 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)
verumproof
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 ;
TARSKI:def 3 ( 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)
;
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 ) )
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;
verum
end;