let n be Element of NAT ; :: thesis: for r being real number
for y, x, z being Point of (TOP-REAL n) st y in Sphere x,r & z in Sphere x,r holds
(LSeg y,z) \ {y,z} c= Ball x,r
let r be real number ; :: thesis: for y, x, z being Point of (TOP-REAL n) st y in Sphere x,r & z in Sphere x,r holds
(LSeg y,z) \ {y,z} c= Ball x,r
let y, x, z be Point of (TOP-REAL n); :: thesis: ( y in Sphere x,r & z in Sphere x,r implies (LSeg y,z) \ {y,z} c= Ball x,r )
assume that
A1:
y in Sphere x,r
and
A2:
z in Sphere x,r
; :: thesis: (LSeg y,z) \ {y,z} c= Ball x,r
per cases
( y = z or y <> z )
;
suppose A3:
y <> z
;
:: thesis: (LSeg y,z) \ {y,z} c= Ball x,rlet a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in (LSeg y,z) \ {y,z} or a in Ball x,r )assume A4:
a in (LSeg y,z) \ {y,z}
;
:: thesis: a in Ball x,rthen reconsider R =
a as
Point of
(TOP-REAL n) ;
A5:
R in LSeg y,
z
by A4, XBOOLE_0:def 5;
then consider l being
Real such that A6:
0 <= l
and A7:
l <= 1
and A8:
R = ((1 - l) * y) + (l * z)
by JGRAPH_1:52;
set l1 = 1
- l;
set X =
|((y - x),(z - x))|;
UU: the
carrier of
(TOP-REAL n) =
REAL n
by EUCLID:25
.=
n -tuples_on REAL
;
then reconsider xf =
x,
yf =
y,
zf =
z as
Element of
n -tuples_on REAL ;
reconsider y1 =
y - x,
z1 =
z - x as
FinSequence of
REAL by EUCLID:27;
reconsider Rf =
R - x as
FinSequence of
REAL by EUCLID:27;
A9:
Sum (sqr Rf) >= 0
by RVSUM_1:116;
A10:
|.(y - x).| ^2 = r ^2
by A1, Th9;
A11:
|.(z - x).| ^2 = r ^2
by A2, Th9;
reconsider W1 =
(1 - l) * (y - x),
W2 =
l * (z - x) as
Element of
REAL n by EUCLID:25;
A12:
W1 + W2 =
((1 - l) * (y - x)) + (l * (z - x))
by EUCLID:68
.=
(((1 - l) * y) - ((1 - l) * x)) + (l * (z - x))
by EUCLID:53
.=
(((1 - l) * y) - ((1 - l) * x)) + ((l * z) - (l * x))
by EUCLID:53
.=
((((1 - l) * y) - ((1 - l) * x)) + (l * z)) - (l * x)
by EUCLID:49
.=
((((1 - l) * y) + (l * z)) - ((1 - l) * x)) - (l * x)
by JORDAN2C:9
.=
(((1 - l) * y) + (l * z)) - (((1 - l) * x) + (l * x))
by EUCLID:50
.=
(((1 - l) * y) + (l * z)) - (((1 * x) - (l * x)) + (l * x))
by EUCLID:54
.=
(((1 - l) * y) + (l * z)) - (1 * x)
by EUCLID:52
.=
Rf
by A8, EUCLID:33
;
reconsider W1 =
W1,
W2 =
W2 as
Element of
n -tuples_on REAL by EUCLID:25;
reconsider yyf =
yf,
zzf =
zf,
xxf =
xf as
Element of
REAL n ;
AA:
y - x = yyf - xxf
by EUCLID:73;
A:
sqr W1 =
sqr ((1 - l) * (y - x))
.=
sqr ((1 - l) * (yf - xf))
by AA, EUCLID:69
.=
((1 - l) ^2 ) * (sqr (yf - xf))
by RVSUM_1:84
;
BB:
z - x = zzf - xxf
by EUCLID:73;
B:
sqr W2 =
sqr (l * (z - x))
.=
sqr (l * (zf - xf))
by BB, EUCLID:69
;
C:
((1 - l) ^2 ) * (Sum (sqr (yf - xf))) = ((1 - l) ^2 ) * (|.y1.| ^2 )
by Th5, AA;
D:
Sum (sqr (zf - xf)) =
Sum (sqr (zzf - xxf))
by BB
.=
|.z1.| ^2
by A10, Th5, BB
;
E:
mlt W1,
W2 =
mlt ((1 - l) * (y - x)),
(l * (z - x))
.=
mlt ((1 - l) * (y - x)),
(l * (zzf - xxf))
by AA, BB, EUCLID:69
.=
mlt ((1 - l) * (yyf - xxf)),
(l * (zzf - xxf))
by AA, BB, EUCLID:69
.=
(1 - l) * (mlt (yf - xf),(l * (zf - xf)))
by RVSUM_1:94
;
F:
Sum (mlt (yf - xf),(zf - xf)) = |((y - x),(z - x))|
by AA, BB, EUCLID_2:def 1;
|.(R - x).| ^2 =
Sum (sqr Rf)
by A9, SQUARE_1:def 4
.=
Sum (((sqr W1) + (2 * (mlt W1,W2))) + (sqr W2))
by A12, RVSUM_1:98
.=
(Sum ((sqr W1) + (2 * (mlt W1,W2)))) + (Sum (sqr W2))
by RVSUM_1:119
.=
((Sum (sqr W1)) + (Sum (2 * (mlt W1,W2)))) + (Sum (sqr W2))
by RVSUM_1:119
.=
((Sum (((1 - l) ^2 ) * (sqr (yf - xf)))) + (Sum (2 * (mlt W1,W2)))) + (Sum (sqr (l * (zf - xf))))
by A, B, RVSUM_1:84
.=
((((1 - l) ^2 ) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt W1,W2)))) + (Sum (sqr (l * (zf - xf))))
by RVSUM_1:117
.=
((((1 - l) ^2 ) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt W1,W2)))) + (Sum ((l ^2 ) * (sqr (zf - xf))))
by RVSUM_1:84
.=
((((1 - l) ^2 ) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt W1,W2)))) + ((l ^2 ) * (Sum (sqr (zf - xf))))
by RVSUM_1:117
.=
((((1 - l) ^2 ) * (|.y1.| ^2 )) + (Sum (2 * (mlt W1,W2)))) + ((l ^2 ) * (Sum (sqr (zf - xf))))
by Th5, C
.=
((((1 - l) ^2 ) * (r ^2 )) + (Sum (2 * (mlt W1,W2)))) + ((l ^2 ) * (|.z1.| ^2 ))
by A10, Th5, D
.=
((((1 - l) ^2 ) * (r ^2 )) + (2 * (Sum (mlt W1,W2)))) + ((l ^2 ) * (r ^2 ))
by A11, RVSUM_1:117
.=
((((1 - l) ^2 ) * (r ^2 )) + (2 * (Sum ((1 - l) * (mlt (yf - xf),(l * (zf - xf))))))) + ((l ^2 ) * (r ^2 ))
by E, RVSUM_1:94
.=
((((1 - l) ^2 ) * (r ^2 )) + (2 * (Sum ((1 - l) * (l * (mlt (yf - xf),(zf - xf))))))) + ((l ^2 ) * (r ^2 ))
by RVSUM_1:94
.=
((((1 - l) ^2 ) * (r ^2 )) + (2 * (Sum (((1 - l) * l) * (mlt (yf - xf),(zf - xf)))))) + ((l ^2 ) * (r ^2 ))
by RVSUM_1:71
.=
((((1 - l) ^2 ) * (r ^2 )) + (2 * (((1 - l) * l) * (Sum (mlt (yf - xf),(zf - xf)))))) + ((l ^2 ) * (r ^2 ))
by RVSUM_1:117
.=
((((1 - l) ^2 ) * (r ^2 )) + (((2 * (1 - l)) * l) * (Sum (mlt (yf - xf),(zf - xf))))) + ((l ^2 ) * (r ^2 ))
.=
((((1 - l) ^2 ) * (r ^2 )) + (((2 * (1 - l)) * l) * |((y - x),(z - x))|)) + ((l ^2 ) * (r ^2 ))
by F, EUCLID_2:def 1
.=
((((1 - (2 * l)) + (l ^2 )) + (l ^2 )) * (r ^2 )) + (((2 * l) * (1 - l)) * |((y - x),(z - x))|)
;
then A13:
(|.(R - x).| ^2 ) - (r ^2 ) = ((2 * l) * (1 - l)) * ((- (r ^2 )) + |((y - x),(z - x))|)
;
Sphere x,
r c= cl_Ball x,
r
by Th17;
then
LSeg y,
z c= cl_Ball x,
r
by A1, A2, JORDAN1:def 1;
then A14:
|.(R - x).| <= r
by A5, Th8;
then A15:
2
* l > 0
by A6, XREAL_1:131;
A16:
1
- 1
<= 1
- l
by A7, XREAL_1:15;
then A17:
(2 * l) * (1 - l) > 0
by A15, A16, XREAL_1:131;
A18:
Sum (sqr (yf - zf)) >= 0
by RVSUM_1:116;
CC:
yyf - zzf = y - z
by EUCLID:73;
then
|.(R - x).| < r
by A14, XXREAL_0:1;
hence
a in Ball x,
r
;
:: thesis: verum end;