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