let n be Element of NAT ; :: thesis: for r1 being Real
for z1 being Element of COMPLEX n holds Ball z1,r1 is open
let r1 be Real; :: thesis: for z1 being Element of COMPLEX n holds Ball z1,r1 is open
let z1 be Element of COMPLEX n; :: thesis: Ball z1,r1 is open
let x be Element of COMPLEX n; :: according to COMPLSP1:def 15 :: thesis: ( x in Ball z1,r1 implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball z1,r1 ) ) )
assume A1: x in Ball z1,r1 ; :: thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball z1,r1 ) )
take r = r1 - |.(z1 - x).|; :: thesis: ( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball z1,r1 ) )
|.(z1 - x).| < r1 by A1, Th80;
hence 0 < r by XREAL_1:52; :: thesis: for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball z1,r1
let z be Element of COMPLEX n; :: thesis: ( |.z.| < r implies x + z in Ball z1,r1 )
(z1 - x) - z = z1 - (x + z) by Th45;
then A2: |.(z1 - (x + z)).| <= |.z.| + |.(z1 - x).| by Th69;
assume |.z.| < r ; :: thesis: x + z in Ball z1,r1
then |.z.| + |.(z1 - x).| < r + |.(z1 - x).| by XREAL_1:8;
then |.(z1 - (x + z)).| < r + |.(z1 - x).| by A2, XXREAL_0:2;
hence x + z in Ball z1,r1 by Th80; :: thesis: verum