let n be Element of NAT ; :: thesis: for W being Subset of (Euclid n)
for a being Real
for P being Subset of (TOP-REAL n) st n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } & P = W holds
( P is connected & not W is bounded )
let W be Subset of (Euclid n); :: thesis: for a being Real
for P being Subset of (TOP-REAL n) st n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } & P = W holds
( P is connected & not W is bounded )
let a be Real; :: thesis: for P being Subset of (TOP-REAL n) st n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } & P = W holds
( P is connected & not W is bounded )
let P be Subset of (TOP-REAL n); :: thesis: ( n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } & P = W implies ( P is connected & not W is bounded ) )
assume A1: ( n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } & P = W ) ; :: thesis: ( P is connected & not W is bounded )
hence P is connected by Th59; :: thesis: not W is bounded
A2: 1 <= n by A1, XXREAL_0:2;
then A3: 1 <= sqrt n by SQUARE_1:18, SQUARE_1:26;
assume W is bounded ; :: thesis: contradiction
then consider r being Real such that
A4: 0 < r and
A5: for x, y being Point of (Euclid n) st x in W & y in W holds
dist (x,y) <= r by TBSP_1:def 7;
A6: r + (abs a) <= abs (r + (abs a)) by ABSVALUE:4;
( abs (r + (abs a)) >= 0 & 1 <= sqrt n ) by A2, COMPLEX1:46, SQUARE_1:18, SQUARE_1:26;
then A7: (abs (r + (abs a))) * 1 <= (abs (r + (abs a))) * (sqrt n) by XREAL_1:64;
( a <= abs a & abs a < r + (abs a) ) by A4, ABSVALUE:4, XREAL_1:29;
then A8: a < r + (abs a) by XXREAL_0:2;
|.(- ((r + (abs a)) * (1.REAL n))).| = |.((r + (abs a)) * (1.REAL n)).| by TOPRNS_1:26
.= (abs (r + (abs a))) * |.(1.REAL n).| by TOPRNS_1:7
.= (abs (r + (abs a))) * (sqrt n) by Th35 ;
then r + (abs a) <= |.(- ((r + (abs a)) * (1.REAL n))).| by A7, A6, XXREAL_0:2;
then a < |.(- ((r + (abs a)) * (1.REAL n))).| by A8, XXREAL_0:2;
then A9: - ((r + (abs a)) * (1.REAL n)) in W by A1;
then reconsider z2 = - ((r + (abs a)) * (1.REAL n)) as Point of (Euclid n) ;
A10: r + (abs a) <= abs (r + (abs a)) by ABSVALUE:4;
abs (r + (abs a)) >= 0 by COMPLEX1:46;
then A11: (abs (r + (abs a))) * 1 <= (abs (r + (abs a))) * (sqrt n) by A3, XREAL_1:64;
|.((r + (abs a)) * (1.REAL n)).| = (abs (r + (abs a))) * |.(1.REAL n).| by TOPRNS_1:7
.= (abs (r + (abs a))) * (sqrt n) by Th35 ;
then r + (abs a) <= |.((r + (abs a)) * (1.REAL n)).| by A11, A10, XXREAL_0:2;
then a < |.((r + (abs a)) * (1.REAL n)).| by A8, XXREAL_0:2;
then A12: (r + (abs a)) * (1.REAL n) in W by A1;
then reconsider z1 = (r + (abs a)) * (1.REAL n) as Point of (Euclid n) ;
A13: (r + (abs a)) + (r + (abs a)) <= abs ((r + (abs a)) + (r + (abs a))) by ABSVALUE:4;
abs ((r + (abs a)) + (r + (abs a))) >= 0 by COMPLEX1:46;
then A14: (abs ((r + (abs a)) + (r + (abs a)))) * 1 <= (abs ((r + (abs a)) + (r + (abs a)))) * (sqrt n) by A3, XREAL_1:64;
A15: 0 <= abs a by COMPLEX1:46;
then A16: r + 0 <= r + (abs a) by XREAL_1:6;
A17: (r + (abs a)) + 0 < (r + (abs a)) + (r + (abs a)) by A4, A15, XREAL_1:6;
dist (z1,z2) = |.(((r + (abs a)) * (1.REAL n)) - (- ((r + (abs a)) * (1.REAL n)))).| by JGRAPH_1:28
.= |.(((r + (abs a)) * (1.REAL n)) + ((r + (abs a)) * (1.REAL n))).|
.= |.(((r + (abs a)) + (r + (abs a))) * (1.REAL n)).| by EUCLID:33
.= (abs ((r + (abs a)) + (r + (abs a)))) * |.(1.REAL n).| by TOPRNS_1:7
.= (abs ((r + (abs a)) + (r + (abs a)))) * (sqrt n) by Th35 ;
then (r + (abs a)) + (r + (abs a)) <= dist (z1,z2) by A14, A13, XXREAL_0:2;
then r + (abs a) < dist (z1,z2) by A17, XXREAL_0:2;
then r < dist (z1,z2) by A16, XXREAL_0:2;
hence contradiction by A5, A12, A9; :: thesis: verum