let n be Nat; 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; 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); ( 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 <> {}
; (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 )
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 )
A17:
Z is bounded_below
A18:
( X <> {} & X is bounded_below )
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; verum