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