let a, b, r, s be Real; :: thesis: ( r <> s implies circle (a,b,r) misses circle (a,b,s) )
assume A1: r <> s ; :: thesis: circle (a,b,r) misses circle (a,b,s)
per cases ( not r is positive or not s is positive or ( r is positive & s is positive ) ) ;
suppose ( not r is positive or not s is positive ) ; :: thesis: circle (a,b,r) misses circle (a,b,s)
per cases then ( r = 0 or r < 0 or s < 0 or s = 0 ) ;
suppose A2: r = 0 ; :: thesis: circle (a,b,r) misses circle (a,b,s)
then A3: circle (a,b,r) = {|[a,b]|} by EUCLID10:36;
assume circle (a,b,r) meets circle (a,b,s) ; :: thesis: contradiction
then consider p being object such that
A4: p in circle (a,b,r) and
A5: p in circle (a,b,s) by XBOOLE_0:3;
p in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = s } by A5, JGRAPH_6:def 5;
then consider p1 being Point of (TOP-REAL 2) such that
A6: p = p1 and
A7: |.(p1 - |[a,b]|).| = s ;
s = |.(|[a,b]| - |[a,b]|).| by A6, A7, A4, A3, TARSKI:def 1
.= 0 by EUCLID_6:42 ;
hence contradiction by A2, A1; :: thesis: verum
end;
suppose ( r < 0 or s < 0 ) ; :: thesis: circle (a,b,r) misses circle (a,b,s)
then ( circle (a,b,r) is empty or circle (a,b,s) is empty ) ;
hence circle (a,b,r) misses circle (a,b,s) ; :: thesis: verum
end;
suppose A8: s = 0 ; :: thesis: circle (a,b,r) misses circle (a,b,s)
then A9: circle (a,b,s) = {|[a,b]|} by EUCLID10:36;
assume circle (a,b,r) meets circle (a,b,s) ; :: thesis: contradiction
then consider p being object such that
A10: p in circle (a,b,s) and
A11: p in circle (a,b,r) by XBOOLE_0:3;
p in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } by A11, JGRAPH_6:def 5;
then consider p1 being Point of (TOP-REAL 2) such that
A12: p = p1 and
A13: |.(p1 - |[a,b]|).| = r ;
r = |.(|[a,b]| - |[a,b]|).| by A12, A13, A10, A9, TARSKI:def 1
.= 0 by EUCLID_6:42 ;
hence contradiction by A8, A1; :: thesis: verum
end;
end;
end;
suppose ( r is positive & s is positive ) ; :: thesis: circle (a,b,r) misses circle (a,b,s)
assume circle (a,b,r) meets circle (a,b,s) ; :: thesis: contradiction
then consider p being object such that
A15: p in circle (a,b,r) and
A16: p in circle (a,b,s) by XBOOLE_0:3;
p in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } by A15, JGRAPH_6:def 5;
then consider p1 being Point of (TOP-REAL 2) such that
A17: p = p1 and
A18: |.(p1 - |[a,b]|).| = r ;
p in { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = s } by A16, JGRAPH_6:def 5;
then consider p2 being Point of (TOP-REAL 2) such that
A19: p = p2 and
A20: |.(p2 - |[a,b]|).| = s ;
thus contradiction by A17, A19, A18, A1, A20; :: thesis: verum
end;
end;