let W be Subset of (Euclid 1); :: thesis: for a being Real st W = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) } holds
not W is bounded
let a be Real; :: thesis: ( W = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) } implies not W is bounded )
|.a.| >= 0 by COMPLEX1:46;
then A1: (|.a.| + |.a.|) + |.a.| >= 0 + |.a.| by XREAL_1:6;
assume A2: W = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) } ; :: thesis: not W is bounded
assume W is bounded ; :: thesis: contradiction
then consider r being Real such that
A3: 0 < r and
A4: for x, y being Point of (Euclid 1) st x in W & y in W holds
dist (x,y) <= r ;
A5: (- (3 * (r + |.a.|))) * (1.REAL 1) = (- (3 * (r + |.a.|))) * <*1*> by FINSEQ_2:59
.= <*((- (3 * (r + |.a.|))) * 1)*> by RVSUM_1:47 ;
reconsider z1 = (- (3 * (r + |.a.|))) * (1.REAL 1) as Point of (Euclid 1) by FINSEQ_2:131;
3 * r > 0 by A3, XREAL_1:129;
then ( a <= |.a.| & 0 + |.a.| < (3 * r) + (3 * |.a.|) ) by A1, ABSVALUE:4, XREAL_1:8;
then a < 3 * (r + |.a.|) by XXREAL_0:2;
then - a > - (3 * (r + |.a.|)) by XREAL_1:24;
then A6: (- (3 * (r + |.a.|))) * (1.REAL 1) in { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) } by A5;
A7: (- (r + |.a.|)) * (1.REAL 1) = (- (r + |.a.|)) * <*1*> by FINSEQ_2:59
.= <*((- (r + |.a.|)) * 1)*> by RVSUM_1:47 ;
reconsider z2 = (- (r + |.a.|)) * (1.REAL 1) as Point of (Euclid 1) by FINSEQ_2:131;
dist (z1,z2) = |.(((- (3 * (r + |.a.|))) * (1.REAL 1)) - ((- (r + |.a.|)) * (1.REAL 1))).| by JGRAPH_1:28
.= |.(((- (3 * (r + |.a.|))) - (- (r + |.a.|))) * (1.REAL 1)).| by RLVECT_1:35
.= |.(- (((- (3 * (r + |.a.|))) - (- (r + |.a.|))) * (1.REAL 1))).| by TOPRNS_1:26
.= |.((- ((- (3 * (r + |.a.|))) + (- (- (r + |.a.|))))) * (1.REAL 1)).| by RLVECT_1:79
.= |.((r + |.a.|) + (r + |.a.|)).| * |.(1.REAL 1).| by TOPRNS_1:7
.= |.((r + |.a.|) + (r + |.a.|)).| * (sqrt 1) by EUCLID:73 ;
then A8: (r + |.a.|) + (r + |.a.|) <= dist (z1,z2) by ABSVALUE:4;
A9: 0 <= |.a.| by COMPLEX1:46;
then (r + |.a.|) + 0 < (r + |.a.|) + (r + |.a.|) by A3, XREAL_1:6;
then A10: r + |.a.| < dist (z1,z2) by A8, XXREAL_0:2;
r + 0 <= r + |.a.| by A9, XREAL_1:6;
then A11: r < dist (z1,z2) by A10, XXREAL_0:2;
( a <= |.a.| & 0 + |.a.| < r + |.a.| ) by A3, ABSVALUE:4, XREAL_1:6;
then a < r + |.a.| by XXREAL_0:2;
then - a > - (r + |.a.|) by XREAL_1:24;
then (- (r + |.a.|)) * (1.REAL 1) in W by A2, A7;
hence contradiction by A2, A4, A6, A11; :: thesis: verum