let r be Real; :: thesis: for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds

upper_bound (r ** X) = r * (upper_bound X)

let X be non empty Subset of REAL; :: thesis: ( X is bounded_above & 0 <= r implies upper_bound (r ** X) = r * (upper_bound X) )

assume that

A1: X is bounded_above and

A2: 0 <= r ; :: thesis: upper_bound (r ** X) = r * (upper_bound X)

A3: for a being Real st a in r ** X holds

a <= r * (upper_bound X)

a <= b ) holds

r * (upper_bound X) <= b

upper_bound (r ** X) = r * (upper_bound X)

let X be non empty Subset of REAL; :: thesis: ( X is bounded_above & 0 <= r implies upper_bound (r ** X) = r * (upper_bound X) )

assume that

A1: X is bounded_above and

A2: 0 <= r ; :: thesis: upper_bound (r ** X) = r * (upper_bound X)

A3: for a being Real st a in r ** X holds

a <= r * (upper_bound X)

proof

for b being Real st ( for a being Real st a in r ** X holds
let a be Real; :: thesis: ( a in r ** X implies a <= r * (upper_bound X) )

assume a in r ** X ; :: thesis: a <= r * (upper_bound X)

then a in { (r * x) where x is Real : x in X } by Th8;

then consider x being Real such that

A4: a = r * x and

A5: x in X ;

x <= upper_bound X by A1, A5, SEQ_4:def 1;

hence a <= r * (upper_bound X) by A2, A4, XREAL_1:64; :: thesis: verum

end;assume a in r ** X ; :: thesis: a <= r * (upper_bound X)

then a in { (r * x) where x is Real : x in X } by Th8;

then consider x being Real such that

A4: a = r * x and

A5: x in X ;

x <= upper_bound X by A1, A5, SEQ_4:def 1;

hence a <= r * (upper_bound X) by A2, A4, XREAL_1:64; :: thesis: verum

a <= b ) holds

r * (upper_bound X) <= b

proof

hence
upper_bound (r ** X) = r * (upper_bound X)
by A3, SEQ_4:46; :: thesis: verum
consider x being Element of REAL such that

A6: x in X by SUBSET_1:4;

let b be Real; :: thesis: ( ( for a being Real st a in r ** X holds

a <= b ) implies r * (upper_bound X) <= b )

assume A7: for a being Real st a in r ** X holds

a <= b ; :: thesis: r * (upper_bound X) <= b

reconsider x = x as Real ;

r * x in { (r * y) where y is Real : y in X } by A6;

then A8: r * x in r ** X by Th8;

end;A6: x in X by SUBSET_1:4;

let b be Real; :: thesis: ( ( for a being Real st a in r ** X holds

a <= b ) implies r * (upper_bound X) <= b )

assume A7: for a being Real st a in r ** X holds

a <= b ; :: thesis: r * (upper_bound X) <= b

reconsider x = x as Real ;

r * x in { (r * y) where y is Real : y in X } by A6;

then A8: r * x in r ** X by Th8;

now :: thesis: r * (upper_bound X) <= bend;

hence
r * (upper_bound X) <= b
; :: thesis: verumper cases
( r = 0 or r > 0 )
by A2;

end;

suppose A9:
r > 0
; :: thesis: r * (upper_bound X) <= b

for z being Real st z in X holds

z <= b / r

then r * (upper_bound X) <= (b / r) * r by A9, XREAL_1:64;

hence r * (upper_bound X) <= b by A9, XCMPLX_1:87; :: thesis: verum

end;z <= b / r

proof

then
upper_bound X <= b / r
by SEQ_4:45;
let z be Real; :: thesis: ( z in X implies z <= b / r )

assume z in X ; :: thesis: z <= b / r

then r * z in { (r * y) where y is Real : y in X } ;

then r * z in r ** X by Th8;

hence z <= b / r by A7, A9, XREAL_1:77; :: thesis: verum

end;assume z in X ; :: thesis: z <= b / r

then r * z in { (r * y) where y is Real : y in X } ;

then r * z in r ** X by Th8;

hence z <= b / r by A7, A9, XREAL_1:77; :: thesis: verum

then r * (upper_bound X) <= (b / r) * r by A9, XREAL_1:64;

hence r * (upper_bound X) <= b by A9, XCMPLX_1:87; :: thesis: verum