let A be Interval; :: thesis: for x being Real st 0 < x & A is left_open_interval holds
x ** A is left_open_interval
let x be Real; :: thesis: ( 0 < x & A is left_open_interval implies x ** A is left_open_interval )
assume A1: 0 < x ; :: thesis: ( not A is left_open_interval or x ** A is left_open_interval )
assume A is left_open_interval ; :: thesis: x ** A is left_open_interval
then consider a being R_eal, b being real number such that
A2: a <= b and
A3: A = ].a,b.] by MEASURE5:def 8;
reconsider b = b as R_eal by XXREAL_0:def 1;
now
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 A2, Th6;
case A4: ( a = -infty & b in REAL ) ; :: thesis: x ** A is left_open_interval
then consider s being Real such that
A5: s = b ;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A6: d = x * s ;
consider c being R_eal such that
A7: c = -infty ;
A8: ].c,d.] c= x ** A
proof
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in ].c,d.] or q in x ** A )
assume A9: q in ].c,d.] ; :: thesis: q in x ** A
then reconsider q = q as Real by A6, XREAL_0:def 1;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A10: q / x in A
proof
q / x is R_eal by XXREAL_0:def 1;
then consider q3 being R_eal such that
A11: q3 = q / x ;
A12: q3 <= b
proof
( q1 <= d & x * (q / x) = q ) by A1, A9, XCMPLX_1:88, XXREAL_1:2;
hence q3 <= b by A1, A5, A6, A11, XREAL_1:70; :: thesis: verum
end;
a < q3 by A4, A11, XXREAL_0:12;
hence q / x in A by A3, A11, A12, XXREAL_1:2; :: thesis: verum
end;
q = x * (q / x) by A1, XCMPLX_1:88;
hence q in x ** A by A10, INTEGRA2:def 2; :: thesis: verum
end;
A13: c <= d by A7, XXREAL_0:5;
x ** A c= ].c,d.]
proof
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in ].c,d.] )
assume A14: q in x ** A ; :: thesis: q in ].c,d.]
then reconsider q = q as Real ;
consider z2 being Real such that
A15: z2 in A and
A16: q = x * z2 by A14, INTEGRA2:def 2;
reconsider q = q as R_eal by XXREAL_0:def 1;
A17: -infty < q by XXREAL_0:12;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
z2 <= b by A3, A15, XXREAL_1:2;
then consider r, o being Real such that
A18: ( r = z2 & o = b ) and
A19: r <= o by A4;
x * r <= x * o by A1, A19, XREAL_1:66;
hence q in ].c,d.] by A5, A7, A6, A16, A18, A17, XXREAL_1:2; :: thesis: verum
end;
then x ** A = ].c,d.] by A8, XBOOLE_0:def 10;
hence x ** A is left_open_interval by A6, A13, MEASURE5:def 8; :: thesis: verum
end;
case A20: ( a in REAL & b in REAL ) ; :: thesis: x ** A is left_open_interval
then reconsider s = a as Real ;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A21: d = x * s ;
consider r being Real such that
A22: r = b by A20;
x * r is R_eal by XXREAL_0:def 1;
then consider g being R_eal such that
A23: g = x * r ;
A24: ].d,g.] c= x ** A
proof
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in ].d,g.] or q in x ** A )
assume A25: q in ].d,g.] ; :: thesis: q in x ** A
then reconsider q = q as Real by A23, XREAL_0:def 1;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A26: q / x in A
proof
q / x is R_eal by XXREAL_0:def 1;
then consider q3 being R_eal such that
A27: q3 = q / x ;
A28: q3 <= b
proof
q1 <= g by A25, XXREAL_1:2;
then consider p, o being Real such that
A29: ( p = q1 & o = g ) and
A30: p <= o by A23;
p / x <= o / x by A1, A30, XREAL_1:74;
hence q3 <= b by A1, A22, A23, A27, A29, XCMPLX_1:90; :: thesis: verum
end;
( d < q1 & x * (q / x) = q ) by A1, A25, XCMPLX_1:88, XXREAL_1:2;
then a < q3 by A1, A21, A27, XREAL_1:66;
hence q / x in A by A3, A27, A28, XXREAL_1:2; :: thesis: verum
end;
q = x * (q / x) by A1, XCMPLX_1:88;
hence q in x ** A by A26, INTEGRA2:def 2; :: thesis: verum
end;
A31: x * s <= x * r by A1, A2, A22, XREAL_1:66;
x ** A c= ].d,g.]
proof
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in ].d,g.] )
assume A32: q in x ** A ; :: thesis: q in ].d,g.]
then reconsider q = q as Real ;
consider z2 being Real such that
A33: z2 in A and
A34: q = x * z2 by A32, INTEGRA2:def 2;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
a <= z2 by A3, A33, XXREAL_1:2;
then consider 1o, 1ra being Real such that
A35: ( 1o = a & 1ra = z2 ) and
1o <= 1ra by A20;
1o < 1ra by A3, A33, A35, XXREAL_1:2;
then A36: x * 1o < x * 1ra by A1, XREAL_1:70;
z2 <= b by A3, A33, XXREAL_1:2;
then consider 2o, 2r being Real such that
A37: ( 2o = z2 & 2r = b ) and
A38: 2o <= 2r by A20;
( x * 2o is R_eal & x * 2r is R_eal ) by XXREAL_0:def 1;
then consider 2o1, 2r1 being R_eal such that
A39: ( 2o1 = x * 2o & 2r1 = x * 2r ) ;
2o1 <= 2r1 by A1, A38, A39, XREAL_1:66;
hence q in ].d,g.] by A22, A21, A23, A34, A35, A37, A36, A39, XXREAL_1:2; :: thesis: verum
end;
then x ** A = ].d,g.] by A24, XBOOLE_0:def 10;
hence x ** A is left_open_interval by A21, A23, A31, MEASURE5:def 8; :: thesis: verum
end;
end;
end;
hence x ** A is left_open_interval ; :: thesis: verum