let n be Element of NAT ; :: thesis: for x, z being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist ((x + z),A) <= (dist (x,A)) + |.z.|
let x, z be Element of COMPLEX n; :: thesis: for A being Subset of (COMPLEX n) st A <> {} holds
dist ((x + z),A) <= (dist (x,A)) + |.z.|
let A be Subset of (COMPLEX n); :: thesis: ( A <> {} implies dist ((x + z),A) <= (dist (x,A)) + |.z.| )
defpred S₁[ set ] means $1 in A;
deffunc H₁( Element of COMPLEX n) -> Real = |.((x + z) - $1).|;
reconsider Y = { H₁(z1) where z1 is Element of COMPLEX n : S₁[z1] } as Subset of REAL from DOMAIN_1:sch 8();
deffunc H₂( Element of COMPLEX n) -> Real = |.(x - $1).|;
A1: Y is bounded_below

proof

take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of Y
let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not r in Y or 0 <= r )
assume r in Y ; :: thesis: 0 <= r
then ex z1 being Element of COMPLEX n st
( r = |.((x + z) - z1).| & z1 in A ) ;
hence 0 <= r by Th65; :: thesis: verum

end;

reconsider X = { H₂(z1) where z1 is Element of COMPLEX n : S₁[z1] } as Subset of REAL from DOMAIN_1:sch 8();
assume A <> {} ; :: thesis: dist ((x + z),A) <= (dist (x,A)) + |.z.|
then consider z2 being Element of COMPLEX n such that
A2: z2 in A by SUBSET_1:10;
A3: dist ((x + z),A) = lower_bound Y by Def18;

A4: now

let r9 be Real; :: thesis: ( r9 in X implies r9 >= (dist ((x + z),A)) - |.z.| )
assume r9 in X ; :: thesis: r9 >= (dist ((x + z),A)) - |.z.|
then consider z3 being Element of COMPLEX n such that
A5: r9 = |.(x - z3).| and
A6: z3 in A ;
|.((x + z) - z3).| = |.((x - z3) + z).| by Th46;
then A7: |.((x + z) - z3).| <= r9 + |.z.| by A5, Th68;
|.((x + z) - z3).| in Y by A6;
then |.((x + z) - z3).| >= dist ((x + z),A) by A3, A1, Def5;
then r9 + |.z.| >= dist ((x + z),A) by A7, XXREAL_0:2;
hence r9 >= (dist ((x + z),A)) - |.z.| by XREAL_1:22; :: thesis: verum

end;

A8: |.(x - z2).| in X by A2;
dist (x,A) = lower_bound X by Def18;
then (dist ((x + z),A)) - |.z.| <= dist (x,A) by A8, A4, Th84;
hence dist ((x + z),A) <= (dist (x,A)) + |.z.| by XREAL_1:22; :: thesis: verum