let A be non empty Interval; :: thesis: for x being Real st x <> 0 & A is closed_interval holds
x ** A is closed_interval
let x be Real; :: thesis: ( x <> 0 & A is closed_interval implies x ** A is closed_interval )
assume A1: x <> 0 ; :: thesis: ( not A is closed_interval or x ** A is closed_interval )
assume A is closed_interval ; :: thesis: x ** A is closed_interval
then consider a, b being real number such that
A2: A = [.a,b.] by MEASURE5:def 3;
reconsider a = a, b = b as R_eal by XXREAL_0:def 1;
now
per cases ( x < 0 or x = 0 or 0 < x ) ;
case A3: x < 0 ; :: thesis: x ** A is closed_interval
now
reconsider s = a, r = b as Real by Th6;
reconsider d = x * s as R_eal by XXREAL_0:def 1;
reconsider g = x * r as R_eal by XXREAL_0:def 1;
A4: b in REAL by Th6;
A5: [.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 A6: q in [.g,d.] ; :: thesis: q in x ** A
then reconsider q = q as Real by XREAL_0:def 1;
set q2 = q / x;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A7: g <= q1 by A6, XXREAL_1:1;
A8: q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def 1;
A9: q3 <= b
proof
consider p, o being Real such that
A10: ( p = g & o = q1 ) and
A11: p <= o by A7;
o / x <= p / x by A3, A11, XREAL_1:73;
hence q3 <= b by A3, A10, XCMPLX_1:89; :: thesis: verum
end;
a <= q3
proof
( q1 <= d & x * (q / x) = q ) by A1, A6, XCMPLX_1:87, XXREAL_1:1;
hence a <= q3 by A3, XREAL_1:69; :: thesis: verum
end;
hence q / x in A by A2, A9, XXREAL_1:1; :: thesis: verum
end;
q = x * (q / x) by A1, XCMPLX_1:87;
hence q in x ** A by A8, MEMBER_1:193; :: thesis: verum
end;
A12: a in REAL by Th6;
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 A13: q in x ** A ; :: thesis: q in [.g,d.]
then reconsider q = q as Real ;
consider z2 being Real such that
A14: z2 in A and
A15: q = x * z2 by A13, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
a <= z2 by A2, A14, XXREAL_1:1;
then consider 1o, 1ra being Real such that
A16: ( 1o = a & 1ra = z2 ) and
A17: 1o <= 1ra by A12;
z2 <= b by A2, A14, XXREAL_1:1;
then consider 2o, 2r being Real such that
A18: ( 2o = z2 & 2r = b ) and
A19: 2o <= 2r by A4;
A20: x * 2r <= x * 2o by A3, A19, XREAL_1:65;
( x * 1o is R_eal & x * 1ra is R_eal ) by XXREAL_0:def 1;
then consider 1o1, 1r1 being R_eal such that
A21: ( 1o1 = x * 1o & 1r1 = x * 1ra ) ;
1r1 <= 1o1 by A3, A17, A21, XREAL_1:65;
hence q in [.g,d.] by A15, A16, A18, A20, A21, XXREAL_1:1; :: thesis: verum
end;
then x ** A = [.g,d.] by A5, XBOOLE_0:def 10;
hence x ** A is closed_interval by MEASURE5:def 3; :: thesis: verum
end;
hence x ** A is closed_interval ; :: thesis: verum
end;
case A22: 0 < x ; :: thesis: x ** A is closed_interval
now
per cases ( a in REAL & b in REAL ) by Th6;
case A23: ( a in REAL & b in REAL ) ; :: thesis: x ** A is closed_interval
then reconsider r = b as Real ;
reconsider s = a as Real by A23;
reconsider g = x * r as R_eal by XXREAL_0:def 1;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A24: d = x * s ;
A25: [.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 A26: q in [.d,g.] ; :: thesis: q in x ** A
then reconsider q = q as Real by A24, XREAL_0:def 1;
set q2 = q / x;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A27: q1 = q ;
A28: q = x * (q / x) by A1, XCMPLX_1:87;
q / x in A
proof
q / x is R_eal by XXREAL_0:def 1;
then consider q3 being R_eal such that
A29: q3 = q / x ;
A30: q3 <= b
proof
q1 <= g by A26, A27, XXREAL_1:1;
then consider p, o being Real such that
A31: ( p = q1 & o = g ) and
A32: p <= o by A27;
p / x <= o / x by A22, A32, XREAL_1:72;
hence q3 <= b by A22, A27, A29, A31, XCMPLX_1:89; :: thesis: verum
end;
a <= q3
proof
d <= q1 by A26, A27, XXREAL_1:1;
hence a <= q3 by A22, A24, A27, A28, A29, XREAL_1:68; :: thesis: verum
end;
hence q / x in A by A2, A29, A30, XXREAL_1:1; :: thesis: verum
end;
hence q in x ** A by A28, 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 A33: q in x ** A ; :: thesis: q in [.d,g.]
then reconsider q = q as Real ;
consider z2 being Real such that
A34: z2 in A and
A35: q = x * z2 by A33, INTEGRA2:39;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
a <= z2 by A2, A34, XXREAL_1:1;
then consider 1o, 1ra being Real such that
A36: ( 1o = a & 1ra = z2 ) and
A37: 1o <= 1ra by A23;
z2 <= b by A2, A34, XXREAL_1:1;
then consider 2o, 2r being Real such that
A38: ( 2o = z2 & 2r = b ) and
A39: 2o <= 2r by A23;
A40: x * 2o <= x * 2r by A22, A39, XREAL_1:64;
( x * 1o is R_eal & x * 1ra is R_eal ) by XXREAL_0:def 1;
then consider 1o1, 1r1 being R_eal such that
A41: ( 1o1 = x * 1o & 1r1 = x * 1ra ) ;
1o1 <= 1r1 by A22, A37, A41, XREAL_1:64;
hence q in [.d,g.] by A24, A35, A36, A38, A40, A41, XXREAL_1:1; :: thesis: verum
end;
then x ** A = [.d,g.] by A25, XBOOLE_0:def 10;
hence x ** A is closed_interval by A24, MEASURE5:def 3; :: thesis: verum
end;
end;
end;
hence x ** A is closed_interval ; :: thesis: verum
end;
end;
end;
hence x ** A is closed_interval ; :: thesis: verum