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 & 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 A20:
(
a in REAL &
b in REAL )
;
:: thesis: x ** A is left_open_interval then consider s being
Real such that A21:
s = a
;
consider r being
Real such that A22:
r = b
by A20;
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:
x ** A = ].g,d.]
proof
A26:
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 A27:
q in x ** A
;
:: thesis: q in ].g,d.]
then reconsider q =
q as
Real ;
consider z2 being
Real such that A28:
(
z2 in A &
q = x * z2 )
by A27, INTEGRA2:def 2;
reconsider z2 =
z2 as
R_eal by XXREAL_0:def 1;
A29:
(
a <= z2 &
z2 < b )
by A2, A28, XXREAL_1:3;
A30:
(
a <= z2 &
z2 <= b &
z2 <> b )
by A2, A28, XXREAL_1:3;
consider 1o,
1r being
Real such that A31:
(
1o = a &
1r = z2 &
1o <= 1r )
by A20, A29;
consider 2o,
2r being
Real such that A32:
(
2o = z2 &
2r = b &
2o <= 2r )
by A20, A30;
A33:
x * 1r <= x * 1o
by A1, A31, XREAL_1:67;
A34:
2o < 2r
by A2, A28, A32, XXREAL_1:3;
(
x * 2o is
R_eal &
x * 2r is
R_eal )
by XXREAL_0:def 1;
then consider 2o1,
2r1 being
R_eal such that A35:
(
2o1 = x * 2o &
2r1 = x * 2r )
;
2r1 < 2o1
by A1, A34, A35, XREAL_1:71;
hence
q in ].g,d.]
by A21, A22, A23, A24, A28, A31, A32, A33, A35, XXREAL_1:2;
:: thesis: verum
end;
].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 A36:
q in ].g,d.]
;
:: thesis: q in x ** A
then reconsider q =
q as
Real by A23, XREAL_0:def 1;
q is
R_eal
by XXREAL_0:def 1;
then consider q1 being
R_eal such that A37:
q1 = q
;
A38:
(
g < q1 &
q1 <= d &
q1 in REAL )
by A36, A37, XXREAL_1:2;
A39:
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 A40:
q3 = q / x
;
(
a <= q3 &
q3 < b &
q3 in REAL )
proof
A41:
q3 < b
proof
A42:
g < q1
by A36, A37, XXREAL_1:2;
consider p,
o being
Real such that A43:
(
p = g &
o = q1 &
p <= o )
by A24, A38;
o / x < p / x
by A1, A42, A43, XREAL_1:77;
hence
q3 < b
by A1, A22, A24, A37, A40, A43, XCMPLX_1:90;
:: thesis: verum
end;
a <= q3
proof
q1 <= d
by A36, A37, XXREAL_1:2;
then consider r,
o being
Real such that A44:
(
r = q1 &
o = d &
r <= o )
by A23, A37;
x * (q / x) = q
by A1, XCMPLX_1:88;
hence
a <= q3
by A1, A21, A23, A37, A40, A44, XREAL_1:71;
:: thesis: verum
end;
hence
(
a <= q3 &
q3 < b &
q3 in REAL )
by A40, A41;
:: thesis: verum
end;
hence
q / x in A
by A2, A40, XXREAL_1:3;
:: thesis: verum
end;
hence
q in x ** A
by A39, INTEGRA2:def 2;
:: thesis: verum
end;
hence
x ** A = ].g,d.]
by A26, XBOOLE_0:def 10;
:: thesis: verum
end;
x * r <= x * s
by A1, A2, A21, A22, XREAL_1:67;
hence
x ** A is
left_open_interval
by A23, A24, A25, MEASURE5:def 8;
:: thesis: verum end; case A45:
(
a in REAL &
b = +infty )
;
:: thesis: x ** A is left_open_interval then consider s being
Real such that A46:
s = a
;
consider c being
R_eal such that A47:
c = -infty
;
x * s is
R_eal
by XXREAL_0:def 1;
then consider d being
R_eal such that A48:
d = x * s
;
A49:
x ** A = ].c,d.]
proof
A50:
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 A51:
q in x ** A
;
:: thesis: q in ].c,d.]
then reconsider q =
q as
Real ;
consider z2 being
Real such that A52:
(
z2 in A &
q = x * z2 )
by A51, 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 A2, A52, XXREAL_1:3;
then consider o,
r being
Real such that A53:
(
o = a &
r = z2 &
o <= r )
by A45;
A54:
x * r <= x * o
by A1, A53, XREAL_1:67;
-infty < q
by XXREAL_0:12;
hence
q in ].c,d.]
by A46, A47, A48, A52, A53, A54, XXREAL_1:2;
:: thesis: verum
end;
].c,d.] c= x ** A
hence
x ** A = ].c,d.]
by A50, XBOOLE_0:def 10;
:: thesis: verum
end;
c <= d
by A47, XXREAL_0:5;
hence
x ** A is
left_open_interval
by A49, A48, MEASURE5:def 8;
:: thesis: verum end;
hence
x ** A is left_open_interval
; :: thesis: verum