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