let a be real number ; :: thesis: for r being non negative real number
for r1, r2, s1, s2 being real number
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 number ; :: thesis: for r1, r2, s1, s2 being real number
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 number ; :: 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 ) and
A5: r2 = (t `2 ) - (s `2 ) and
A6: s1 = (s `1 ) - (o `1 ) and
A7: s2 = (s `2 ) - (o `2 ) and
A8: 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))]|
set H = HC s,t,o,r;
set M = (s1 * r1) + (s2 * r2);
set A = (r1 ^2 ) + (r2 ^2 );
set B = 2 * ((s1 * r1) + (s2 * r2));
set C = ((s1 ^2 ) + (s2 ^2 )) - (r ^2 );
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: 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 number such that
A10: HC s,t,o,r = ((1 - l) * s) + (l * t) and
A11: 0 <= l by TOPREAL9:26;
A12: HC s,t,o,r = ((1 * s) - (l * s)) + (l * t) by A10, EUCLID:54
.= (s - (l * s)) + (l * t) by EUCLID:33
.= (s + (l * t)) - (l * s) by JORDAN2C:9
.= s + ((l * t) - (l * s)) by EUCLID:49
.= s + (l * (t - s)) by EUCLID:53 ;
then A13: (HC s,t,o,r) `1 = (s `1 ) + ((l * (t - s)) `1 ) by TOPREAL3:7
.= (s `1 ) + (l * ((t - s) `1 )) by TOPREAL3:9
.= (s `1 ) + (l * ((t `1 ) - (s `1 ))) by TOPREAL3:8 ;
A14: (HC s,t,o,r) `2 = (s `2 ) + ((l * (t - s)) `2 ) by A12, TOPREAL3:7
.= (s `2 ) + (l * ((t - s) `2 )) by TOPREAL3:9
.= (s `2 ) + (l * ((t `2 ) - (s `2 ))) by TOPREAL3:8 ;
( r1 <> 0 or r2 <> 0 ) by A3, A4, A5, TOPREAL3:11;
then A15: 0 + 0 < (r1 ^2 ) + (r2 ^2 ) by SQUARE_1:74, XREAL_1:10;
A16: 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 )))) ;
A17: 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;
HC s,t,o,r in Sphere o,r by A9, 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:46
.= ((((HC s,t,o,r) `1 ) - (o `1 )) ^2 ) + ((((HC s,t,o,r) - o) `2 ) ^2 ) by TOPREAL3:8
.= ((((HC s,t,o,r) `1 ) - (o `1 )) ^2 ) + ((((HC s,t,o,r) `2 ) - (o `2 )) ^2 ) by TOPREAL3:8
.= (((((1 - l) * (s `1 )) + (l * (t `1 ))) - (o `1 )) ^2 ) + ((((HC s,t,o,r) `2 ) - (o `2 )) ^2 ) by A10, TOPREAL9:41
.= (((((1 - l) * (s `1 )) + (l * (t `1 ))) - (o `1 )) ^2 ) + (((((1 - l) * (s `2 )) + (l * (t `2 ))) - (o `2 )) ^2 ) by A10, TOPREAL9:42
.= ((((l ^2 ) * ((r1 ^2 ) + (r2 ^2 ))) + ((l * 2) * ((s1 * r1) + (s2 * r2)))) + (s1 ^2 )) + (s2 ^2 ) by A4, A5, A6, A7 ;
then ((((r1 ^2 ) + (r2 ^2 )) * (l ^2 )) + ((2 * ((s1 * r1) + (s2 * r2))) * l)) + (((s1 ^2 ) + (s2 ^2 )) - (r ^2 )) = 0 ;
then A18: Polynom ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 )),l = 0 by POLYEQ_1:def 2;
the carrier of (Tdisk o,r) = cl_Ball o,r by Th3;
then |.(s - o).| <= r by A1, TOPREAL9:8;
then A19: |.(s - o).| ^2 <= r ^2 by SQUARE_1:77;
|.(s - o).| ^2 = (((s - o) `1 ) ^2 ) + (((s - o) `2 ) ^2 ) by JGRAPH_1:46
.= (s1 ^2 ) + (((s - o) `2 ) ^2 ) by A6, TOPREAL3:8
.= (s1 ^2 ) + (s2 ^2 ) by A7, TOPREAL3:8 ;
then A20: ((s1 ^2 ) + (s2 ^2 )) - (r ^2 ) <= (r ^2 ) - (r ^2 ) by A19, XREAL_1:11;
then ((r1 ^2 ) + (r2 ^2 )) * (((s1 ^2 ) + (s2 ^2 )) - (r ^2 )) <= 0 ;
then - 0 <= - (((r1 ^2 ) + (r2 ^2 )) * (((s1 ^2 ) + (s2 ^2 )) - (r ^2 ))) ;
then 0 + 0 <= (((s1 * r1) + (s2 * r2)) ^2 ) + (- (((r1 ^2 ) + (r2 ^2 )) * (((s1 ^2 ) + (s2 ^2 )) - (r ^2 )))) ;
then A21: ((- (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 A16, SQUARE_1:97
.= (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:85
.= a by A8, XCMPLX_1:92 ;
(4 * ((r1 ^2 ) + (r2 ^2 ))) * (((s1 ^2 ) + (s2 ^2 )) - (r ^2 )) <= 0 by A20;
then A22: ((2 * ((s1 * r1) + (s2 * r2))) ^2 ) - ((4 * ((r1 ^2 ) + (r2 ^2 ))) * (((s1 ^2 ) + (s2 ^2 )) - (r ^2 ))) >= 0 ;
then A23: ( 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 A15, A17, A18, POLYEQ_1:5;
for x being real number 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

proof

let x be real number ; :: thesis: 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
thus Polynom ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 )),x = ((((r1 ^2 ) + (r2 ^2 )) * (x ^2 )) + ((2 * ((s1 * r1) + (s2 * r2))) * x)) + (((s1 ^2 ) + (s2 ^2 )) - (r ^2 )) by POLYEQ_1:def 2
.= (((r1 ^2 ) + (r2 ^2 )) * (x - (((- (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 - (((- (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 A15, A17, A22, QUIN_1:16
.= ((r1 ^2 ) + (r2 ^2 )) * ((x - (((- (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 - (((- (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 ))))))
.= 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 by POLYEQ_1:def 3 ; :: thesis: verum

end;

then A24: (((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 A15, POLYEQ_1:11;
A25: 2 * ((r1 ^2 ) + (r2 ^2 )) > 0 by A15, XREAL_1:131;

A26: now

set D = sqrt (delta ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 )));
assume ((- (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 ))) ; :: thesis: contradiction
then (- (sqrt (delta ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 ))))) - (2 * ((s1 * r1) + (s2 * r2))) > (sqrt (delta ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 )))) - (2 * ((s1 * r1) + (s2 * r2))) by XREAL_1:74;
then - (sqrt (delta ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 )))) > sqrt (delta ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 ))) by XREAL_1:11;
then A27: (- (sqrt (delta ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 ))))) + (sqrt (delta ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 )))) > (sqrt (delta ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 )))) + (sqrt (delta ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 )))) by XREAL_1:8;
0 <= sqrt (delta ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 ))) by A17, A22;
then 0 + 0 <= (sqrt (delta ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 )))) + (sqrt (delta ((r1 ^2 ) + (r2 ^2 )),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2 ) + (s2 ^2 )) - (r ^2 )))) ;
hence contradiction by A27; :: thesis: verum

end;

per cases ( ((s1 ^2 ) + (s2 ^2 )) - (r ^2 ) < 0 or ((- (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 ))) or ((s1 ^2 ) + (s2 ^2 )) - (r ^2 ) = 0 ) by A20;

suppose ((s1 ^2 ) + (s2 ^2 )) - (r ^2 ) < 0 ; :: thesis: HC s,t,o,r = |[((s `1 ) + (a * r1)),((s `2 ) + (a * r2))]|

then (((s1 ^2 ) + (s2 ^2 )) - (r ^2 )) / ((r1 ^2 ) + (r2 ^2 )) < 0 by A15, XREAL_1:143;
hence HC s,t,o,r = |[((s `1 ) + (a * r1)),((s `2 ) + (a * r2))]| by A4, A5, A11, A13, A14, A21, A23, A24, A26, EUCLID:57; :: thesis: verum

end;

suppose ((- (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 ))) ; :: thesis: HC s,t,o,r = |[((s `1 ) + (a * r1)),((s `2 ) + (a * r2))]|

hence HC s,t,o,r = |[((s `1 ) + (a * r1)),((s `2 ) + (a * r2))]| by A4, A5, A13, A14, A21, A23, EUCLID:57; :: thesis: verum

end;

suppose A28: ((s1 ^2 ) + (s2 ^2 )) - (r ^2 ) = 0 ; :: thesis: HC s,t,o,r = |[((s `1 ) + (a * r1)),((s `2 ) + (a * r2))]|

now

assume A29: 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 ))) ; :: thesis: contradiction

A30: now

assume l = 0 ; :: thesis: contradiction
then HC s,t,o,r = s + (0. (TOP-REAL 2)) by A12, EUCLID:33
.= s by EUCLID:31 ;
hence contradiction by A1, A2, A3, Def3; :: thesis: verum

end;

per cases ( 0 < 2 * ((s1 * r1) + (s2 * r2)) or 2 * ((s1 * r1) + (s2 * r2)) <= 0 ) ;

suppose A31: 0 < 2 * ((s1 * r1) + (s2 * r2)) ; :: thesis: contradiction

then A32: (- 2) * (2 * ((s1 * r1) + (s2 * r2))) < 0 by XREAL_1:134;
((- (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)))) - (2 * ((s1 * r1) + (s2 * r2)))) / (2 * ((r1 ^2 ) + (r2 ^2 ))) by A17, A28, A31, SQUARE_1:89;
hence contradiction by A11, A25, A29, A32, XREAL_1:143; :: thesis: verum

end;

suppose 2 * ((s1 * r1) + (s2 * r2)) <= 0 ; :: thesis: contradiction

then ((- (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)))) - (- (2 * ((s1 * r1) + (s2 * r2))))) / (2 * ((r1 ^2 ) + (r2 ^2 ))) by A17, A28, SQUARE_1:90
.= 0 ;
hence contradiction by A29, A30; :: thesis: verum

end;

end;

end;

hence HC s,t,o,r = |[((s `1 ) + (a * r1)),((s `2 ) + (a * r2))]| by A4, A5, A13, A14, A21, A23, EUCLID:57; :: thesis: verum

end;

end;