let A be non empty Interval; for x being Real st x <> 0 & A is open_interval holds
x ** A is open_interval
let x be Real; ( x <> 0 & A is open_interval implies x ** A is open_interval )
assume A1:
x <> 0
; ( not A is open_interval or x ** A is open_interval )
assume A2:
A is open_interval
; x ** A is open_interval
then consider a, b being R_eal such that
A3:
A = ].a,b.[
by MEASURE5:def 2;
A4:
a < b
by A3, XXREAL_1:28;
now ( ( x < 0 & x ** A is open_interval ) or ( x = 0 & x ** A is open_interval ) or ( 0 < x & x ** A is open_interval ) )per cases
( x < 0 or x = 0 or 0 < x )
;
case A5:
x < 0
;
x ** A is open_interval now ( ( a = -infty & b = -infty & x ** A is open_interval ) or ( a = -infty & b in REAL & x ** A is open_interval ) or ( a = -infty & b = +infty & x ** A is open_interval ) or ( a in REAL & b in REAL & x ** A is open_interval ) or ( a in REAL & b = +infty & x ** A is open_interval ) or ( a = +infty & b = +infty & x ** A is open_interval ) )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 A4, Th5;
case A6:
(
a = -infty &
b in REAL )
;
x ** A is open_interval then reconsider s =
b as
Real ;
set 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:
].d,+infty.[ c= x ** A
x ** A c= ].d,+infty.[
proof
let q be
object ;
TARSKI:def 3 ( not q in x ** A or q in ].d,+infty.[ )
assume A13:
q in x ** A
;
q in ].d,+infty.[
then reconsider q =
q as
Element of
REAL ;
consider z2 being
Real such that A14:
z2 in A
and A15:
q = x * z2
by A13, INTEGRA2:39;
reconsider q =
q as
R_eal by XXREAL_0:def 1;
A16:
q < +infty
by XXREAL_0:9;
reconsider z2 =
z2 as
R_eal by XXREAL_0:def 1;
z2 < b
by A3, A14, MEASURE5:def 1;
then consider r,
o being
Real such that A17:
(
r = z2 &
o = b )
and
r <= o
by A6;
reconsider o1 =
x * o,
r1 =
x * r as
R_eal by XXREAL_0:def 1;
r < o
by A3, A14, A17, MEASURE5:def 1;
then
o1 < r1
by A5, XREAL_1:69;
hence
q in ].d,+infty.[
by A7, A15, A17, A16, MEASURE5:def 1;
verum
end; then
x ** A = ].d,+infty.[
by A8;
hence
x ** A is
open_interval
by MEASURE5:def 2;
verum end; case A18:
(
a in REAL &
b in REAL )
;
x ** A is open_interval then reconsider s =
a,
r =
b as
Real ;
reconsider d =
x * s,
g =
x * r as
R_eal by XXREAL_0:def 1;
A19:
].g,d.[ c= x ** A
x ** A c= ].g,d.[
proof
let q be
object ;
TARSKI:def 3 ( not q in x ** A or q in ].g,d.[ )
assume A25:
q in x ** A
;
q in ].g,d.[
then reconsider q =
q as
Real ;
consider z2 being
Real such that A26:
z2 in A
and A27:
q = x * z2
by A25, INTEGRA2:39;
reconsider z2 =
z2 as
R_eal by XXREAL_0:def 1;
a < z2
by A3, A26, MEASURE5:def 1;
then consider 1o,
1ra being
Real such that A28:
(
1o = a &
1ra = z2 )
and
1o <= 1ra
by A18;
z2 < b
by A3, A26, MEASURE5:def 1;
then consider 2o,
2r being
Real such that A29:
(
2o = z2 &
2r = b )
and
2o <= 2r
by A18;
reconsider 1o1 =
x * 1o,
1r1 =
x * 1ra,
2o1 =
x * 2o,
2r1 =
x * 2r as
R_eal by XXREAL_0:def 1;
2o < 2r
by A3, A26, A29, MEASURE5:def 1;
then A30:
2r1 < 2o1
by A5, XREAL_1:69;
1o < 1ra
by A3, A26, A28, MEASURE5:def 1;
then
1r1 < 1o1
by A5, XREAL_1:69;
hence
q in ].g,d.[
by A27, A28, A29, A30, MEASURE5:def 1;
verum
end; then
x ** A = ].g,d.[
by A19;
hence
x ** A is
open_interval
by MEASURE5:def 2;
verum end; case A31:
(
a in REAL &
b = +infty )
;
x ** A is open_interval then reconsider s =
a as
Real ;
set c =
-infty ;
reconsider d =
x * s as
R_eal by XXREAL_0:def 1;
A32:
].-infty,d.[ c= x ** A
x ** A c= ].-infty,d.[
proof
let q be
object ;
TARSKI:def 3 ( not q in x ** A or q in ].-infty,d.[ )
assume A36:
q in x ** A
;
q in ].-infty,d.[
then reconsider q =
q as
Element of
REAL ;
consider z2 being
Real such that A37:
z2 in A
and A38:
q = x * z2
by A36, INTEGRA2:39;
reconsider z2 =
z2,
q =
q as
R_eal by XXREAL_0:def 1;
a < z2
by A3, A37, MEASURE5:def 1;
then consider o,
r being
Real such that A39:
(
o = a &
r = z2 )
and
o <= r
by A31;
reconsider o1 =
x * o,
r1 =
x * r as
R_eal by XXREAL_0:def 1;
A40:
-infty < q
by XXREAL_0:12;
o < r
by A3, A37, A39, MEASURE5:def 1;
then
r1 < o1
by A5, XREAL_1:69;
hence
q in ].-infty,d.[
by A38, A39, A40, MEASURE5:def 1;
verum
end; then
x ** A = ].-infty,d.[
by A32;
hence
x ** A is
open_interval
by MEASURE5:def 2;
verum end; end; end; hence
x ** A is
open_interval
;
verum end; case A41:
0 < x
;
x ** A is open_interval now ( ( a = -infty & b = -infty & x ** A is open_interval ) or ( a = -infty & b in REAL & x ** A is open_interval ) or ( a = -infty & b = +infty & x ** A is open_interval ) or ( a in REAL & b in REAL & x ** A is open_interval ) or ( a in REAL & b = +infty & x ** A is open_interval ) or ( a = +infty & b = +infty & x ** A is open_interval ) )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 A4, Th5;
case A42:
(
a = -infty &
b in REAL )
;
x ** A is open_interval then reconsider s =
b as
Real ;
set c =
-infty ;
reconsider d =
x * s as
R_eal by XXREAL_0:def 1;
A43:
].-infty,d.[ c= x ** A
x ** A c= ].-infty,d.[
proof
let q be
object ;
TARSKI:def 3 ( not q in x ** A or q in ].-infty,d.[ )
assume A48:
q in x ** A
;
q in ].-infty,d.[
then reconsider q =
q as
Element of
REAL ;
consider z2 being
Real such that A49:
z2 in A
and A50:
q = x * z2
by A48, INTEGRA2:39;
reconsider z2 =
z2,
q =
q as
R_eal by XXREAL_0:def 1;
z2 < b
by A3, A49, MEASURE5:def 1;
then consider r,
o being
Real such that A51:
(
r = z2 &
o = b )
and
r <= o
by A42;
reconsider o1 =
x * o,
r1 =
x * r as
R_eal by XXREAL_0:def 1;
A52:
-infty < q
by XXREAL_0:12;
r < o
by A3, A49, A51, MEASURE5:def 1;
then
r1 < o1
by A41, XREAL_1:68;
hence
q in ].-infty,d.[
by A50, A51, A52, MEASURE5:def 1;
verum
end; then
x ** A = ].-infty,d.[
by A43;
hence
x ** A is
open_interval
by MEASURE5:def 2;
verum end; case A53:
(
a in REAL &
b in REAL )
;
x ** A is open_interval then reconsider s =
a,
r =
b as
Real ;
reconsider d =
x * s as
R_eal by XXREAL_0:def 1;
reconsider g =
x * r as
R_eal by XXREAL_0:def 1;
A54:
].d,g.[ c= x ** A
proof
let q be
object ;
TARSKI:def 3 ( not q in ].d,g.[ or q in x ** A )
assume A55:
q in ].d,g.[
;
q in x ** A
then reconsider q =
q as
Real ;
set q2 =
q / x;
q is
R_eal
by XXREAL_0:def 1;
then consider q1 being
R_eal such that A56:
q1 = q
;
A57:
q1 < g
by A55, A56, MEASURE5:def 1;
A58:
d < q1
by A55, A56, MEASURE5:def 1;
A59:
q / x in A
proof
reconsider q3 =
q / x as
R_eal ;
x * (q / x) = q
by A1, XCMPLX_1:87;
then A60:
a < q3
by A41, A56, A58, XREAL_1:64;
q / x < (x * r) / x
by A41, A56, A57, XREAL_1:74;
then
q3 < b
by A41, XCMPLX_1:89;
hence
q / x in A
by A3, A60, MEASURE5:def 1;
verum
end;
q = x * (q / x)
by A1, XCMPLX_1:87;
hence
q in x ** A
by A59, MEMBER_1:193;
verum
end;
x ** A c= ].d,g.[
proof
let q be
object ;
TARSKI:def 3 ( not q in x ** A or q in ].d,g.[ )
assume A61:
q in x ** A
;
q in ].d,g.[
then reconsider q =
q as
Real ;
consider z2 being
Real such that A62:
z2 in A
and A63:
q = x * z2
by A61, INTEGRA2:39;
reconsider z2 =
z2 as
R_eal by XXREAL_0:def 1;
z2 < b
by A3, A62, MEASURE5:def 1;
then consider 2o,
2r being
Real such that A64:
(
2o = z2 &
2r = b )
and
2o <= 2r
by A53;
reconsider 2o1 =
x * 2o,
2r1 =
x * 2r as
R_eal by XXREAL_0:def 1;
2o < 2r
by A3, A62, A64, MEASURE5:def 1;
then A65:
2o1 < 2r1
by A41, XREAL_1:68;
a < z2
by A3, A62, MEASURE5:def 1;
then consider 1o,
1ra being
Real such that A66:
(
1o = a &
1ra = z2 )
and
1o <= 1ra
by A53;
reconsider 1o1 =
x * 1o,
1r1 =
x * 1ra as
R_eal by XXREAL_0:def 1;
1o < 1ra
by A3, A62, A66, MEASURE5:def 1;
then
1o1 < 1r1
by A41, XREAL_1:68;
hence
q in ].d,g.[
by A63, A66, A64, A65, MEASURE5:def 1;
verum
end; then
x ** A = ].d,g.[
by A54;
hence
x ** A is
open_interval
by MEASURE5:def 2;
verum end; case A67:
(
a in REAL &
b = +infty )
;
x ** A is open_interval then reconsider s =
a as
Element of
REAL ;
set c =
+infty ;
reconsider d =
x * s as
R_eal by XXREAL_0:def 1;
A68:
x ** A c= ].d,+infty.[
proof
let q be
object ;
TARSKI:def 3 ( not q in x ** A or q in ].d,+infty.[ )
assume A69:
q in x ** A
;
q in ].d,+infty.[
then reconsider q =
q as
Element of
REAL ;
consider z2 being
Real such that A70:
z2 in A
and A71:
q = x * z2
by A69, INTEGRA2:39;
reconsider q =
q as
R_eal by XXREAL_0:def 1;
A72:
q < +infty
by XXREAL_0:9;
reconsider z2 =
z2 as
R_eal by XXREAL_0:def 1;
a < z2
by A3, A70, MEASURE5:def 1;
then consider o,
r being
Real such that A73:
(
o = a &
r = z2 )
and
o <= r
by A67;
reconsider o1 =
x * o,
r1 =
x * r as
R_eal by XXREAL_0:def 1;
o < r
by A3, A70, A73, MEASURE5:def 1;
then
o1 < r1
by A41, XREAL_1:68;
hence
q in ].d,+infty.[
by A71, A73, A72, MEASURE5:def 1;
verum
end;
].d,+infty.[ c= x ** A
then
x ** A = ].d,+infty.[
by A68;
hence
x ** A is
open_interval
by MEASURE5:def 2;
verum end; end; end; hence
x ** A is
open_interval
;
verum end; end; end;
hence
x ** A is open_interval
; verum