let n be Element of NAT ; :: thesis: for a, b, r being real number
for x, z, y being Point of (TOP-REAL n) st a + b = 1 & (abs a) + (abs b) = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) holds
(a * x) + (b * y) in Ball (z,r)
let a, b, r be real number ; :: thesis: for x, z, y being Point of (TOP-REAL n) st a + b = 1 & (abs a) + (abs b) = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) holds
(a * x) + (b * y) in Ball (z,r)
let x, z, y be Point of (TOP-REAL n); :: thesis: ( a + b = 1 & (abs a) + (abs b) = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) implies (a * x) + (b * y) in Ball (z,r) )
assume that
A1: a + b = 1 and
A2: (abs a) + (abs b) = 1 and
A3: b <> 0 and
A4: x in cl_Ball (z,r) and
A5: y in Ball (z,r) ; :: thesis: (a * x) + (b * y) in Ball (z,r)
|.(y - z).| < r by A5, Th7;
then A6: |.(z - y).| < r by TOPRNS_1:27;
|.(x - z).| <= r by A4, Th8;
then ( 0 <= abs a & |.(z - x).| <= r ) by COMPLEX1:46, TOPRNS_1:27;
then A7: (abs a) * |.(z - x).| <= (abs a) * r by XREAL_1:64;
0 < abs b by A3, COMPLEX1:47;
then (abs b) * |.(z - y).| < (abs b) * r by A6, XREAL_1:68;
then ((abs a) * |.(z - x).|) + ((abs b) * |.(z - y).|) < ((abs a) * r) + ((abs b) * r) by A7, XREAL_1:8;
then ( a is Real & ((abs a) * |.(z - x).|) + ((abs b) * |.(z - y).|) < ((abs a) + (abs b)) * r ) by XREAL_0:def 1;
then ( b is Real & |.(a * (z - x)).| + ((abs b) * |.(z - y).|) < 1 * r ) by A2, TOPRNS_1:7, XREAL_0:def 1;
then A8: |.(a * (z - x)).| + |.(b * (z - y)).| < r by TOPRNS_1:7;
|.(((a * z) + (b * z)) - ((a * x) + (b * y))).| = |.(((a * z) - ((a * x) + (b * y))) + (b * z)).| by JORDAN2C:7
.= |.((((a * z) - (a * x)) - (b * y)) + (b * z)).| by EUCLID:46
.= |.((((a * z) - (a * x)) + (b * z)) - (b * y)).| by JORDAN2C:7
.= |.(((a * z) - (a * x)) + ((b * z) - (b * y))).| by EUCLID:45
.= |.((a * (z - x)) + ((b * z) - (b * y))).| by EUCLID:49
.= |.((a * (z - x)) + (b * (z - y))).| by EUCLID:49 ;
then |.(((a * z) + (b * z)) - ((a * x) + (b * y))).| <= |.(a * (z - x)).| + |.(b * (z - y)).| by TOPRNS_1:29;
then |.(((a * z) + (b * z)) - ((a * x) + (b * y))).| < r by A8, XXREAL_0:2;
then A9: |.(((a * x) + (b * y)) - ((a * z) + (b * z))).| < r by TOPRNS_1:27;
(a * z) + (b * z) = (a + b) * z by EUCLID:33
.= z by A1, EUCLID:29 ;
hence (a * x) + (b * y) in Ball (z,r) by A9; :: thesis: verum