let a, b, r be real number ; :: thesis: ( r > 0 implies ( Ball |[a,b]|,r c= y>=0-plane iff r <= b ) )
assume A1:
r > 0
; :: thesis: ( Ball |[a,b]|,r c= y>=0-plane iff r <= b )
hereby :: thesis: ( r <= b implies Ball |[a,b]|,r c= y>=0-plane )
assume that A2:
Ball |[a,b]|,
r c= y>=0-plane
and A3:
r > b
;
:: thesis: contradiction
|[a,b]| in Ball |[a,b]|,
r
by A1, Th17;
then reconsider b =
b as non
negative Real by A2, Th22, XREAL_0:def 1;
reconsider br =
b - r as
negative Real by A3, XREAL_1:51;
reconsider r =
r as
positive Real by A1, XREAL_0:def 1;
b + r < r + r
by A3, XREAL_1:8;
then A4:
(b + r) / 2
< (r + r) / 2
by XREAL_1:76;
set y =
br / 2;
(
|[a,(br / 2)]| - |[a,b]| = |[(a - a),((br / 2) - b)]| &
(br / 2) - b is
Real )
by EUCLID:66;
then |.(|[a,(br / 2)]| - |[a,b]|).| =
|.((br / 2) - b).|
by TOPREAL6:31
.=
|.(b - (br / 2)).|
by COMPLEX1:146
.=
(b + r) / 2
by ABSVALUE:def 1
;
then
|[a,(br / 2)]| in Ball |[a,b]|,
r
by A4, TOPREAL9:7;
hence
contradiction
by A2, Th22;
:: thesis: verum
end;
assume A5:
r <= b
; :: thesis: Ball |[a,b]|,r c= y>=0-plane
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball |[a,b]|,r or x in y>=0-plane )
assume A6:
x in Ball |[a,b]|,r
; :: thesis: x in y>=0-plane
then reconsider z = x as Element of (TOP-REAL 2) ;
A7:
z = |[(z `1 ),(z `2 )]|
by EUCLID:57;
then
( z - |[a,b]| = |[((z `1 ) - a),((z `2 ) - b)]| & |[((z `1 ) - a),((z `2 ) - b)]| `1 = (z `1 ) - a & |[((z `1 ) - a),((z `2 ) - b)]| `2 = (z `2 ) - b )
by EUCLID:56, EUCLID:66;
then
( (z `1 ) - a is Real & (z `2 ) - b is Real & |.(z - |[a,b]|).| = sqrt ((((z `1 ) - a) ^2 ) + (((z `2 ) - b) ^2 )) )
by JGRAPH_1:47;
then
( abs ((z `2 ) - b) <= |.(z - |[a,b]|).| & |.(z - |[a,b]|).| < r )
by A6, COMPLEX1:165, TOPREAL9:7;
then
abs ((z `2 ) - b) < r
by XXREAL_0:2;
then A8:
abs (b - (z `2 )) < r
by COMPLEX1:146;
hence
x in y>=0-plane
by A7; :: thesis: verum