let a be Real; :: thesis: for r being non negative Real
for r1, r2, s1, s2 being Real
for s, t, o being Point of (TOP-REAL 2) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) holds
HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
let r be non negative Real; :: thesis: for r1, r2, s1, s2 being Real
for s, t, o being Point of (TOP-REAL 2) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) holds
HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
let r1, r2, s1, s2 be Real; :: thesis: for s, t, o being Point of (TOP-REAL 2) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) holds
HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
let s, t, o be Point of (TOP-REAL 2); :: thesis: ( s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) implies HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| )
assume that
A1: s is Point of (Tdisk (o,r)) and
A2: t is Point of (Tdisk (o,r)) and
A3: s <> t and
A4: ( r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) ) and
A5: s1 = (s `1) - (o `1) and
A6: s2 = (s `2) - (o `2) and
A7: a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) ; :: thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3;
then |.(s - o).| <= r by A1, TOPREAL9:8;
then A8: |.(s - o).| ^2 <= r ^2 by SQUARE_1:15;
set C = ((s1 ^2) + (s2 ^2)) - (r ^2);
set A = (r1 ^2) + (r2 ^2);
set M = (s1 * r1) + (s2 * r2);
set B = 2 * ((s1 * r1) + (s2 * r2));
set l1 = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)));
set l2 = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)));
A9: delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))) = ((2 * ((s1 * r1) + (s2 * r2))) ^2) - ((4 * ((r1 ^2) + (r2 ^2))) * (((s1 ^2) + (s2 ^2)) - (r ^2))) by QUIN_1:def 1;
|.(s - o).| ^2 = (((s - o) `1) ^2) + (((s - o) `2) ^2) by JGRAPH_1:29
.= (s1 ^2) + (((s - o) `2) ^2) by A5, TOPREAL3:3
.= (s1 ^2) + (s2 ^2) by A6, TOPREAL3:3 ;
then A10: ((s1 ^2) + (s2 ^2)) - (r ^2) <= (r ^2) - (r ^2) by A8, XREAL_1:9;
then A11: ((2 * ((s1 * r1) + (s2 * r2))) ^2) - ((4 * ((r1 ^2) + (r2 ^2))) * (((s1 ^2) + (s2 ^2)) - (r ^2))) >= 0 ;
( r1 <> 0 or r2 <> 0 ) by A3, A4, TOPREAL3:6;
then A13: 0 + 0 < (r1 ^2) + (r2 ^2) by SQUARE_1:12, XREAL_1:8;
for x being Real holds Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),x) = Quard (((r1 ^2) + (r2 ^2)),(((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),(((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),x) then A14: (((s1 ^2) + (s2 ^2)) - (r ^2)) / ((r1 ^2) + (r2 ^2)) = (((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))) * (((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))) by A13, POLYEQ_1:11;
delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))) = ((2 * ((s1 * r1) + (s2 * r2))) ^2) - ((4 * ((r1 ^2) + (r2 ^2))) * (((s1 ^2) + (s2 ^2)) - (r ^2))) by QUIN_1:def 1
.= 4 * ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))) ;
then A15: ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) + ((sqrt 4) * (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2))))))) / (2 * ((r1 ^2) + (r2 ^2))) by A10, SQUARE_1:29
.= (2 * (- (((s1 * r1) + (s2 * r2)) - (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))))) / (2 * ((r1 ^2) + (r2 ^2))) by SQUARE_1:20
.= a by A7, XCMPLX_1:91 ;
set H = HC (s,t,o,r);
A16: HC (s,t,o,r) in (halfline (s,t)) /\ (Sphere (o,r)) by A1, A2, A3, Def3;
then HC (s,t,o,r) in halfline (s,t) by XBOOLE_0:def 4;
then consider l being Real such that
A17: HC (s,t,o,r) = ((1 - l) * s) + (l * t) and
A18: 0 <= l by TOPREAL9:26;
A19: HC (s,t,o,r) = ((1 * s) - (l * s)) + (l * t) by A17, 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 ;
then A20: (HC (s,t,o,r)) `1 = (s `1) + ((l * (t - s)) `1) by TOPREAL3:2
.= (s `1) + (l * ((t - s) `1)) by TOPREAL3:4
.= (s `1) + (l * ((t `1) - (s `1))) by TOPREAL3:3 ;
HC (s,t,o,r) in Sphere (o,r) by A16, XBOOLE_0:def 4;
then |.((HC (s,t,o,r)) - o).| = r by TOPREAL9:9;
then r ^2 = ((((HC (s,t,o,r)) - o) `1) ^2) + ((((HC (s,t,o,r)) - o) `2) ^2) by JGRAPH_1:29
.= ((((HC (s,t,o,r)) `1) - (o `1)) ^2) + ((((HC (s,t,o,r)) - o) `2) ^2) by TOPREAL3:3
.= ((((HC (s,t,o,r)) `1) - (o `1)) ^2) + ((((HC (s,t,o,r)) `2) - (o `2)) ^2) by TOPREAL3:3
.= (((((1 - l) * (s `1)) + (l * (t `1))) - (o `1)) ^2) + ((((HC (s,t,o,r)) `2) - (o `2)) ^2) by A17, TOPREAL9:41
.= (((((1 - l) * (s `1)) + (l * (t `1))) - (o `1)) ^2) + (((((1 - l) * (s `2)) + (l * (t `2))) - (o `2)) ^2) by A17, TOPREAL9:42
.= ((((l ^2) * ((r1 ^2) + (r2 ^2))) + ((l * 2) * ((s1 * r1) + (s2 * r2)))) + (s1 ^2)) + (s2 ^2) by A4, A5, A6 ;
then ((((r1 ^2) + (r2 ^2)) * (l ^2)) + ((2 * ((s1 * r1) + (s2 * r2))) * l)) + (((s1 ^2) + (s2 ^2)) - (r ^2)) = 0 ;
then Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),l) = 0 by POLYEQ_1:def 2;
then A21: ( l = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) or l = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ) by A13, A9, A10, POLYEQ_1:5;
A22: (HC (s,t,o,r)) `2 = (s `2) + ((l * (t - s)) `2) by A19, TOPREAL3:2
.= (s `2) + (l * ((t - s) `2)) by TOPREAL3:4
.= (s `2) + (l * ((t `2) - (s `2))) by TOPREAL3:3 ;