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
A3: A = ].a,b.[ by MEASURE5:def 2;
A4: a < b by A3, XXREAL_1:28;
now :: thesis: ( ( 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 ; :: thesis: x ** A is open_interval
now :: thesis: ( ( 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 ) ; :: 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: ].d,+infty.[ c= x ** A
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in ].d,+infty.[ or q in x ** A )
assume A9: q in ].d,+infty.[ ; :: thesis: q in x ** A
then reconsider q = q as Real ;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A10: d < q1 by A9, MEASURE5:def 1;
A11: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
x * q2 = q by A1, XCMPLX_1:87;
then A12: q3 < b by A5, A7, A10, XREAL_1:65;
a < q3 by A6, XXREAL_0:12;
hence q2 in A by A3, A12, MEASURE5:def 1; :: thesis: verum
end;
q = x * (q / x) by A1, XCMPLX_1:87;
hence q in x ** A by A11, MEMBER_1:193; :: thesis: verum
end;
x ** A c= ].d,+infty.[
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in ].d,+infty.[ )
assume A13: q in x ** A ; :: thesis: 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; :: thesis: verum
end;
then x ** A = ].d,+infty.[ by A8;
hence x ** A is open_interval by MEASURE5:def 2; :: 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: ].g,d.[ c= x ** A
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in ].g,d.[ or q in x ** A )
assume A20: 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;
A21: q1 < d by A20, MEASURE5:def 1;
A22: g < q1 by A20, MEASURE5:def 1;
A23: 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:87;
then A24: a < q3 by A5, A21, XREAL_1:65;
q / x < (x * r) / x by A5, A22, XREAL_1:75;
then q3 < b by A5, XCMPLX_1:89;
hence q / x in A by A3, A24, MEASURE5:def 1; :: thesis: verum
end;
q = x * (q / x) by A1, XCMPLX_1:87;
hence q in x ** A by A23, MEMBER_1:193; :: thesis: verum
end;
x ** A c= ].g,d.[
proof
let q be object ; :: 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 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; :: thesis: verum
end;
then x ** A = ].g,d.[ by A19;
hence x ** A is open_interval by MEASURE5:def 2; :: thesis: verum
end;
case A31: ( 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;
A32: ].-infty,d.[ c= x ** A
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in ].-infty,d.[ or q in x ** A )
assume A33: q in ].-infty,d.[ ; :: thesis: q in x ** A
then reconsider q = q as Real ;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A34: q = x * (q / x) by A1, XCMPLX_1:87;
q2 in A hence q in x ** A by A34, MEMBER_1:193; :: thesis: verum
end;
x ** A c= ].-infty,d.[
proof
let q be object ; :: 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 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; :: thesis: verum
end;
then x ** A = ].-infty,d.[ by A32;
hence x ** A is open_interval by MEASURE5:def 2; :: thesis: verum
end;
end;
end;
hence x ** A is open_interval ; :: thesis: verum
end;
case A41: 0 < x ; :: thesis: x ** A is open_interval
now :: thesis: ( ( 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 ) ; :: 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;
A43: ].-infty,d.[ c= x ** A
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in ].-infty,d.[ or q in x ** A )
assume A44: q in ].-infty,d.[ ; :: thesis: q in x ** A
then reconsider q = q as Real ;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A45: q1 < d by A44, MEASURE5:def 1;
A46: q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
x * q2 = q by A1, XCMPLX_1:87;
then A47: q3 < b by A41, A45, XREAL_1:64;
a < q3 by A42, XXREAL_0:12;
hence q2 in A by A3, A47, MEASURE5:def 1; :: thesis: verum
end;
q = x * (q / x) by A1, XCMPLX_1:87;
hence q in x ** A by A46, MEMBER_1:193; :: thesis: verum
end;
x ** A c= ].-infty,d.[
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in ].-infty,d.[ )
assume A48: q in x ** A ; :: thesis: 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; :: thesis: verum
end;
then x ** A = ].-infty,d.[ by A43;
hence x ** A is open_interval by MEASURE5:def 2; :: thesis: verum
end;
case A53: ( 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;
A54: ].d,g.[ c= x ** A
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in ].d,g.[ or q in x ** A )
assume A55: 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
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 by XXREAL_0:def 1;
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; :: thesis: verum
end;
q = x * (q / x) by A1, XCMPLX_1:87;
hence q in x ** A by A59, MEMBER_1:193; :: thesis: verum
end;
x ** A c= ].d,g.[
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in ].d,g.[ )
assume A61: q in x ** A ; :: thesis: 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; :: thesis: verum
end;
then x ** A = ].d,g.[ by A54;
hence x ** A is open_interval by MEASURE5:def 2; :: thesis: verum
end;
case A67: ( a in REAL & b = +infty ) ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not q in x ** A or q in ].d,+infty.[ )
assume A69: q in x ** A ; :: thesis: 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; :: thesis: verum
end;
].d,+infty.[ c= x ** A
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in ].d,+infty.[ or q in x ** A )
assume A74: q in ].d,+infty.[ ; :: thesis: q in x ** A
then reconsider q = q as Real ;
reconsider q2 = q / x as Element of REAL by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A75: q = x * (q / x) by A1, XCMPLX_1:87;
A76: d < q1 by A74, MEASURE5:def 1;
q2 in A
proof
reconsider q3 = q2 as R_eal by XXREAL_0:def 1;
( a < q3 & q3 < b ) by A41, A67, A76, A75, XREAL_1:64, XXREAL_0:9;
hence q2 in A by A3, MEASURE5:def 1; :: thesis: verum
end;
hence q in x ** A by A75, MEMBER_1:193; :: thesis: verum
end;
then x ** A = ].d,+infty.[ by A68;
hence x ** A is open_interval by MEASURE5:def 2; :: thesis: verum
end;
end;
end;
hence x ** A is open_interval ; :: thesis: verum
end;
end;
end;
hence x ** A is open_interval ; :: thesis: verum