let r be real number ; :: thesis: for n being Element of 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 Element of 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 p' = p1 as Point of (Euclid n) by A1;
A3:
dist p',u < r
by A1, METRIC_1:12;
thus
LSeg p1,p2 c= Ball u,r
:: thesis: verumproof
p2 in { u4 where u4 is Point of (Euclid n) : dist u,u4 < r }
by A2, METRIC_1:18;
then A4:
ex
u4 being
Point of
(Euclid n) st
(
u4 = p2 &
dist u,
u4 < r )
;
reconsider q2' =
u as
Element of
REAL n ;
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in LSeg p1,p2 or a in Ball u,r )
reconsider q2 =
q2' as
Point of
(TOP-REAL n) by EUCLID:25;
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 = abs lambda
by A6, ABSVALUE:def 1;
set p =
((1 - lambda) * p1) + (lambda * p2);
reconsider p' =
((1 - lambda) * p1) + (lambda * p2),
p1' =
p1,
p2' =
p2 as
Element of
REAL n by EUCLID:25;
reconsider u5 =
((1 - lambda) * p1) + (lambda * p2) as
Point of
(Euclid n) by EUCLID:25;
A9:
(
(Pitag_dist n) . q2',
p' = |.(q2' - p').| &
(Pitag_dist n) . u,
u5 = dist u,
u5 )
by EUCLID:def 6, METRIC_1:def 1;
(Pitag_dist n) . q2',
p2' = |.(q2' - p2').|
by EUCLID:def 6;
then A10:
|.(q2' + (- p2')).| < r
by A4, METRIC_1:def 1;
A11:
0 <= 1
- lambda
by A7, XREAL_1:50;
then A12:
1
- lambda = abs (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) . q2',
p1' = |.(q2' - p1').|
by EUCLID:def 6;
then A16:
dist u,
u3 = |.(q2' - p1').|
by A13, METRIC_1:def 1;
( (
(abs (1 - lambda)) * |.(q2' + (- p1')).| < (1 - lambda) * r &
(abs lambda) * |.(q2' + (- p2')).| <= lambda * r ) or (
(abs (1 - lambda)) * |.(q2' + (- p1')).| <= (1 - lambda) * r &
(abs lambda) * |.(q2' + (- p2')).| < lambda * r ) )
then A17:
((abs (1 - lambda)) * |.(q2' + (- p1')).|) + ((abs lambda) * |.(q2' + (- p2')).|) < ((1 - lambda) * r) + (lambda * r)
by XREAL_1:10;
q2' - p1' = q2 - p1
by EUCLID:73;
then A18:
(
q2' - p' = q2 - (((1 - lambda) * p1) + (lambda * p2)) &
(1 - lambda) * (q2' - p1') = (1 - lambda) * (q2 - p1) )
by EUCLID:69, EUCLID:73;
q2' - p2' = q2 - p2
by EUCLID:73;
then A19:
lambda * (q2' - p2') = lambda * (q2 - p2)
by EUCLID:69;
q2 - (((1 - lambda) * p1) + (lambda * p2)) =
(((1 - lambda) + lambda) * q2) - (((1 - lambda) * p1) + (lambda * p2))
by EUCLID:33
.=
(((1 - lambda) * q2) + (lambda * q2)) - (((1 - lambda) * p1) + (lambda * p2))
by EUCLID:37
.=
(((1 - lambda) * q2) + (lambda * q2)) + (- (((1 - lambda) * p1) + (lambda * p2)))
.=
(((1 - lambda) * q2) + (lambda * q2)) + ((- ((1 - lambda) * p1)) - (lambda * p2))
by EUCLID:42
.=
((((1 - lambda) * q2) + (lambda * q2)) + (- ((1 - lambda) * p1))) + (- (lambda * p2))
by EUCLID:30
.=
((((1 - lambda) * q2) + (- ((1 - lambda) * p1))) + (lambda * q2)) + (- (lambda * p2))
by EUCLID:30
.=
((((1 - lambda) * q2) + ((1 - lambda) * (- p1))) + (lambda * q2)) + (- (lambda * p2))
by EUCLID:44
.=
(((1 - lambda) * (q2 + (- p1))) + (lambda * q2)) + (- (lambda * p2))
by EUCLID:36
.=
((1 - lambda) * (q2 + (- p1))) + ((lambda * q2) + (- (lambda * p2)))
by EUCLID:30
.=
((1 - lambda) * (q2 + (- p1))) + ((lambda * q2) + (lambda * (- p2)))
by EUCLID:44
.=
((1 - lambda) * (q2 - p1)) + (lambda * (q2 - p2))
by EUCLID:36
;
then
q2' - p' = ((1 - lambda) * (q2' - p1')) + (lambda * (q2' - p2'))
by A18, A19, EUCLID:68;
then A20:
|.(q2' - p').| <= |.((1 - lambda) * (q2' - p1')).| + |.(lambda * (q2' - p2')).|
by EUCLID:15;
|.((1 - lambda) * (q2' + (- p1'))).| + |.(lambda * (q2' + (- p2'))).| =
((abs (1 - lambda)) * |.(q2' + (- p1')).|) + |.(lambda * (q2' + (- p2'))).|
by EUCLID:14
.=
((abs (1 - lambda)) * |.(q2' + (- p1')).|) + ((abs lambda) * |.(q2' + (- p2')).|)
by EUCLID:14
;
then
|.(q2' - p').| < 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:18;
:: thesis: verum
end;
thus
verum
; :: thesis: verum