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 y = z ; :: thesis: (LSeg y,z) \ {y,z} c= Ball x,r
then ( LSeg y,z = {y} & {y,z} = {y} ) by ENUMSET1:69, RLTOPSP1:71;
then (LSeg y,z) \ {y,z} = {} by XBOOLE_1:37;
hence (LSeg y,z) \ {y,z} c= Ball x,r by XBOOLE_1:2; :: thesis: verum
end;
suppose A3: y <> z ; :: thesis: (LSeg y,z) \ {y,z} c= Ball x,r
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 yyf = yf, zzf = zf, xxf = xf as Element of REAL n ;
reconsider y1 = y - x, z1 = z - x as FinSequence of REAL by EUCLID:27;
set X = |((y - x),(z - x))|;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg y,z) \ {y,z} or a in Ball x,r )
A4: z - x = zzf - xxf by EUCLID:73;
A5: Sum (sqr (zf - xf)) = Sum (sqr (zzf - xxf))
.= |.z1.| ^2 by A4, Th5 ;
A6: |.(z - x).| ^2 = r ^2 by A2, Th9;
assume A7: a in (LSeg y,z) \ {y,z} ; :: thesis: a in Ball x,r
then reconsider R = a as Point of (TOP-REAL n) ;
A8: R in LSeg y,z by A7, XBOOLE_0:def 5;
then consider l being Real such that
A9: 0 <= l and
A10: l <= 1 and
A11: R = ((1 - l) * y) + (l * z) by JGRAPH_1:52;
set l1 = 1 - l;
reconsider W1 = (1 - l) * (y - x), W2 = l * (z - x) as Element of REAL n by EUCLID:25;
A12: Sum (sqr (yf - zf)) >= 0 by RVSUM_1:116;
reconsider Rf = R - x as FinSequence of REAL by EUCLID:27;
A13: y - x = yyf - xxf by EUCLID:73;
A14: 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 A11, EUCLID:33 ;
reconsider W1 = W1, W2 = W2 as Element of n -tuples_on REAL ;
A15: mlt W1,W2 = mlt ((1 - l) * (y - x)),(l * (z - x))
.= mlt ((1 - l) * (y - x)),(l * (zzf - xxf)) by A4, EUCLID:69
.= mlt ((1 - l) * (yyf - xxf)),(l * (zzf - xxf)) by A13, EUCLID:69
.= (1 - l) * (mlt (yf - xf),(l * (zf - xf))) by RVSUM_1:94 ;
A16: sqr W2 = sqr (l * (z - x))
.= sqr (l * (zf - xf)) by A4, EUCLID:69 ;
A17: sqr W1 = sqr ((1 - l) * (y - x))
.= sqr ((1 - l) * (yf - xf)) by A13, EUCLID:69
.= ((1 - l) ^2 ) * (sqr (yf - xf)) by RVSUM_1:84 ;
Sum (sqr Rf) >= 0 by RVSUM_1:116;
then |.(R - x).| ^2 = Sum (sqr Rf) by SQUARE_1:def 4
.= Sum (((sqr W1) + (2 * (mlt W1,W2))) + (sqr W2)) by A14, 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 A17, A16
.= ((((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 A13, Th5
.= ((((1 - l) ^2 ) * (r ^2 )) + (Sum (2 * (mlt W1,W2)))) + ((l ^2 ) * (|.z1.| ^2 )) by A1, A5, Th9
.= ((((1 - l) ^2 ) * (r ^2 )) + (2 * (Sum (mlt W1,W2)))) + ((l ^2 ) * (r ^2 )) by A6, RVSUM_1:117
.= ((((1 - l) ^2 ) * (r ^2 )) + (2 * (Sum ((1 - l) * (mlt (yf - xf),(l * (zf - xf))))))) + ((l ^2 ) * (r ^2 )) by A15
.= ((((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 A13, A4, RVSUM_1:def 17
.= ((((1 - (2 * l)) + (l ^2 )) + (l ^2 )) * (r ^2 )) + (((2 * l) * (1 - l)) * |((y - x),(z - x))|) ;
then A18: (|.(R - x).| ^2 ) - (r ^2 ) = ((2 * l) * (1 - l)) * ((- (r ^2 )) + |((y - x),(z - x))|) ;
A19: yyf - zzf = y - z by EUCLID:73;
then A20: 2 * l > 0 by A9, XREAL_1:131;
1 - 1 <= 1 - l by A10, XREAL_1:15;
then A22: (2 * l) * (1 - l) > 0 by A20, A21, XREAL_1:131;
A23: |.(y - x).| ^2 = r ^2 by A1, Th9;
A24: now
assume |.(R - x).| = r ; :: thesis: contradiction
then |((y - x),(z - x))| - (r ^2 ) = 0 by A18, A22, XCMPLX_1:6;
then 0 = ((|.(y - x).| ^2 ) - (2 * |((y - x),(z - x))|)) + (|.(z - x).| ^2 ) by A2, A23, Th9
.= |.((y - x) - (z - x)).| ^2 by EUCLID_2:68
.= |.(((y - x) - z) + x).| ^2 by EUCLID:51
.= |.(((y - x) + x) - z).| ^2 by JORDAN2C:9
.= |.(yf - zf).| ^2 by A19, EUCLID:52
.= Sum (sqr (yf - zf)) by A12, SQUARE_1:def 4 ;
then yf - zf = n |-> 0 by RVSUM_1:121;
hence contradiction by A3, RVSUM_1:59; :: thesis: verum
end;
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 |.(R - x).| <= r by A8, Th8;
then |.(R - x).| < r by A24, XXREAL_0:1;
hence a in Ball x,r ; :: thesis: verum
end;
end;