let x be Real; for y being non negative Real
for r, a being positive Real st a <= 1 holds
(+ (x,y,r)) " [.0,a.[ = (Ball (|[x,y]|,(r * a))) /\ y>=0-plane
let y be non negative Real; for r, a being positive Real st a <= 1 holds
(+ (x,y,r)) " [.0,a.[ = (Ball (|[x,y]|,(r * a))) /\ y>=0-plane
let r, a be positive Real; ( a <= 1 implies (+ (x,y,r)) " [.0,a.[ = (Ball (|[x,y]|,(r * a))) /\ y>=0-plane )
set f = + (x,y,r);
assume A1:
a <= 1
; (+ (x,y,r)) " [.0,a.[ = (Ball (|[x,y]|,(r * a))) /\ y>=0-plane
then
r * a <= r * 1
by XREAL_1:64;
then A2:
Ball (|[x,y]|,(r * a)) c= Ball (|[x,y]|,r)
by JORDAN:18;
thus
(+ (x,y,r)) " [.0,a.[ c= (Ball (|[x,y]|,(r * a))) /\ y>=0-plane
XBOOLE_0:def 10 (Ball (|[x,y]|,(r * a))) /\ y>=0-plane c= (+ (x,y,r)) " [.0,a.[proof
let u be
object ;
TARSKI:def 3 ( not u in (+ (x,y,r)) " [.0,a.[ or u in (Ball (|[x,y]|,(r * a))) /\ y>=0-plane )
assume A3:
u in (+ (x,y,r)) " [.0,a.[
;
u in (Ball (|[x,y]|,(r * a))) /\ y>=0-plane
then reconsider p =
u as
Point of
Niemytzki-plane ;
p in y>=0-plane
by Lm1;
then reconsider q =
p as
Element of
(TOP-REAL 2) ;
(+ (x,y,r)) . p in [.0,a.[
by A3, FUNCT_2:38;
then A4:
(+ (x,y,r)) . p < a
by XXREAL_1:3;
A5:
p = |[(q `1),(q `2)]|
by EUCLID:53;
then A6:
q `2 >= 0
by Lm1, Th18;
then
p in Ball (
|[x,y]|,
r)
by A4, A1, A5, Def6;
then
(+ (x,y,r)) . p = |.(|[x,y]| - q).| / r
by A5, A6, Def6;
then A7:
|.(|[x,y]| - q).| < r * a
by A4, XREAL_1:77;
|.(|[x,y]| - q).| = |.(q - |[x,y]|).|
by TOPRNS_1:27;
then
p in Ball (
|[x,y]|,
(r * a))
by A7, TOPREAL9:7;
hence
u in (Ball (|[x,y]|,(r * a))) /\ y>=0-plane
by Lm1, XBOOLE_0:def 4;
verum
end;
let u be object ; TARSKI:def 3 ( not u in (Ball (|[x,y]|,(r * a))) /\ y>=0-plane or u in (+ (x,y,r)) " [.0,a.[ )
assume A8:
u in (Ball (|[x,y]|,(r * a))) /\ y>=0-plane
; u in (+ (x,y,r)) " [.0,a.[
then reconsider p = u as Point of Niemytzki-plane by Lm1, XBOOLE_0:def 4;
reconsider q = p as Element of (TOP-REAL 2) by A8;
A9:
u in Ball (|[x,y]|,(r * a))
by A8, XBOOLE_0:def 4;
then A10:
|.(q - |[x,y]|).| < r * a
by TOPREAL9:7;
A11:
|.(|[x,y]| - q).| = |.(q - |[x,y]|).|
by TOPRNS_1:27;
A12:
p = |[(q `1),(q `2)]|
by EUCLID:53;
u in y>=0-plane
by A8, XBOOLE_0:def 4;
then
q `2 >= 0
by A12, Th18;
then A13:
(+ (x,y,r)) . p = |.(|[x,y]| - q).| / r
by A2, A9, A12, Def6;
then
r * ((+ (x,y,r)) . p) = |.(|[x,y]| - q).|
by XCMPLX_1:87;
then
(+ (x,y,r)) . p < a
by A10, A11, XREAL_1:64;
then
(+ (x,y,r)) . p in [.0,a.[
by A13, XXREAL_1:3;
hence
u in (+ (x,y,r)) " [.0,a.[
by FUNCT_2:38; verum