let n be 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) -> Element of REAL = In (|.((x + z) - $1).|,REAL);
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) -> Element of REAL = In (|.(x - $1).|,REAL);
deffunc H₄( Element of COMPLEX n) -> Real = |.(x - $1).|;
A1: for z1 being Element of COMPLEX n holds H₂(z1) = H₁(z1) ;
A2: { H₂(z1) where z1 is Element of COMPLEX n : S₁[z1] } = { H₁(z2) where z2 is Element of COMPLEX n : S₁[z2] } from FRAENKEL:sch 5(A1);
A3: for z1 being Element of COMPLEX n holds H₃(z1) = H₄(z1) ;
A4: { H₃(z1) where z1 is Element of COMPLEX n : S₁[z1] } = { H₄(z2) where z2 is Element of COMPLEX n : S₁[z2] } from FRAENKEL:sch 5(A3);
A5: Y is bounded_below

proof

take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of Y
let r be ExtReal; :: 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 ) by A2;
hence 0 <= r by Th94; :: 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
A6: z2 in A by SUBSET_1:4;
A7: dist ((x + z),A) = lower_bound Y by Def17, A2;

A8: now :: thesis: for r9 being Real st r9 in X holds
r9 >= (dist ((x + z),A)) - |.z.|

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
A9: r9 = |.(x - z3).| and
A10: z3 in A by A4;
|.((x + z) - z3).| = |.((x - z3) + z).| by Th75;
then A11: |.((x + z) - z3).| <= r9 + |.z.| by A9, Th97;
|.((x + z) - z3).| in Y by A10, A2;
then |.((x + z) - z3).| >= dist ((x + z),A) by A7, A5, Def2;
then r9 + |.z.| >= dist ((x + z),A) by A11, XXREAL_0:2;
hence r9 >= (dist ((x + z),A)) - |.z.| by XREAL_1:20; :: thesis: verum

end;

A12: |.(x - z2).| in X by A6, A4;
dist (x,A) = lower_bound X by Def17, A4;
then (dist ((x + z),A)) - |.z.| <= dist (x,A) by A12, A8, Th112;
hence dist ((x + z),A) <= (dist (x,A)) + |.z.| by XREAL_1:20; :: thesis: verum