let n be Nat; for a, r being Real
for y, z, x being Point of (TOP-REAL n)
for S, T, X being Element of REAL n st S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds
ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) )
let a, r be Real; for y, z, x being Point of (TOP-REAL n)
for S, T, X being Element of REAL n st S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds
ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) )
let y, z, x be Point of (TOP-REAL n); for S, T, X being Element of REAL n st S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds
ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) )
let S, T, X be Element of REAL n; ( S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) ) )
assume that
A1:
S = y
and
A2:
T = z
and
A3:
X = x
; ( not y <> z or not y in Ball (x,r) or not a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) or ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) ) )
set s = y;
set t = z;
A4:
Sum (sqr (T - S)) >= 0
by RVSUM_1:86;
then A5:
|.(T - S).| ^2 = Sum (sqr (T - S))
by SQUARE_1:def 2;
set A = Sum (sqr (T - S));
assume that
A6:
y <> z
and
A7:
y in Ball (x,r)
and
A8:
a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))
; ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) )
A9:
|.(T - S).| <> 0
by A1, A2, A6, EUCLID:16;
set C = (Sum (sqr (S - X))) - (r ^2);
set B = 2 * |((z - y),(y - x))|;
A11:
( r = 0 or r <> 0 )
;
Sum (sqr (S - X)) >= 0
by RVSUM_1:86;
then A12:
|.(S - X).| ^2 = Sum (sqr (S - X))
by SQUARE_1:def 2;
|.(y - x).| < r
by A7, Th5;
then
(sqrt (Sum (sqr (S - X)))) ^2 < r ^2
by A1, A3, SQUARE_1:16;
then A13:
(Sum (sqr (S - X))) - (r ^2) < 0
by A12, XREAL_1:49;
then A14:
((Sum (sqr (S - X))) - (r ^2)) / (Sum (sqr (T - S))) < 0
by A10, XREAL_1:141;
set l2 = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
set l1 = ((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
take e1 = ((1 - (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * y) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z); ( {e1} = (halfline (y,z)) /\ (Sphere (x,r)) & e1 = ((1 - a) * y) + (a * z) )
A15:
0 <= - (- r)
by A7;
A16:
( delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2))) = ((2 * |((z - y),(y - x))|) ^2) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - X))) - (r ^2))) & (2 * |((z - y),(y - x))|) ^2 >= 0 )
by QUIN_1:def 1, XREAL_1:63;
A17:
for x being Real holds Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),x) = Quard ((Sum (sqr (T - S))),(((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x)
proof
let x be
Real;
Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),x) = Quard ((Sum (sqr (T - S))),(((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x)
thus Polynom (
(Sum (sqr (T - S))),
(2 * |((z - y),(y - x))|),
((Sum (sqr (S - X))) - (r ^2)),
x) =
(((Sum (sqr (T - S))) * (x ^2)) + ((2 * |((z - y),(y - x))|) * x)) + ((Sum (sqr (S - X))) - (r ^2))
by POLYEQ_1:def 2
.=
((Sum (sqr (T - S))) * (x - (((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) * (x - (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))
by A10, A13, A16, QUIN_1:16
.=
(Sum (sqr (T - S))) * ((x - (((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * (x - (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))))
.=
Quard (
(Sum (sqr (T - S))),
(((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),
(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),
x)
by POLYEQ_1:def 3
;
verum
end;
then
((Sum (sqr (S - X))) - (r ^2)) / (Sum (sqr (T - S))) = (((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))
by A10, POLYEQ_1:11;
then A18:
( ( ((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) < 0 & ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) > 0 ) or ( ((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) > 0 & ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) < 0 ) )
by A14, XREAL_1:133;
A19: (((Sum (sqr (T - S))) * ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2)) + ((2 * |((z - y),(y - x))|) * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) - (- ((Sum (sqr (S - X))) - (r ^2))) =
Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))
by POLYEQ_1:def 2
.=
Quard ((Sum (sqr (T - S))),(((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))
by A17
.=
(Sum (sqr (T - S))) * (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) - (((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) - (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))))
by POLYEQ_1:def 3
.=
0
;
|.(e1 - x).| ^2 =
|.((((1 * y) - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y)) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z)) - x).| ^2
by RLVECT_1:35
.=
|.(((y - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y)) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z)) - x).| ^2
by RLVECT_1:def 8
.=
|.(((y + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z)) - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y)) - x).| ^2
by RLVECT_1:def 3
.=
|.((y + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z) - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y))) - x).| ^2
by RLVECT_1:def 3
.=
|.((y - x) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z) - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y))).| ^2
by RLVECT_1:def 3
.=
|.((y - x) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (z - y))).| ^2
by RLVECT_1:34
.=
((|.(y - x).| ^2) + (2 * |(((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (z - y)),(y - x))|)) + (|.((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (z - y)).| ^2)
by EUCLID_2:45
.=
((Sum (sqr (S - X))) + (2 * ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * |((z - y),(y - x))|))) + (|.((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (z - y)).| ^2)
by A12, A1, A3, EUCLID_2:19
.=
((Sum (sqr (S - X))) + ((2 * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * |((z - y),(y - x))|)) + ((|.(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))).| * |.(z - y).|) ^2)
by TOPRNS_1:7
.=
((Sum (sqr (S - X))) + ((2 * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * |((z - y),(y - x))|)) + ((|.(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))).| ^2) * (|.(z - y).| ^2))
.=
((Sum (sqr (S - X))) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (2 * |((z - y),(y - x))|))) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2) * (|.(T - S).| ^2))
by A1, A2, COMPLEX1:75
.=
((Sum (sqr (S - X))) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (2 * |((z - y),(y - x))|))) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2) * (Sum (sqr (T - S))))
by A4, SQUARE_1:def 2
.=
r ^2
by A19
;
then
( |.(e1 - x).| = r or |.(e1 - x).| = - r )
by SQUARE_1:40;
then A20:
e1 in Sphere (x,r)
by A15, A11;
A21:
(4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - X))) - (r ^2)) < 0
by A10, A13, XREAL_1:129, XREAL_1:132;
then A22:
e1 in halfline (y,z)
by A10, A16, A18, QUIN_1:25;
hereby TARSKI:def 3 e1 = ((1 - a) * y) + (a * z)
let d be
object ;
( d in (halfline (y,z)) /\ (Sphere (x,r)) implies d in {e1} )assume A23:
d in (halfline (y,z)) /\ (Sphere (x,r))
;
d in {e1}then
d in halfline (
y,
z)
by XBOOLE_0:def 4;
then consider l being
Real such that A24:
d = ((1 - l) * y) + (l * z)
and A25:
0 <= l
;
A26:
|.(l * (z - y)).| ^2 =
(|.l.| * |.(z - y).|) ^2
by TOPRNS_1:7
.=
(|.l.| ^2) * (|.(z - y).| ^2)
.=
(l ^2) * (|.(z - y).| ^2)
by COMPLEX1:75
;
d in Sphere (
x,
r)
by A23, XBOOLE_0:def 4;
then r =
|.((((1 - l) * y) + (l * z)) - x).|
by A24, Th7
.=
|.((((1 * y) - (l * y)) + (l * z)) - x).|
by RLVECT_1:35
.=
|.(((y - (l * y)) + (l * z)) - x).|
by RLVECT_1:def 8
.=
|.((y - ((l * y) - (l * z))) - x).|
by RLVECT_1:29
.=
|.((y + (- ((l * y) - (l * z)))) + (- x)).|
.=
|.((y + (- x)) + (- ((l * y) - (l * z)))).|
by RLVECT_1:def 3
.=
|.((y - x) - ((l * y) - (l * z))).|
.=
|.((y + (- x)) + (- ((l * y) - (l * z)))).|
.=
|.((y - x) + (- (l * (y - z)))).|
by RLVECT_1:34
.=
|.((y - x) + (l * (- (y - z)))).|
by RLVECT_1:25
.=
|.((y - x) + (l * (z - y))).|
by RLVECT_1:33
;
then r ^2 =
((|.(y - x).| ^2) + (2 * |((l * (z - y)),(y - x))|)) + (|.(l * (z - y)).| ^2)
by EUCLID_2:45
.=
((|.(y - x).| ^2) + (2 * (l * |((z - y),(y - x))|))) + (|.(l * (z - y)).| ^2)
by EUCLID_2:19
;
then
(((Sum (sqr (T - S))) * (l ^2)) + ((2 * |((z - y),(y - x))|) * l)) + ((Sum (sqr (S - X))) - (r ^2)) = 0
by A5, A12, A1, A3, A2, A26;
then
Polynom (
(Sum (sqr (T - S))),
(2 * |((z - y),(y - x))|),
((Sum (sqr (S - X))) - (r ^2)),
l)
= 0
by POLYEQ_1:def 2;
then
(
l = ((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) or
l = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) )
by A10, A13, A16, POLYEQ_1:5;
hence
d in {e1}
by A10, A21, A16, A18, A24, A25, QUIN_1:25, TARSKI:def 1;
verum
end;
thus
e1 = ((1 - a) * y) + (a * z)
by A8; verum