let a be Real; :: thesis: for r being non negative Real
for n being non zero Element of NAT
for s, t, o being Point of (TOP-REAL n)
for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) holds
HC (s,t,o,r) = ((1 - a) * s) + (a * t)
let r be non negative Real; :: thesis: for n being non zero Element of NAT
for s, t, o being Point of (TOP-REAL n)
for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) holds
HC (s,t,o,r) = ((1 - a) * s) + (a * t)
let n be non zero Element of NAT ; :: thesis: for s, t, o being Point of (TOP-REAL n)
for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) holds
HC (s,t,o,r) = ((1 - a) * s) + (a * t)
let s, t, o be Point of (TOP-REAL n); :: thesis: for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) holds
HC (s,t,o,r) = ((1 - a) * s) + (a * t)
let S, T, O be Element of REAL n; :: thesis: ( S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) implies HC (s,t,o,r) = ((1 - a) * s) + (a * t) )
assume that
A1: S = s and
A2: T = t and
A3: O = o and
A4: s is Point of (Tdisk (o,r)) and
A5: t is Point of (Tdisk (o,r)) and
A6: s <> t ; :: thesis: ( not a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) or HC (s,t,o,r) = ((1 - a) * s) + (a * t) )
A7: ( |.(T - S).| = sqrt (Sum (sqr (T - S))) & Sum (sqr (T - S)) >= 0 ) by EUCLID:def 5, RVSUM_1:86;
set H = HC (s,t,o,r);
A8: HC (s,t,o,r) in (halfline (s,t)) /\ (Sphere (o,r)) by A4, A5, A6, Def3;
then HC (s,t,o,r) in halfline (s,t) by XBOOLE_0:def 4;
then consider l being Real such that
A9: HC (s,t,o,r) = ((1 - l) * s) + (l * t) and
A10: 0 <= l by TOPREAL9:26;
HC (s,t,o,r) in Sphere (o,r) by A8, XBOOLE_0:def 4;
then r = |.((((1 - l) * s) + (l * t)) - o).| by A9, TOPREAL9:9
.= |.((((1 * s) - (l * s)) + (l * t)) - o).| by RLVECT_1:35
.= |.(((s - (l * s)) + (l * t)) - o).| by RLVECT_1:def 8
.= |.((s - ((l * s) - (l * t))) - o).| by RLVECT_1:29
.= |.((s + (- ((l * s) - (l * t)))) + (- o)).|
.= |.((s + (- o)) + (- ((l * s) - (l * t)))).| by RLVECT_1:def 3
.= |.((s - o) - ((l * s) - (l * t))).|
.= |.((s - o) + (- (l * (s - t)))).| by RLVECT_1:34
.= |.((s - o) + (l * (- (s - t)))).| by RLVECT_1:25
.= |.((s - o) + (l * (t - s))).| by RLVECT_1:33 ;
then A11: r ^2 = ((|.(s - o).| ^2) + (2 * |((l * (t - s)),(s - o))|)) + (|.(l * (t - s)).| ^2) by EUCLID_2:45
.= ((|.(s - o).| ^2) + (2 * (l * |((t - s),(s - o))|))) + (|.(l * (t - s)).| ^2) by EUCLID_2:19 ;
set A = Sum (sqr (T - S));
A12: |.(T - S).| <> 0 by A1, A2, A6, EUCLID:16;

A13: now :: thesis: not Sum (sqr (T - S)) <= 0

assume Sum (sqr (T - S)) <= 0 ; :: thesis: contradiction
then Sum (sqr (T - S)) = 0 by RVSUM_1:86;
hence contradiction by A12, EUCLID:def 5, SQUARE_1:17; :: thesis: verum

end;

set C = (Sum (sqr (S - O))) - (r ^2);
set M = |((t - s),(s - o))|;
set B = 2 * |((t - s),(s - o))|;
set l1 = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
set l2 = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
A14: |.(S - O).| = sqrt (Sum (sqr (S - O))) by EUCLID:def 5;
Sum (sqr (S - O)) >= 0 by RVSUM_1:86;
then A15: |.(S - O).| ^2 = Sum (sqr (S - O)) by A14, SQUARE_1:def 2;
A16: delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2))) = ((2 * |((t - s),(s - o))|) ^2) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - O))) - (r ^2))) by QUIN_1:def 1;
the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3;
then |.(s - o).| <= r by A4, TOPREAL9:8;
then A17: (sqrt (Sum (sqr (S - O)))) ^2 <= r ^2 by A1, A3, A14, SQUARE_1:15;
then A18: (Sum (sqr (S - O))) - (r ^2) <= 0 by A14, A15, XREAL_1:47;

now :: thesis: for x being Real holds Polynom ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)),x) = Quard ((Sum (sqr (T - S))),(((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x)

let x be Real; :: thesis: Polynom ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)),x) = Quard ((Sum (sqr (T - S))),(((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x)
thus Polynom ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)),x) = (((Sum (sqr (T - S))) * (x ^2)) + ((2 * |((t - s),(s - o))|) * x)) + ((Sum (sqr (S - O))) - (r ^2)) by POLYEQ_1:def 2
.= ((Sum (sqr (T - S))) * (x - (((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) * (x - (((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) by A13, A18, A16, QUIN_1:16
.= (Sum (sqr (T - S))) * ((x - (((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * (x - (((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))))
.= Quard ((Sum (sqr (T - S))),(((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x) by POLYEQ_1:def 3 ; :: thesis: verum

end;

then A19: ((Sum (sqr (S - O))) - (r ^2)) / (Sum (sqr (T - S))) = (((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) by A13, POLYEQ_1:11;

A20: now :: thesis: not ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) > ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))

set D = sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2))));
assume ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) > ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ; :: thesis: contradiction
then (- (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) - (2 * |((t - s),(s - o))|) > (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2))))) - (2 * |((t - s),(s - o))|) by A13, XREAL_1:72;
hence contradiction by A13, A18, A16, XREAL_1:9; :: thesis: verum

end;

assume A21: a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) ; :: thesis: HC (s,t,o,r) = ((1 - a) * s) + (a * t)
delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2))) = ((2 * |((t - s),(s - o))|) ^2) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - O))) - (r ^2))) by QUIN_1:def 1
.= 4 * ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))) ;
then A22: ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) + ((sqrt 4) * (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2))))))) / (2 * (Sum (sqr (T - S)))) by A13, A18, SQUARE_1:29
.= (2 * (- (|((t - s),(s - o))| - (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))))) / (2 * (Sum (sqr (T - S)))) by SQUARE_1:20
.= a by A21, XCMPLX_1:91 ;
A23: HC (s,t,o,r) = ((1 * s) - (l * s)) + (l * t) by A9, RLVECT_1:35
.= (s - (l * s)) + (l * t) by RLVECT_1:def 8
.= (s + (l * t)) - (l * s) by RLVECT_1:def 3
.= s + ((l * t) - (l * s)) by RLVECT_1:def 3
.= s + (l * (t - s)) by RLVECT_1:34 ;
A24: |.(l * (t - s)).| ^2 = (|.l.| * |.(t - s).|) ^2 by TOPRNS_1:7
.= (|.l.| ^2) * (|.(t - s).| ^2)
.= (l ^2) * (|.(t - s).| ^2) by COMPLEX1:75 ;
(((Sum (sqr (T - S))) * (l ^2)) + ((2 * |((t - s),(s - o))|) * l)) + ((Sum (sqr (S - O))) - (r ^2)) = (((Sum (sqr (T - S))) * (l ^2)) + ((2 * |((t - s),(s - o))|) * l)) + ((Sum (sqr (S - O))) - (r ^2))
.= (((|.(T - S).| ^2) * (l ^2)) + ((2 * |((t - s),(s - o))|) * l)) + ((|.(S - O).| ^2) - (r ^2)) by A7, A15, SQUARE_1:def 2
.= (((|.(t - s).| ^2) * (l ^2)) + ((2 * |((t - s),(s - o))|) * l)) + ((|.(s - o).| ^2) - (r ^2)) by A1, A2, A3
.= 0 by A24, A11 ;
then Polynom ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)),l) = 0 by POLYEQ_1:def 2;
then A25: ( l = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) or l = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ) by A13, A18, A16, POLYEQ_1:5;

per cases ( (Sum (sqr (S - O))) - (r ^2) < 0 or ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) or (Sum (sqr (S - O))) - (r ^2) = 0 ) by A14, A15, A17, XREAL_1:47;

suppose (Sum (sqr (S - O))) - (r ^2) < 0 ; :: thesis: HC (s,t,o,r) = ((1 - a) * s) + (a * t)

hence HC (s,t,o,r) = ((1 - a) * s) + (a * t) by A9, A10, A13, A22, A25, A19, A20, XREAL_1:141; :: thesis: verum

end;

suppose ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ; :: thesis: HC (s,t,o,r) = ((1 - a) * s) + (a * t)

hence HC (s,t,o,r) = ((1 - a) * s) + (a * t) by A9, A22, A25; :: thesis: verum

end;

suppose A26: (Sum (sqr (S - O))) - (r ^2) = 0 ; :: thesis: HC (s,t,o,r) = ((1 - a) * s) + (a * t)

now :: thesis: not l = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))

A27: now :: thesis: not l = 0

assume l = 0 ; :: thesis: contradiction
then HC (s,t,o,r) = s + (0. (TOP-REAL n)) by A23, RLVECT_1:10
.= s by RLVECT_1:4 ;
hence contradiction by A4, A5, A6, Def3; :: thesis: verum

end;

assume A28: l = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ; :: thesis: contradiction

per cases ( 0 < 2 * |((t - s),(s - o))| or 2 * |((t - s),(s - o))| <= 0 ) ;

suppose A29: 0 < 2 * |((t - s),(s - o))| ; :: thesis: contradiction

then ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) - (2 * |((t - s),(s - o))|)) / (2 * (Sum (sqr (T - S)))) by A16, A26, SQUARE_1:22;
hence contradiction by A10, A13, A28, A29, XREAL_1:129, XREAL_1:141; :: thesis: verum

end;

suppose 2 * |((t - s),(s - o))| <= 0 ; :: thesis: contradiction

then ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) - (- (2 * |((t - s),(s - o))|))) / (2 * (Sum (sqr (T - S)))) by A16, A26, SQUARE_1:23
.= 0 ;
hence contradiction by A28, A27; :: thesis: verum

end;

end;

end;

hence HC (s,t,o,r) = ((1 - a) * s) + (a * t) by A9, A22, A25; :: thesis: verum

end;

end;