let n be Nat; :: thesis: for x being Element of COMPLEX n
for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
(dist (x,A)) + (dist (x,B)) >= dist (A,B)
let x be Element of COMPLEX n; :: thesis: for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
(dist (x,A)) + (dist (x,B)) >= dist (A,B)
let A, B be Subset of (COMPLEX n); :: thesis: ( A <> {} & B <> {} implies (dist (x,A)) + (dist (x,B)) >= dist (A,B) )
defpred S1[ set ] means $1 in B;
deffunc H1( Element of COMPLEX n) -> Real = |.(x - $1).|;
deffunc H2( Element of COMPLEX n) -> Element of REAL = In (|.(x - $1).|,REAL);
reconsider Y = { H2(z) where z is Element of COMPLEX n : S1[z] } as Subset of REAL from DOMAIN_1:sch 8();
 defpred S2[ set , set ] means ( $1 in A & $2 in B );
defpred S3[ set ] means $1 in A;
deffunc H3( Element of COMPLEX n, Element of COMPLEX n) -> Element of REAL = In (|.($1 - $2).|,REAL);
deffunc H4( Element of COMPLEX n, Element of COMPLEX n) -> Real = |.($1 - $2).|;
reconsider X = { H2(z) where z is Element of COMPLEX n : S3[z] } as Subset of REAL from DOMAIN_1:sch 8();
 assume that
A1: A <> {} and
A2: B <> {} ; :: thesis: (dist (x,A)) + (dist (x,B)) >= dist (A,B)
consider z2 being Element of COMPLEX n such that
A3: z2 in B by A2, SUBSET_1:4;
A4: ( Y <> {} & Y is bounded_below )
proof
H2(z2) in Y by A3;
hence Y <> {} ; :: thesis: Y is bounded_below
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 = H2(z1) & z1 in B ) ;
hence 0 <= r by Th94; :: thesis: verum
end;
A5: for z being Element of COMPLEX n holds H2(z) = H1(z) ;
A6: { H2(z) where z is Element of COMPLEX n : S1[z] } = { H1(z1) where z1 is Element of COMPLEX n : S1[z1] } from FRAENKEL:sch 5(A5);
 { H2(z) where z is Element of COMPLEX n : S3[z] } = { H1(z1) where z1 is Element of COMPLEX n : S3[z1] } from FRAENKEL:sch 5(A5);
 then A7: ( lower_bound X = dist (x,A) & lower_bound Y = dist (x,B) ) by Def17, A6;
A8: H2(z2) in Y by A3;
reconsider Z = { H3(z1,z) where z1, z is Element of COMPLEX n : S2[z1,z] } as Subset of REAL from DOMAIN_1:sch 9();
 consider z1 being Element of COMPLEX n such that
A9: z1 in A by A1, SUBSET_1:4;
X ++ Y c= REAL by MEMBERED:3;
then reconsider XY = X ++ Y as Subset of REAL ;
A10: for r being Real st r in XY holds
ex r1 being Real st
( r1 in Z & r1 <= r )
proof
let r be Real; :: thesis: ( r in XY implies ex r1 being Real st
( r1 in Z & r1 <= r ) )
assume r in XY ; :: thesis: ex r1 being Real st
( r1 in Z & r1 <= r )
then r in { (r2 + r1) where r2, r1 is Complex : ( r2 in X & r1 in Y ) } by MEMBER_1:def 6;
then consider r2, r1 being Complex such that
A11: r = r2 + r1 and
A12: r2 in X and
A13: r1 in Y ;
consider z2 being Element of COMPLEX n such that
A14: ( r1 = H2(z2) & z2 in B ) by A13;
consider z1 being Element of COMPLEX n such that
A15: r2 = H2(z1) and
A16: z1 in A by A12;
take r3 = H3(z1,z2); :: thesis: ( r3 in Z & r3 <= r )
r2 = |.(z1 - x).| by A15, Th103;
hence ( r3 in Z & r3 <= r ) by A11, A16, A14, Th104; :: thesis: verum
end;
A17: Z is bounded_below
proof
take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of Z
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in Z or 0 <= r )
assume r in Z ; :: thesis: 0 <= r
then ex z1, z being Element of COMPLEX n st
( r = H3(z1,z) & S2[z1,z] ) ;
hence 0 <= r by Th94; :: thesis: verum
end;
A18: ( X <> {} & X is bounded_below )
proof
H2(z1) in X by A9;
hence X <> {} ; :: thesis: X is bounded_below
take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of X
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in X or 0 <= r )
assume r in X ; :: thesis: 0 <= r
then ex z being Element of COMPLEX n st
( r = H2(z) & z in A ) ;
hence 0 <= r by Th94; :: thesis: verum
end;
A19: for z3, z being Element of COMPLEX n holds H3(z3,z) = H4(z3,z) ;
{ H3(z3,z) where z3, z is Element of COMPLEX n : S2[z3,z] } = { H4(z3,z) where z3, z is Element of COMPLEX n : S2[z3,z] } from FRAENKEL:sch 7(A19);
 then A20: lower_bound Z = dist (A,B) by Def19;
H2(z1) in X by A9;
then |.(x - z1).| + |.(x - z2).| in X ++ Y by A8, MEMBER_1:46;
then XY <> {} ;
then lower_bound XY >= lower_bound Z by A17, A10, Th125;
hence (dist (x,A)) + (dist (x,B)) >= dist (A,B) by A18, A4, A7, A20, Th124; :: thesis: verum