let A be Interval; :: thesis: for x being Real st x <> 0 & A is open_interval holds
x ** A is open_interval
let x be Real; :: thesis: ( x <> 0 & A is open_interval implies x ** A is open_interval )
assume A1: x <> 0 ; :: thesis: ( not A is open_interval or x ** A is open_interval )
assume A2: A is open_interval ; :: thesis: x ** A is open_interval
then consider a, b being R_eal such that
A3: ( a <= b & A = ].a,b.[ ) by MEASURE5:def 5;
now
per cases ( x < 0 or x = 0 or 0 < x ) ;
case A4: x < 0 ; :: thesis: x ** A is open_interval
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 A6: ( a = -infty & b in REAL ) ; :: thesis: 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: x ** A = ].d,+infty .[
proof
A9: x ** A c= ].d,+infty .[
proof
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in ].d,+infty .[ )
assume A10: q in x ** A ; :: thesis: q in ].d,+infty .[
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 A3, A11, MEASURE5:def 2;
then consider r, o being Real such that
A12: ( r = z2 & o = b & r <= o ) by A6;
A13: r < o by A3, A11, A12, MEASURE5:def 2;
reconsider o1 = x * o, r1 = x * r as R_eal by XXREAL_0:def 1;
A14: o1 < r1 by A4, A13, XREAL_1:71;
q < +infty by XXREAL_0:9;
hence q in ].d,+infty .[ by A7, A11, A12, A14, MEASURE5:def 2; :: thesis: verum
end;
].d,+infty .[ c= x ** A
proof
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in ].d,+infty .[ or q in x ** A )
assume A15: q in ].d,+infty .[ ; :: thesis: q in x ** A
then reconsider q = q as Real ;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A16: ( d < q1 & q1 < +infty & q1 in REAL ) by A15, MEASURE5:def 2;
A17: q = x * (q / x) by A1, XCMPLX_1:88;
set q2 = q / x;
q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def 1;
( a < q3 & q3 < b & q3 in REAL )
proof
x * (q / x) = q by A1, XCMPLX_1:88;
hence ( a < q3 & q3 < b & q3 in REAL ) by A4, A6, A7, A16, XREAL_1:67, XXREAL_0:12; :: thesis: verum
end;
hence q / x in A by A3, MEASURE5:def 2; :: thesis: verum
end;
hence q in x ** A by A17, INTEGRA2:def 2; :: thesis: verum
end;
hence x ** A = ].d,+infty .[ by A9, XBOOLE_0:def 10; :: thesis: verum
end;
d <= +infty by XXREAL_0:4;
hence x ** A is open_interval by A8, MEASURE5:def 5; :: thesis: verum
end;
case A18: ( a in REAL & b in REAL ) ; :: thesis: 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: x ** A = ].g,d.[
proof
A20: 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 A21: q in x ** A ; :: thesis: q in ].g,d.[
then reconsider q = q as Real ;
consider z2 being Real such that
A22: ( z2 in A & q = x * z2 ) by A21, INTEGRA2:def 2;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
A23: ( a < z2 & z2 < b ) by A3, A22, MEASURE5:def 2;
then consider 1o, 1r being Real such that
A24: ( 1o = a & 1r = z2 & 1o <= 1r ) by A18;
consider 2o, 2r being Real such that
A25: ( 2o = z2 & 2r = b & 2o <= 2r ) by A18, A23;
A26: 1o < 1r by A3, A22, A24, MEASURE5:def 2;
A27: 2o < 2r by A3, A22, A25, MEASURE5:def 2;
reconsider 1o1 = x * 1o, 1r1 = x * 1r, 2o1 = x * 2o, 2r1 = x * 2r as R_eal by XXREAL_0:def 1;
A28: 1r1 < 1o1 by A4, A26, XREAL_1:71;
2r1 < 2o1 by A4, A27, XREAL_1:71;
hence q in ].g,d.[ by A22, A24, A25, A28, MEASURE5:def 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 A29: q in ].g,d.[ ; :: thesis: q in x ** A
then reconsider q = q as Real ;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A30: ( g < q1 & q1 < d & q1 in REAL ) by A29, MEASURE5:def 2;
A31: q = x * (q / x) by A1, XCMPLX_1:88;
set q2 = q / x;
q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def 1;
( a < q3 & q3 < b & q3 in REAL )
proof
A32: q3 < b
proof
q / x < (x * r) / x by A4, A30, XREAL_1:77;
hence q3 < b by A4, XCMPLX_1:90; :: thesis: verum
end;
a < q3
proof
x * (q / x) = q by A1, XCMPLX_1:88;
hence a < q3 by A4, A30, XREAL_1:67; :: thesis: verum
end;
hence ( a < q3 & q3 < b & q3 in REAL ) by A32; :: thesis: verum
end;
hence q / x in A by A3, MEASURE5:def 2; :: thesis: verum
end;
hence q in x ** A by A31, INTEGRA2:def 2; :: thesis: verum
end;
hence x ** A = ].g,d.[ by A20, XBOOLE_0:def 10; :: thesis: verum
end;
x * r <= x * s by A3, A4, XREAL_1:67;
hence x ** A is open_interval by A19, MEASURE5:def 5; :: thesis: verum
end;
case A33: ( a in REAL & b = +infty ) ; :: thesis: 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;
A34: x ** A = ].-infty ,d.[
proof
A35: x ** A c= ].-infty ,d.[
proof
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in ].-infty ,d.[ )
assume A36: q in x ** A ; :: thesis: q in ].-infty ,d.[
then reconsider q = q as Real ;
consider z2 being Real such that
A37: ( z2 in A & q = x * z2 ) by A36, INTEGRA2:def 2;
reconsider z2 = z2, q = q as R_eal by XXREAL_0:def 1;
( a < z2 & z2 < b ) by A3, A37, MEASURE5:def 2;
then consider o, r being Real such that
A38: ( o = a & r = z2 & o <= r ) by A33;
A39: o < r by A3, A37, A38, MEASURE5:def 2;
reconsider o1 = x * o, r1 = x * r as R_eal by XXREAL_0:def 1;
A40: r1 < o1 by A4, A39, XREAL_1:71;
-infty < q by XXREAL_0:12;
hence q in ].-infty ,d.[ by A37, A38, A40, MEASURE5:def 2; :: thesis: verum
end;
].-infty ,d.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in ].-infty ,d.[ or q in x ** A )
assume A41: q in ].-infty ,d.[ ; :: thesis: q in x ** A
then reconsider q = q as Real ;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A42: q = x * (q / x) by A1, XCMPLX_1:88;
set q2 = q / x;
q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def 1;
( a < q3 & q3 < b & q3 in REAL )
proof
a < q3
proof
( q1 <= d & q1 <> d ) by A41, MEASURE5:def 2;
then x * (q / x) < x * s by A42, XXREAL_0:1;
hence a < q3 by A4, XREAL_1:67; :: thesis: verum
end;
hence ( a < q3 & q3 < b & q3 in REAL ) by A33, XXREAL_0:9; :: thesis: verum
end;
hence q / x in A by A3, MEASURE5:def 2; :: thesis: verum
end;
hence q in x ** A by A42, INTEGRA2:def 2; :: thesis: verum
end;
hence x ** A = ].-infty ,d.[ by A35, XBOOLE_0:def 10; :: thesis: verum
end;
-infty <= d by XXREAL_0:5;
hence x ** A is open_interval by A34, MEASURE5:def 5; :: thesis: verum
end;
end;
end;
hence x ** A is open_interval ; :: thesis: verum
end;
case A44: 0 < x ; :: thesis: x ** A is open_interval
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 A46: ( a = -infty & b in REAL ) ; :: thesis: 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;
A47: x ** A = ].-infty ,d.[
proof
A48: x ** A c= ].-infty ,d.[
proof
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in ].-infty ,d.[ )
assume A49: q in x ** A ; :: thesis: q in ].-infty ,d.[
then reconsider q = q as Real ;
consider z2 being Real such that
A50: ( z2 in A & q = x * z2 ) by A49, INTEGRA2:def 2;
reconsider z2 = z2, q = q as R_eal by XXREAL_0:def 1;
( a < z2 & z2 < b ) by A3, A50, MEASURE5:def 2;
then consider r, o being Real such that
A51: ( r = z2 & o = b & r <= o ) by A46;
A52: r < o by A3, A50, A51, MEASURE5:def 2;
reconsider o1 = x * o, r1 = x * r as R_eal by XXREAL_0:def 1;
A53: r1 < o1 by A44, A52, XREAL_1:70;
-infty < q by XXREAL_0:12;
hence q in ].-infty ,d.[ by A50, A51, A53, MEASURE5:def 2; :: thesis: verum
end;
].-infty ,d.[ c= x ** A
proof
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in ].-infty ,d.[ or q in x ** A )
assume A54: q in ].-infty ,d.[ ; :: thesis: q in x ** A
then reconsider q = q as Real ;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A55: ( -infty < q1 & q1 < d & q1 in REAL ) by A54, MEASURE5:def 2;
A56: q = x * (q / x) by A1, XCMPLX_1:88;
set q2 = q / x;
q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def 1;
( a < q3 & q3 < b & q3 in REAL )
proof
q3 < b
proof
x * (q / x) = q by A1, XCMPLX_1:88;
hence q3 < b by A44, A55, XREAL_1:66; :: thesis: verum
end;
hence ( a < q3 & q3 < b & q3 in REAL ) by A46, XXREAL_0:12; :: thesis: verum
end;
hence q / x in A by A3, MEASURE5:def 2; :: thesis: verum
end;
hence q in x ** A by A56, INTEGRA2:def 2; :: thesis: verum
end;
hence x ** A = ].-infty ,d.[ by A48, XBOOLE_0:def 10; :: thesis: verum
end;
-infty <= d by XXREAL_0:5;
hence x ** A is open_interval by A47, MEASURE5:def 5; :: thesis: verum
end;
case A57: ( a in REAL & b in REAL ) ; :: thesis: 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;
A58: x ** A = ].d,g.[
proof
A59: 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 A60: q in x ** A ; :: thesis: q in ].d,g.[
then reconsider q = q as Real ;
consider z2 being Real such that
A61: ( z2 in A & q = x * z2 ) by A60, INTEGRA2:def 2;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
A62: ( a < z2 & z2 < b ) by A3, A61, MEASURE5:def 2;
then consider 1o, 1r being Real such that
A63: ( 1o = a & 1r = z2 & 1o <= 1r ) by A57;
consider 2o, 2r being Real such that
A64: ( 2o = z2 & 2r = b & 2o <= 2r ) by A57, A62;
A65: 1o < 1r by A3, A61, A63, MEASURE5:def 2;
A66: 2o < 2r by A3, A61, A64, MEASURE5:def 2;
reconsider 1o1 = x * 1o, 1r1 = x * 1r as R_eal by XXREAL_0:def 1;
reconsider 2o1 = x * 2o, 2r1 = x * 2r as R_eal by XXREAL_0:def 1;
A67: 1o1 < 1r1 by A44, A65, XREAL_1:70;
2o1 < 2r1 by A44, A66, XREAL_1:70;
hence q in ].d,g.[ by A61, A63, A64, A67, MEASURE5:def 2; :: 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 A68: q in ].d,g.[ ; :: thesis: q in x ** A
then reconsider q = q as Real ;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A69: q1 = q ;
A70: ( d < q1 & q1 < g & q1 in REAL ) by A68, A69, MEASURE5:def 2;
A71: q = x * (q / x) by A1, XCMPLX_1:88;
set q2 = q / x;
q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def 1;
( a < q3 & q3 < b & q3 in REAL )
proof
A72: q3 < b
proof
q / x < (x * r) / x by A44, A69, A70, XREAL_1:76;
hence q3 < b by A44, XCMPLX_1:90; :: thesis: verum
end;
a < q3
proof
x * (q / x) = q by A1, XCMPLX_1:88;
hence a < q3 by A44, A69, A70, XREAL_1:66; :: thesis: verum
end;
hence ( a < q3 & q3 < b & q3 in REAL ) by A72; :: thesis: verum
end;
hence q / x in A by A3, MEASURE5:def 2; :: thesis: verum
end;
hence q in x ** A by A71, INTEGRA2:def 2; :: thesis: verum
end;
hence x ** A = ].d,g.[ by A59, XBOOLE_0:def 10; :: thesis: verum
end;
x * s <= x * r by A3, A44, XREAL_1:66;
hence x ** A is open_interval by A58, MEASURE5:def 5; :: thesis: verum
end;
case A73: ( a in REAL & b = +infty ) ; :: thesis: 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;
A74: x ** A = ].d,+infty .[
proof
A75: x ** A c= ].d,+infty .[
proof
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in ].d,+infty .[ )
assume A76: q in x ** A ; :: thesis: q in ].d,+infty .[
then reconsider q = q as Real ;
consider z2 being Real such that
A77: ( z2 in A & q = x * z2 ) by A76, 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, A77, MEASURE5:def 2;
then consider o, r being Real such that
A78: ( o = a & r = z2 & o <= r ) by A73;
A79: o < r by A3, A77, A78, MEASURE5:def 2;
reconsider o1 = x * o, r1 = x * r as R_eal by XXREAL_0:def 1;
A80: o1 < r1 by A44, A79, XREAL_1:70;
q < +infty by XXREAL_0:9;
hence q in ].d,+infty .[ by A77, A78, A80, MEASURE5:def 2; :: thesis: verum
end;
].d,+infty .[ c= x ** A
proof
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in ].d,+infty .[ or q in x ** A )
assume A81: q in ].d,+infty .[ ; :: thesis: q in x ** A
then reconsider q = q as Real ;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A82: ( d < q1 & q1 < +infty & q1 in REAL ) by A81, MEASURE5:def 2;
A83: q = x * (q / x) by A1, XCMPLX_1:88;
set q2 = q / x;
q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def 1;
( a < q3 & q3 < b & q3 in REAL ) by A44, A73, A82, A83, XREAL_1:66, XXREAL_0:9;
hence q / x in A by A3, MEASURE5:def 2; :: thesis: verum
end;
hence q in x ** A by A83, INTEGRA2:def 2; :: thesis: verum
end;
hence x ** A = ].d,+infty .[ by A75, XBOOLE_0:def 10; :: thesis: verum
end;
d <= +infty by XXREAL_0:4;
hence x ** A is open_interval by A74, MEASURE5:def 5; :: thesis: verum
end;
end;
end;
hence x ** A is open_interval ; :: thesis: verum
end;
end;
end;
hence x ** A is open_interval ; :: thesis: verum