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 S1[ set ] means $1 in A;
deffunc H1( Element of COMPLEX n) -> Element of REAL = In (|.((x + z) - $1).|,REAL);
deffunc H2( Element of COMPLEX n) -> Real = |.((x + z) - $1).|;
reconsider Y = { H1(z1) where z1 is Element of COMPLEX n : S1[z1] } as Subset of REAL from DOMAIN_1:sch 8();
 deffunc H3( Element of COMPLEX n) -> Element of REAL = In (|.(x - $1).|,REAL);
deffunc H4( Element of COMPLEX n) -> Real = |.(x - $1).|;
A1: for z1 being Element of COMPLEX n holds H2(z1) = H1(z1) ;
A2: { H2(z1) where z1 is Element of COMPLEX n : S1[z1] } = { H1(z2) where z2 is Element of COMPLEX n : S1[z2] } from FRAENKEL:sch 5(A1);
 A3: for z1 being Element of COMPLEX n holds H3(z1) = H4(z1) ;
A4: { H3(z1) where z1 is Element of COMPLEX n : S1[z1] } = { H4(z2) where z2 is Element of COMPLEX n : S1[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 = { H3(z1) where z1 is Element of COMPLEX n : S1[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