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 A1:
( p1 in Ball u,r & p2 in Ball u,r )
; :: thesis: LSeg p1,p2 c= Ball u,r
then reconsider p' = p1 as Point of (Euclid n) ;
A2:
dist p',u < r
by A1, METRIC_1:12;
thus
LSeg p1,p2 c= Ball u,r
:: thesis: verumproof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in LSeg p1,p2 or a in Ball u,r )
assume
a in LSeg p1,
p2
;
:: thesis: a in Ball u,r
then consider lambda being
Real such that A3:
((1 - lambda) * p1) + (lambda * p2) = a
and A4:
(
0 <= lambda &
lambda <= 1 )
;
set p =
((1 - lambda) * p1) + (lambda * p2);
reconsider q2' =
u as
Element of
REAL n ;
reconsider q2 =
q2' as
Point of
(TOP-REAL n) by EUCLID:25;
A5:
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)))
by EUCLID:45
.=
(((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
;
reconsider p' =
((1 - lambda) * p1) + (lambda * p2),
p1' =
p1,
p2' =
p2 as
Element of
REAL n by EUCLID:25;
U:
(
q2' - p' = q2 - (((1 - lambda) * p1) + (lambda * p2)) &
q2' - p1' = q2 - p1 &
q2' - p2' = q2 - p2 )
by EUCLID:73;
then
(
(1 - lambda) * (q2' - p1') = (1 - lambda) * (q2 - p1) &
lambda * (q2' - p2') = lambda * (q2 - p2) )
by EUCLID:69;
then
q2' - p' = ((1 - lambda) * (q2' - p1')) + (lambda * (q2' - p2'))
by A5, U, EUCLID:68;
then A6:
|.(q2' - p').| <= |.((1 - lambda) * (q2' - p1')).| + |.(lambda * (q2' - p2')).|
by A5, U, EUCLID:15;
A7:
|.((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
;
consider u3 being
Point of
(Euclid n) such that A8:
(
u3 = p1 &
dist u,
u3 < r )
by A2;
A9:
(Pitag_dist n) . q2',
p1' = |.(q2' - p1').|
by EUCLID:def 6;
then A10:
dist u,
u3 = |.(q2' - p1').|
by A8, METRIC_1:def 1;
p2 in { u4 where u4 is Point of (Euclid n) : dist u,u4 < r }
by A1, METRIC_1:18;
then consider u4 being
Point of
(Euclid n) such that A11:
(
u4 = p2 &
dist u,
u4 < r )
;
(Pitag_dist n) . q2',
p2' = |.(q2' - p2').|
by EUCLID:def 6;
then A12:
|.(q2' + (- p2')).| < r
by A11, METRIC_1:def 1;
A13:
0 <= 1
- lambda
by A4, XREAL_1:50;
then A14:
( 1
- lambda = abs (1 - lambda) &
lambda = abs lambda )
by A4, ABSVALUE: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
((abs (1 - lambda)) * |.(q2' + (- p1')).|) + ((abs lambda) * |.(q2' + (- p2')).|) < ((1 - lambda) * r) + (lambda * r)
by XREAL_1:10;
then A15:
|.(q2' - p').| < r
by A6, A7, XXREAL_0:2;
reconsider u5 =
((1 - lambda) * p1) + (lambda * p2) as
Point of
(Euclid n) by EUCLID:25;
A16:
(Pitag_dist n) . q2',
p' = |.(q2' - p').|
by EUCLID:def 6;
(Pitag_dist n) . u,
u5 = dist u,
u5
by METRIC_1:def 1;
then
a in { u6 where u6 is Element of (Euclid n) : dist u,u6 < r }
by A3, A15, A16;
hence
a in Ball u,
r
by METRIC_1:18;
:: thesis: verum
end;
thus
verum
; :: thesis: verum