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