let X be Subset of REAL; :: thesis: ( X is real-bounded iff ex s being Real st
( 0 < s & ( for r being Real st r in X holds
|.r.| < s ) ) )
thus ( X is real-bounded implies ex s being Real st
( 0 < s & ( for r being Real st r in X holds
|.r.| < s ) ) ) :: thesis: ( ex s being Real st
( 0 < s & ( for r being Real st r in X holds
|.r.| < s ) ) implies X is real-bounded )
proof
assume A1: X is real-bounded ; :: thesis: ex s being Real st
( 0 < s & ( for r being Real st r in X holds
|.r.| < s ) )
then consider s1 being Real such that
A2: s1 is UpperBound of X by XXREAL_2:def 10;
A3: for r being Real st r in X holds
r <= s1 by A2, XXREAL_2:def 1;
consider s2 being Real such that
A4: s2 is LowerBound of X by A1, XXREAL_2:def 9;
A5: for r being Real st r in X holds
s2 <= r by A4, XXREAL_2:def 2;
take s = (|.s1.| + |.s2.|) + 1; :: thesis: ( 0 < s & ( for r being Real st r in X holds
|.r.| < s ) )
A6: 0 <= |.s1.| by COMPLEX1:46;
A7: 0 <= |.s2.| by COMPLEX1:46;
hence 0 < s by A6; :: thesis: for r being Real st r in X holds
|.r.| < s
let r be Real; :: thesis: ( r in X implies |.r.| < s )
assume A8: r in X ; :: thesis: |.r.| < s
( s1 <= |.s1.| & r <= s1 ) by A3, A8, ABSVALUE:4;
then r <= |.s1.| by XXREAL_0:2;
then r + 0 <= |.s1.| + |.s2.| by A7, XREAL_1:7;
then A9: r < s by XREAL_1:8;
( - |.s2.| <= s2 & s2 <= r ) by A5, A8, ABSVALUE:4;
then - |.s2.| <= r by XXREAL_0:2;
then (- |.s1.|) + (- |.s2.|) <= 0 + r by A6, XREAL_1:7;
then A10: ((- |.s1.|) - |.s2.|) + (- 1) < r + 0 by XREAL_1:8;
((- |.s1.|) - |.s2.|) - 1 = - ((|.s1.| + |.s2.|) + 1) ;
hence |.r.| < s by A9, A10, SEQ_2:1; :: thesis: verum
end;
given s being Real such that 0 < s and
A11: for r being Real st r in X holds
|.r.| < s ; :: thesis: X is real-bounded
thus X is bounded_below :: according to XXREAL_2:def 11 :: thesis: X is bounded_above
proof
take - s ; :: according to XXREAL_2:def 9 :: thesis: - s is LowerBound of X
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in X or - s <= r )
assume A12: r in X ; :: thesis: - s <= r
then reconsider r = r as Real ;
|.r.| < s by A11, A12;
then A13: - s < - |.r.| by XREAL_1:24;
- |.r.| <= r by ABSVALUE:4;
hence - s <= r by A13, XXREAL_0:2; :: thesis: verum
end;
take s ; :: according to XXREAL_2:def 10 :: thesis: s is UpperBound of X
let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in X or r <= s )
assume A14: r in X ; :: thesis: r <= s
then reconsider r = r as Real ;
r <= |.r.| by ABSVALUE:4;
hence r <= s by A11, A14, XXREAL_0:2; :: thesis: verum