let n be Nat; for r being Real
for y, z, x 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; for y, z, x 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, z, x be Point of (TOP-REAL n); ( 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)
; (LSeg (y,z)) \ {y,z} c= Ball (x,r)
per cases
( y = z or y <> z )
;
suppose A3:
y <> z
;
(LSeg (y,z)) \ {y,z} c= Ball (x,r) the
carrier of
(TOP-REAL n) =
REAL n
by EUCLID:22
.=
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 ;
set X =
|((y - x),(z - x))|;
let a be
object ;
TARSKI:def 3 ( not a in (LSeg (y,z)) \ {y,z} or a in Ball (x,r) )A4:
Sum (sqr (zf - xf)) = |.z1.| ^2
by Th3;
A5:
|.(z - x).| ^2 = r ^2
by A2, Th7;
assume A6:
a in (LSeg (y,z)) \ {y,z}
;
a in Ball (x,r)then reconsider R =
a as
Point of
(TOP-REAL n) ;
A7:
R in LSeg (
y,
z)
by A6, XBOOLE_0:def 5;
then consider l being
Real such that A8:
0 <= l
and A9:
l <= 1
and A10:
R = ((1 - l) * y) + (l * z)
by RLTOPSP1:76;
set l1 = 1
- l;
reconsider W1 =
(1 - l) * (y - x),
W2 =
l * (z - x) as
Element of
REAL n by EUCLID:22;
A11:
Sum (sqr (yf - zf)) >= 0
by RVSUM_1:86;
reconsider Rf =
R - x as
FinSequence of
REAL ;
A12:
W1 + W2 =
(((1 - l) * y) - ((1 - l) * x)) + (l * (z - x))
by RLVECT_1:34
.=
(((1 - l) * y) - ((1 - l) * x)) + ((l * z) - (l * x))
by RLVECT_1:34
.=
((((1 - l) * y) - ((1 - l) * x)) + (l * z)) - (l * x)
by RLVECT_1:def 3
.=
((((1 - l) * y) + (l * z)) - ((1 - l) * x)) - (l * x)
by RLVECT_1:def 3
.=
(((1 - l) * y) + (l * z)) - (((1 - l) * x) + (l * x))
by RLVECT_1:27
.=
(((1 - l) * y) + (l * z)) - (((1 * x) - (l * x)) + (l * x))
by RLVECT_1:35
.=
(((1 - l) * y) + (l * z)) - (1 * x)
by RLVECT_4:1
.=
Rf
by A10, RLVECT_1:def 8
;
reconsider W1 =
W1,
W2 =
W2 as
Element of
n -tuples_on REAL ;
A13:
mlt (
W1,
W2)
= (1 - l) * (mlt ((yf - xf),(l * (zf - xf))))
by RVSUM_1:65;
A14:
sqr W1 = ((1 - l) ^2) * (sqr (yf - xf))
by RVSUM_1:58;
Sum (sqr Rf) >= 0
by RVSUM_1:86;
then |.(R - x).| ^2 =
Sum (sqr Rf)
by SQUARE_1:def 2
.=
Sum (((sqr W1) + (2 * (mlt (W1,W2)))) + (sqr W2))
by A12, RVSUM_1:68
.=
(Sum ((sqr W1) + (2 * (mlt (W1,W2))))) + (Sum (sqr W2))
by RVSUM_1:89
.=
((Sum (sqr W1)) + (Sum (2 * (mlt (W1,W2))))) + (Sum (sqr W2))
by RVSUM_1:89
.=
((((1 - l) ^2) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt (W1,W2))))) + (Sum (sqr (l * (zf - xf))))
by A14, RVSUM_1:87
.=
((((1 - l) ^2) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt (W1,W2))))) + (Sum ((l ^2) * (sqr (zf - xf))))
by RVSUM_1:58
.=
((((1 - l) ^2) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt (W1,W2))))) + ((l ^2) * (Sum (sqr (zf - xf))))
by RVSUM_1:87
.=
((((1 - l) ^2) * (|.y1.| ^2)) + (Sum (2 * (mlt (W1,W2))))) + ((l ^2) * (Sum (sqr (zf - xf))))
by Th3
.=
((((1 - l) ^2) * (r ^2)) + (Sum (2 * (mlt (W1,W2))))) + ((l ^2) * (|.z1.| ^2))
by A1, A4, Th7
.=
((((1 - l) ^2) * (r ^2)) + (2 * (Sum (mlt (W1,W2))))) + ((l ^2) * (r ^2))
by A5, RVSUM_1:87
.=
((((1 - l) ^2) * (r ^2)) + (2 * (Sum ((1 - l) * (l * (mlt ((yf - xf),(zf - xf)))))))) + ((l ^2) * (r ^2))
by A13, RVSUM_1:65
.=
((((1 - l) ^2) * (r ^2)) + (2 * (Sum (((1 - l) * l) * (mlt ((yf - xf),(zf - xf))))))) + ((l ^2) * (r ^2))
by RVSUM_1:49
.=
((((1 - l) ^2) * (r ^2)) + (2 * (((1 - l) * l) * (Sum (mlt ((yf - xf),(zf - xf))))))) + ((l ^2) * (r ^2))
by RVSUM_1:87
.=
((((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 RVSUM_1:def 16
.=
((((1 - (2 * l)) + (l ^2)) + (l ^2)) * (r ^2)) + (((2 * l) * (1 - l)) * |((y - x),(z - x))|)
;
then A15:
(|.(R - x).| ^2) - (r ^2) = ((2 * l) * (1 - l)) * ((- (r ^2)) + |((y - x),(z - x))|)
;
then A16:
2
* l > 0
by A8, XREAL_1:129;
1
- 1
<= 1
- l
by A9, XREAL_1:13;
then A18:
(2 * l) * (1 - l) > 0
by A16, A17, XREAL_1:129;
A19:
|.(y - x).| ^2 = r ^2
by A1, Th7;
Sphere (
x,
r)
c= cl_Ball (
x,
r)
by Th15;
then
LSeg (
y,
z)
c= cl_Ball (
x,
r)
by A1, A2, JORDAN1:def 1;
then
|.(R - x).| <= r
by A7, Th6;
then
|.(R - x).| < r
by A20, XXREAL_0:1;
hence
a in Ball (
x,
r)
;
verum end; end;