let A be non empty Interval; :: thesis: for x being Real st 0 < x & A is right_open_interval holds
x ** A is right_open_interval
let x be Real; :: thesis: ( 0 < x & A is right_open_interval implies x ** A is right_open_interval )
assume A1: 0 < x ; :: thesis: ( not A is right_open_interval or x ** A is right_open_interval )
assume A is right_open_interval ; :: thesis: x ** A is right_open_interval
then consider a being Real, b being R_eal such that
A2: A = [.a,b.[ by MEASURE5:def 4;
A3: a < b by A2, XXREAL_1:27;
reconsider a = a as R_eal by XXREAL_0:def 1;
now :: thesis: ( ( a = -infty & b = -infty & x ** A is right_open_interval ) or ( a = -infty & b in REAL & x ** A is right_open_interval ) or ( a = -infty & b = +infty & x ** A is right_open_interval ) or ( a in REAL & b in REAL & x ** A is right_open_interval ) or ( a in REAL & b = +infty & x ** A is right_open_interval ) or ( a = +infty & b = +infty & x ** A is right_open_interval ) )
per cases ( ( a = -infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = +infty & b = +infty ) ) by A3, Th5;
case A4: ( a in REAL & b in REAL ) ; :: thesis: x ** A is right_open_interval
then consider r being Real such that
A5: r = b ;
x * r is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A6: g = x * r ;
consider s being Real such that
A7: s = a ;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A8: d = x * s ;
A9: [.d,g.[ c= x ** A
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in [.d,g.[ or q in x ** A )
assume A10: q in [.d,g.[ ; :: thesis: q in x ** A
then reconsider q = q as Real by A8;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A12: q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def 1;
A14: q3 < b
proof
q1 <= g by A10, XXREAL_1:3;
then consider p, o being Real such that
A15: ( p = q1 & o = g ) and
p <= o by A6;
p < o by A10, A15, XXREAL_1:3;
then p / x < o / x by A1, XREAL_1:74;
hence q3 < b by A1, A5, A6, A15, XCMPLX_1:89; :: thesis: verum
end;
a <= q3
proof
( d <= q1 & x * (q / x) = q ) by A1, A10, XCMPLX_1:87, XXREAL_1:3;
hence a <= q3 by A1, A7, A8, XREAL_1:68; :: thesis: verum
end;
hence q / x in A by A2, A14, XXREAL_1:3; :: thesis: verum
end;
q = x * (q / x) by A1, XCMPLX_1:87;
hence q in x ** A by A12, MEMBER_1:193; :: thesis: verum
end;
x ** A c= [.d,g.[
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in [.d,g.[ )
assume A16: q in x ** A ; :: thesis: q in [.d,g.[
then reconsider q = q as Real ;
consider z2 being Real such that
A17: z2 in A and
A18: q = x * z2 by A16, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
z2 <= b by A2, A17, XXREAL_1:3;
then consider 2o, 2r being Real such that
A19: ( 2o = z2 & 2r = b ) and
2o <= 2r by A4;
( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def 1;
then consider 2o1, 2r1 being R_eal such that
A20: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
2o < 2r by A2, A17, A19, XXREAL_1:3;
then A21: 2o1 < 2r1 by A1, A20, XREAL_1:68;
a <= z2 by A2, A17, XXREAL_1:3;
then consider 1o, 1ra being Real such that
A22: ( 1o = a & 1ra = z2 ) and
A23: 1o <= 1ra ;
x * 1o <= x * 1ra by A1, A23, XREAL_1:64;
hence q in [.d,g.[ by A7, A5, A8, A6, A18, A22, A19, A20, A21, XXREAL_1:3; :: thesis: verum
end;
then x ** A = [.d,g.[ by A9;
hence x ** A is right_open_interval by A8, MEASURE5:def 4; :: thesis: verum
end;
case A24: ( a in REAL & b = +infty ) ; :: thesis: x ** A is right_open_interval
consider s being Real such that
A25: s = a ;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A26: d = x * s ;
consider c being R_eal such that
A27: c = +infty ;
A28: [.d,c.[ c= x ** A
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in [.d,c.[ or q in x ** A )
assume A29: q in [.d,c.[ ; :: thesis: q in x ** A
then reconsider q = q as Real by A26;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A30: q1 = q ;
A31: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
A33: a <= q3
proof
( d <= q1 & x * q2 = q ) by A1, A29, A30, XCMPLX_1:87, XXREAL_1:3;
hence a <= q3 by A1, A25, A26, A30, XREAL_1:68; :: thesis: verum
end;
q3 < b by A24, XXREAL_0:9;
hence q2 in A by A2, A33, XXREAL_1:3; :: thesis: verum
end;
q = x * (q / x) by A1, XCMPLX_1:87;
hence q in x ** A by A31, MEMBER_1:193; :: thesis: verum
end;
x ** A c= [.d,c.[
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in [.d,c.[ )
assume A34: q in x ** A ; :: thesis: q in [.d,c.[
then reconsider q = q as Element of REAL ;
consider z2 being Real such that
A35: z2 in A and
A36: q = x * z2 by A34, INTEGRA2:39;
reconsider q = q as R_eal by XXREAL_0:def 1;
A37: q < +infty by XXREAL_0:9;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
a <= z2 by A2, A35, XXREAL_1:3;
then consider o, r being Real such that
A38: ( o = a & r = z2 ) and
A39: o <= r ;
x * o <= x * r by A1, A39, XREAL_1:64;
hence q in [.d,c.[ by A25, A27, A26, A36, A38, A37, XXREAL_1:3; :: thesis: verum
end;
then x ** A = [.d,c.[ by A28;
hence x ** A is right_open_interval by A26, MEASURE5:def 4; :: thesis: verum
end;
end;
end;
hence x ** A is right_open_interval ; :: thesis: verum