let a be Real; for n being Nat
for P being Subset of (TOP-REAL n) st n >= 1 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
not P is bounded
let n be Nat; for P being Subset of (TOP-REAL n) st n >= 1 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
not P is bounded
let P be Subset of (TOP-REAL n); ( n >= 1 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } implies not P is bounded )
assume that
A1:
n >= 1
and
A2:
P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a }
; not P is bounded
per cases
( a > 0 or a <= 0 )
;
suppose A3:
a > 0
;
not P is bounded now not P is bounded set p = the
Element of
P;
assume
P is
bounded
;
contradictionthen consider r being
Real such that A4:
for
q being
Point of
(TOP-REAL n) st
q in P holds
|.q.| < r
by Th21;
A5:
P <> {}
by A1, A2, Th39;
then
the
Element of
P in P
;
then reconsider p = the
Element of
P as
Point of
(TOP-REAL n) ;
A6:
|.p.| < r
by A4, A5;
A13:
(a + r) + 1
<= |.((a + r) + 1).|
by ABSVALUE:4;
(
|.((a + r) + 1).| >= 0 &
sqrt 1
<= sqrt n )
by A1, COMPLEX1:46, SQUARE_1:26;
then A14:
|.((a + r) + 1).| * 1
<= |.((a + r) + 1).| * (sqrt n)
by SQUARE_1:18, XREAL_1:64;
A15:
a + r < (a + r) + 1
by XREAL_1:29;
|.(((a + r) + 1) * (1.REAL n)).| =
|.((a + r) + 1).| * |.(1.REAL n).|
by TOPRNS_1:7
.=
|.((a + r) + 1).| * (sqrt n)
by EUCLID:73
;
then
(a + r) + 1
<= |.(((a + r) + 1) * (1.REAL n)).|
by A14, A13, XXREAL_0:2;
then A16:
a + r < |.(((a + r) + 1) * (1.REAL n)).|
by A15, XXREAL_0:2;
r < r + a
by A3, XREAL_1:29;
hence
contradiction
by A2, A4, A7, A16, XXREAL_0:2;
verum end; hence
not
P is
bounded
;
verum end; end;