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