let a, b, r be Real; ( r > 0 & b >= 0 implies ( Ball (|[a,b]|,r) misses y=0-line iff r <= b ) )
assume that
A1:
r > 0
and
A2:
b >= 0
; ( Ball (|[a,b]|,r) misses y=0-line iff r <= b )
hereby ( r <= b implies Ball (|[a,b]|,r) misses y=0-line )
A3:
|[a,0]| in y=0-line
;
assume that A4:
Ball (
|[a,b]|,
r)
misses y=0-line
and A5:
r > b
;
contradiction
|[a,0]| - |[a,b]| = |[(a - a),(0 - b)]|
by EUCLID:62;
then |.(|[a,0]| - |[a,b]|).| =
|.(0 - b).|
by TOPREAL6:23
.=
|.(b - 0).|
by COMPLEX1:60
;
then
|.(|[a,0]| - |[a,b]|).| < r
by A2, A5, ABSVALUE:def 1;
then
|[a,0]| in Ball (
|[a,b]|,
r)
by TOPREAL9:7;
hence
contradiction
by A3, A4, XBOOLE_0:3;
verum
end;
assume A6:
r <= b
; Ball (|[a,b]|,r) misses y=0-line
assume
Ball (|[a,b]|,r) meets y=0-line
; contradiction
then consider x being object such that
A7:
x in Ball (|[a,b]|,r)
and
A8:
x in y=0-line
by XBOOLE_0:3;
reconsider x = x as Element of (TOP-REAL 2) by A7;
A9:
x = |[(x `1),(x `2)]|
by EUCLID:53;
then
x `2 = 0
by A8, Th15;
then A10:
x - |[a,b]| = |[((x `1) - a),(0 - b)]|
by A9, EUCLID:62;
then A11:
(x - |[a,b]|) `2 = 0 - b
by EUCLID:52;
(x - |[a,b]|) `1 = (x `1) - a
by A10, EUCLID:52;
then
|.(x - |[a,b]|).| = sqrt ((((x `1) - a) ^2) + ((0 - b) ^2))
by A11, JGRAPH_1:30;
then
|.(x - |[a,b]|).| >= |.(0 - b).|
by COMPLEX1:79;
then A12:
|.(x - |[a,b]|).| >= |.(b - 0).|
by COMPLEX1:60;
|.(x - |[a,b]|).| < r
by A7, TOPREAL9:7;
then
|.b.| < r
by A12, XXREAL_0:2;
hence
contradiction
by A1, A6, ABSVALUE:def 1; verum