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
A6: (a * z) + (b * z) = (a + b) * z by EUCLID:37
.= z by A1, EUCLID:33 ;
A7: |.(((a * z) + (b * z)) - ((a * x) + (b * y))).| = |.(((a * z) - ((a * x) + (b * y))) + (b * z)).| by JORDAN2C:9
.= |.((((a * z) - (a * x)) - (b * y)) + (b * z)).| by EUCLID:50
.= |.((((a * z) - (a * x)) + (b * z)) - (b * y)).| by JORDAN2C:9
.= |.(((a * z) - (a * x)) + ((b * z) - (b * y))).| by EUCLID:49
.= |.((a * (z - x)) + ((b * z) - (b * y))).| by EUCLID:53
.= |.((a * (z - x)) + (b * (z - y))).| by EUCLID:53 ;
A8: a is Real by XREAL_0:def 1;
A9: b is Real by XREAL_0:def 1;
A10: 0 <= abs a by COMPLEX1:132;
A11: 0 < abs b by A3, COMPLEX1:133;
( |.(x - z).| <= r & |.(y - z).| < r ) by A4, A5, Th7, Th8;
then ( |.(z - x).| <= r & |.(z - y).| < r ) by TOPRNS_1:28;
then ( (abs a) * |.(z - x).| <= (abs a) * r & (abs b) * |.(z - y).| < (abs b) * r ) by A10, A11, XREAL_1:66, XREAL_1:70;
then ((abs a) * |.(z - x).|) + ((abs b) * |.(z - y).|) < ((abs a) * r) + ((abs b) * r) by XREAL_1:10;
then ((abs a) * |.(z - x).|) + ((abs b) * |.(z - y).|) < ((abs a) + (abs b)) * r ;
then |.(a * (z - x)).| + ((abs b) * |.(z - y).|) < 1 * r by A2, A8, TOPRNS_1:8;
then A12: |.(a * (z - x)).| + |.(b * (z - y)).| < r by A9, TOPRNS_1:8;
|.(((a * z) + (b * z)) - ((a * x) + (b * y))).| <= |.(a * (z - x)).| + |.(b * (z - y)).| by A7, TOPRNS_1:30;
then |.(((a * z) + (b * z)) - ((a * x) + (b * y))).| < r by A12, XXREAL_0:2;
then |.(((a * x) + (b * y)) - ((a * z) + (b * z))).| < r by TOPRNS_1:28;
hence (a * x) + (b * y) in Ball z,r by A6; :: thesis: verum