let n be Nat; :: thesis: for W being Subset of (Euclid n)
for a being Real st n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } holds
not W is bounded
let W be Subset of (Euclid n); :: thesis: for a being Real st n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } holds
not W is bounded
let a be Real; :: thesis: ( n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } implies not W is bounded )
assume A1: ( n >= 2 & W = { q where q is Point of (TOP-REAL n) : |.q.| > a } ) ; :: 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 ;
A6: r + |.a.| <= |.(r + |.a.|).| by ABSVALUE:4;
( |.(r + |.a.|).| >= 0 & 1 <= sqrt n ) by A2, COMPLEX1:46, SQUARE_1:18, SQUARE_1:26;
then A7: |.(r + |.a.|).| * 1 <= |.(r + |.a.|).| * (sqrt n) by XREAL_1:64;
( a <= |.a.| & |.a.| < r + |.a.| ) by A4, ABSVALUE:4, XREAL_1:29;
then A8: a < r + |.a.| by XXREAL_0:2;
|.(- ((r + |.a.|) * (1.REAL n))).| = |.((r + |.a.|) * (1.REAL n)).| by TOPRNS_1:26
.= |.(r + |.a.|).| * |.(1.REAL n).| by TOPRNS_1:7
.= |.(r + |.a.|).| * (sqrt n) by EUCLID:73 ;
then r + |.a.| <= |.(- ((r + |.a.|) * (1.REAL n))).| by A7, A6, XXREAL_0:2;
then a < |.(- ((r + |.a.|) * (1.REAL n))).| by A8, XXREAL_0:2;
then A9: - ((r + |.a.|) * (1.REAL n)) in W by A1;
then reconsider z2 = - ((r + |.a.|) * (1.REAL n)) as Point of (Euclid n) ;
A10: r + |.a.| <= |.(r + |.a.|).| by ABSVALUE:4;
|.(r + |.a.|).| >= 0 by COMPLEX1:46;
then A11: |.(r + |.a.|).| * 1 <= |.(r + |.a.|).| * (sqrt n) by A3, XREAL_1:64;
|.((r + |.a.|) * (1.REAL n)).| = |.(r + |.a.|).| * |.(1.REAL n).| by TOPRNS_1:7
.= |.(r + |.a.|).| * (sqrt n) by EUCLID:73 ;
then r + |.a.| <= |.((r + |.a.|) * (1.REAL n)).| by A11, A10, XXREAL_0:2;
then a < |.((r + |.a.|) * (1.REAL n)).| by A8, XXREAL_0:2;
then A12: (r + |.a.|) * (1.REAL n) in W by A1;
then reconsider z1 = (r + |.a.|) * (1.REAL n) as Point of (Euclid n) ;
A13: (r + |.a.|) + (r + |.a.|) <= |.((r + |.a.|) + (r + |.a.|)).| by ABSVALUE:4;
|.((r + |.a.|) + (r + |.a.|)).| >= 0 by COMPLEX1:46;
then A14: |.((r + |.a.|) + (r + |.a.|)).| * 1 <= |.((r + |.a.|) + (r + |.a.|)).| * (sqrt n) by A3, XREAL_1:64;
A15: 0 <= |.a.| by COMPLEX1:46;
then A16: r + 0 <= r + |.a.| by XREAL_1:6;
A17: (r + |.a.|) + 0 < (r + |.a.|) + (r + |.a.|) by A4, A15, XREAL_1:6;
dist (z1,z2) = |.(((r + |.a.|) * (1.REAL n)) - (- ((r + |.a.|) * (1.REAL n)))).| by JGRAPH_1:28
.= |.(((r + |.a.|) * (1.REAL n)) + ((r + |.a.|) * (1.REAL n))).|
.= |.(((r + |.a.|) + (r + |.a.|)) * (1.REAL n)).| by RLVECT_1:def 6
.= |.((r + |.a.|) + (r + |.a.|)).| * |.(1.REAL n).| by TOPRNS_1:7
.= |.((r + |.a.|) + (r + |.a.|)).| * (sqrt n) by EUCLID:73 ;
then (r + |.a.|) + (r + |.a.|) <= dist (z1,z2) by A14, A13, XXREAL_0:2;
then r + |.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