let A be Interval; :: thesis: for x being Real st 0 < x & A is right_open_interval holds
x ** A is right_open_interval
let x be Real; :: thesis: ( 0 < x & A is right_open_interval implies x ** A is right_open_interval )
assume A1:
0 < x
; :: thesis: ( not A is right_open_interval or x ** A is right_open_interval )
assume
A is right_open_interval
; :: thesis: x ** A is right_open_interval
then consider a being real number , b being R_eal such that
A3:
( 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 A3, Th6;
case A18:
(
a in REAL &
b in REAL )
;
:: thesis: x ** A is right_open_interval then consider s being
Real such that A19:
s = a
;
consider r being
Real such that A20:
r = b
by A18;
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 = [.d,g.[
proof
A24:
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 A25:
q in x ** A
;
:: thesis: q in [.d,g.[
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 < b )
by A3, A26, XXREAL_1:3;
A28:
(
a <= z2 &
z2 <= b &
z2 <> b )
by A3, A26, XXREAL_1:3;
consider 1o,
1r being
Real such that A29:
(
1o = a &
1r = z2 &
1o <= 1r )
by A18, A27;
consider 2o,
2r being
Real such that A30:
(
2o = z2 &
2r = b &
2o <= 2r )
by A18, A28;
A31:
x * 1o <= x * 1r
by A1, A29, XREAL_1:66;
A32:
2o < 2r
by A3, A26, A30, 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 A33:
(
2o1 = x * 2o &
2r1 = x * 2r )
;
2o1 < 2r1
by A1, A32, A33, XREAL_1:70;
hence
q in [.d,g.[
by A19, A20, A21, A22, A26, A29, A30, A31, A33, XXREAL_1:3;
:: 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 A34:
q in [.d,g.[
;
:: thesis: q in x ** A
then reconsider q =
q as
Real by A21, XREAL_0:def 1;
q is
R_eal
by XXREAL_0:def 1;
then consider q1 being
R_eal such that A35:
q1 = q
;
A36:
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 A37:
q3 = q / x
;
(
a <= q3 &
q3 < b &
q3 in REAL )
proof
A38:
q3 < b
proof
(
q1 <= g &
q1 <> g )
by A34, A35, XXREAL_1:3;
then consider p,
o being
Real such that A39:
(
p = q1 &
o = g &
p <= o )
by A22, A35;
p < o
by A34, A35, A39, XXREAL_1:3;
then
p / x < o / x
by A1, XREAL_1:76;
hence
q3 < b
by A1, A20, A22, A35, A37, A39, XCMPLX_1:90;
:: thesis: verum
end;
a <= q3
proof
d <= q1
by A34, A35, XXREAL_1:3;
then consider r,
o being
Real such that A40:
(
r = d &
o = q1 &
r <= o )
by A21, A35;
x * (q / x) = q
by A1, XCMPLX_1:88;
hence
a <= q3
by A1, A19, A21, A35, A37, A40, XREAL_1:70;
:: thesis: verum
end;
hence
(
a <= q3 &
q3 < b &
q3 in REAL )
by A37, A38;
:: thesis: verum
end;
hence
q / x in A
by A3, A37, XXREAL_1:3;
:: thesis: verum
end;
hence
q in x ** A
by A36, INTEGRA2:def 2;
:: thesis: verum
end;
hence
x ** A = [.d,g.[
by A24, XBOOLE_0:def 10;
:: thesis: verum
end;
x * s <= x * r
by A1, A3, A19, A20, XREAL_1:66;
hence
x ** A is
right_open_interval
by A21, A22, A23, MEASURE5:def 7;
:: thesis: verum end; case A41:
(
a in REAL &
b = +infty )
;
:: thesis: x ** A is right_open_interval then consider s being
Real such that A42:
s = a
;
consider c being
R_eal such that A43:
c = +infty
;
x * s is
R_eal
by XXREAL_0:def 1;
then consider d being
R_eal such that A44:
d = x * s
;
A45:
x ** A = [.d,c.[
proof
A46:
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 A47:
q in x ** A
;
:: thesis: q in [.d,c.[
then reconsider q =
q as
Real ;
consider z2 being
Real such that A48:
(
z2 in A &
q = x * z2 )
by A47, 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, A48, XXREAL_1:3;
then consider o,
r being
Real such that A49:
(
o = a &
r = z2 &
o <= r )
by A41;
A50:
x * o <= x * r
by A1, A49, XREAL_1:66;
q < +infty
by XXREAL_0:9;
hence
q in [.d,c.[
by A42, A43, A44, A48, A49, A50, 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 A51:
q in [.d,c.[
;
:: thesis: q in x ** A
then reconsider q =
q as
Real by A44, XREAL_0:def 1;
q is
R_eal
by XXREAL_0:def 1;
then consider q1 being
R_eal such that A52:
q1 = q
;
A53:
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 A54:
q3 = q / x
;
(
a <= q3 &
q3 < b &
q3 in REAL )
proof
a <= q3
proof
d <= q1
by A51, A52, XXREAL_1:3;
then consider r,
o being
Real such that A55:
(
r = d &
o = q1 &
r <= o )
by A44, A52;
x * (q / x) = q
by A1, XCMPLX_1:88;
hence
a <= q3
by A1, A42, A44, A52, A54, A55, XREAL_1:70;
:: thesis: verum
end;
hence
(
a <= q3 &
q3 < b &
q3 in REAL )
by A41, A54, XXREAL_0:9;
:: thesis: verum
end;
hence
q / x in A
by A3, A54, XXREAL_1:3;
:: thesis: verum
end;
hence
q in x ** A
by A53, INTEGRA2:def 2;
:: thesis: verum
end;
hence
x ** A = [.d,c.[
by A46, XBOOLE_0:def 10;
:: thesis: verum
end;
d <= c
by A43, XXREAL_0:4;
hence
x ** A is
right_open_interval
by A45, A44, MEASURE5:def 7;
:: thesis: verum end;
hence
x ** A is right_open_interval
; :: thesis: verum