let n be Element of NAT ; :: thesis: for r, a being real number
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 r, a be real number ; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 A1:
( S = y & T = z & X = x )
; :: thesis: ( 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;
assume that
A2:
y <> z
and
A3:
y in Ball x,r
and
A4:
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))))
; :: thesis: ex e being Point of (TOP-REAL n) st
( {e} = (halfline y,z) /\ (Sphere x,r) & e = ((1 - a) * y) + (a * z) )
reconsider G = x as Point of (Euclid n) by TOPREAL3:13;
A6:
0 <= - (- r)
by A3;
set A = Sum (sqr (T - S));
set B = 2 * |((z - y),(y - x))|;
set C = (Sum (sqr (S - X))) - (r ^2 );
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))));
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))));
A7:
|.(T - S).| <> 0
by A1, A2, EUCLID:19;
A9:
|.(y - x).| < r
by A3, Th7;
Sum (sqr (T - S)) >= 0
by RVSUM_1:116;
then A10:
|.(T - S).| ^2 = Sum (sqr (T - S))
by SQUARE_1:def 4;
Sum (sqr (S - X)) >= 0
by RVSUM_1:116;
then A11:
|.(S - X).| ^2 = Sum (sqr (S - X))
by SQUARE_1:def 4;
y - x = S - X
by A1, EUCLID:73;
then
|.(y - x).| = sqrt (Sum (sqr (S - X)))
by A1, A9;
then
(sqrt (Sum (sqr (S - X)))) ^2 < r ^2
by A1, A9, SQUARE_1:78;
then A12:
(Sum (sqr (S - X))) - (r ^2 ) < 0
by A11, XREAL_1:51;
then A13:
((Sum (sqr (S - X))) - (r ^2 )) / (Sum (sqr (T - S))) < 0
by A8, XREAL_1:143;
A14:
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 )))
by QUIN_1:def 1;
A15:
(4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - X))) - (r ^2 )) < 0
by A8, A12, XREAL_1:131, XREAL_1:134;
(2 * |((z - y),(y - x))|) ^2 >= 0
by XREAL_1:65;
then A16:
((2 * |((z - y),(y - x))|) ^2 ) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - X))) - (r ^2 ))) > 0
by A15;
A17:
for x being real number 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 number ;
:: thesis: 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 A8, A14, 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
;
:: thesis: 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 A8, 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 A13, XREAL_1:135;
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); :: thesis: ( {e1} = (halfline y,z) /\ (Sphere x,r) & e1 = ((1 - a) * y) + (a * z) )
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 ))) =
(((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
;
SX:
( y - x = S - X & z - x = T - X & z - y = T - S )
by A1, EUCLID:73;
A20:
e1 in halfline y,z
by A8, A14, A16, A18, QUIN_1:27;
|.(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 EUCLID:54
.=
|.(((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 EUCLID:33
.=
|.(((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 JORDAN2C:9
.=
|.((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 EUCLID:49
.=
|.((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 JORDAN2C:9
.=
|.((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:53
.=
((|.(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:67
.=
((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 A1, A11, SX, EUCLID_2:41
.=
((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))|)) + (((abs (((- (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:8
.=
((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))|)) + (((abs (((- (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 ) * (|.(z - y).| ^2 ))
by A1, A10, SX, COMPLEX1:161
.=
((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, A10, SX, COMPLEX1:161
.=
((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 A1, A10, SX, COMPLEX1:161
.=
((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 A1, A10, SX, COMPLEX1:161
.=
((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 A1, A10, SX, COMPLEX1:161
.=
((((Sum (sqr (S - X))) - (r ^2 )) + (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))))) * (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 A1, A10, SX, COMPLEX1:161
.=
((((Sum (sqr (S - X))) - (r ^2 )) + (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))))) * (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 A1, A10, SX, COMPLEX1:161
.=
r ^2
by A19
;
then A21:
( |.(e1 - x).| = r or |.(e1 - x).| = - r )
by SQUARE_1:109;
( r = 0 or r <> 0 )
;
then A22:
e1 in Sphere x,r
by A6, A21;
hereby :: according to TARSKI:def 3 :: thesis: e1 = ((1 - a) * y) + (a * z)
let d be
set ;
:: thesis: ( d in (halfline y,z) /\ (Sphere x,r) implies d in {e1} )assume A23:
d in (halfline y,z) /\ (Sphere x,r)
;
:: thesis: d in {e1}then
d in halfline y,
z
by XBOOLE_0:def 4;
then consider l being
real number such that A24:
d = ((1 - l) * y) + (l * z)
and A25:
0 <= l
by Th26;
l is
Real
by XREAL_0:def 1;
then A26:
|.(l * (z - y)).| ^2 =
((abs l) * |.(z - y).|) ^2
by TOPRNS_1:8
.=
((abs l) ^2 ) * (|.(z - y).| ^2 )
.=
(l ^2 ) * (|.(z - y).| ^2 )
by COMPLEX1:161
;
d in Sphere x,
r
by A23, XBOOLE_0:def 4;
then r =
|.((((1 - l) * y) + (l * z)) - x).|
by A24, Th9
.=
|.((((1 * y) - (l * y)) + (l * z)) - x).|
by EUCLID:54
.=
|.(((y - (l * y)) + (l * z)) - x).|
by EUCLID:33
.=
|.((y - ((l * y) - (l * z))) - x).|
by EUCLID:51
.=
|.((y - x) - ((l * y) - (l * z))).|
by Th1
.=
|.((y - x) + (- (l * (y - z)))).|
by EUCLID:53
.=
|.((y - x) + (l * (- (y - z)))).|
by EUCLID:44
.=
|.((y - x) + (l * (z - y))).|
by EUCLID:48
;
then A27:
r ^2 =
((|.(y - x).| ^2 ) + (2 * |((l * (z - y)),(y - x))|)) + (|.(l * (z - y)).| ^2 )
by EUCLID_2:67
.=
((|.(y - x).| ^2 ) + (2 * (l * |((z - y),(y - x))|))) + (|.(l * (z - y)).| ^2 )
by EUCLID_2:41
;
(((Sum (sqr (T - S))) * (l ^2 )) + ((2 * |((z - y),(y - x))|) * l)) + ((Sum (sqr (S - X))) - (r ^2 )) = 0
by A1, A10, A11, A26, A27, SX;
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 A8, A14, A16, POLYEQ_1:5;
hence
d in {e1}
by A8, A14, A16, A18, A24, A25, QUIN_1:27, TARSKI:def 1;
:: thesis: verum
end;
thus
e1 = ((1 - a) * y) + (a * z)
by A4; :: thesis: verum