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)

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 ) )
;

end;

suppose
( not r is positive or not s is positive )
; :: thesis: circle (a,b,r) misses circle (a,b,s)

end;

per cases then
( r = 0 or r < 0 or s < 0 or s = 0 )
;

end;

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;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

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;hence circle (a,b,r) misses circle (a,b,s) ; :: thesis: verum

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;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

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;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