let A be 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 <= b and
A3: A = [.a,b.] by MEASURE5:def 6;
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 A4: 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;
A5: b in REAL by Th6;
A6: x * r <= x * s by A2, A4, XREAL_1:67;
A7: [.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 A8: 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;
A9: g <= q1 by A8, XXREAL_1:1;
A10: q / x in A
proof
reconsider q3 = q / x as R_eal by XXREAL_0:def 1;
A11: q3 <= b
proof
consider p, o being Real such that
A12: ( p = g & o = q1 ) and
A13: p <= o by A9;
o / x <= p / x by A4, A13, XREAL_1:75;
hence q3 <= b by A4, A12, XCMPLX_1:90; :: thesis: verum
end;
a <= q3
proof
( q1 <= d & x * (q / x) = q ) by A1, A8, XCMPLX_1:88, XXREAL_1:1;
hence a <= q3 by A4, XREAL_1:71; :: thesis: verum
end;
hence q / x in A by A3, A11, XXREAL_1:1; :: thesis: verum
end;
q = x * (q / x) by A1, XCMPLX_1:88;
hence q in x ** A by A10, INTEGRA2:def 2; :: thesis: verum
end;
A14: 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 A15: q in x ** A ; :: thesis: q in [.g,d.]
then reconsider q = q as Real ;
consider z2 being Real such that
A16: z2 in A and
A17: q = x * z2 by A15, INTEGRA2:def 2;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
a <= z2 by A3, A16, XXREAL_1:1;
then consider 1o, 1ra being Real such that
A18: ( 1o = a & 1ra = z2 ) and
A19: 1o <= 1ra by A14;
z2 <= b by A3, A16, XXREAL_1:1;
then consider 2o, 2r being Real such that
A20: ( 2o = z2 & 2r = b ) and
A21: 2o <= 2r by A5;
A22: x * 2r <= x * 2o by A4, A21, XREAL_1:67;
( x * 1o is R_eal & x * 1ra is R_eal ) by XXREAL_0:def 1;
then consider 1o1, 1r1 being R_eal such that
A23: ( 1o1 = x * 1o & 1r1 = x * 1ra ) ;
1r1 <= 1o1 by A4, A19, A23, XREAL_1:67;
hence q in [.g,d.] by A17, A18, A20, A22, A23, XXREAL_1:1; :: thesis: verum
end;
then x ** A = [.g,d.] by A7, XBOOLE_0:def 10;
hence x ** A is closed_interval by A6, MEASURE5:def 6; :: thesis: verum
end;
hence x ** A is closed_interval ; :: thesis: verum
end;
case A24: 0 < x ; :: thesis: x ** A is closed_interval
now
per cases ( a in REAL & b in REAL ) by Th6;
case A25: ( a in REAL & b in REAL ) ; :: thesis: x ** A is closed_interval
then reconsider r = b as Real ;
reconsider s = a as Real by A25;
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
A26: d = x * s ;
A27: [.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 A28: q in [.d,g.] ; :: thesis: q in x ** A
then reconsider q = q as Real by A26, 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
A29: q1 = q ;
A30: q = x * (q / x) by A1, XCMPLX_1:88;
q / x in A
proof
q / x is R_eal by XXREAL_0:def 1;
then consider q3 being R_eal such that
A31: q3 = q / x ;
A32: q3 <= b
proof
q1 <= g by A28, A29, XXREAL_1:1;
then consider p, o being Real such that
A33: ( p = q1 & o = g ) and
A34: p <= o by A29;
p / x <= o / x by A24, A34, XREAL_1:74;
hence q3 <= b by A24, A29, A31, A33, XCMPLX_1:90; :: thesis: verum
end;
a <= q3
proof
d <= q1 by A28, A29, XXREAL_1:1;
hence a <= q3 by A24, A26, A29, A30, A31, XREAL_1:70; :: thesis: verum
end;
hence q / x in A by A3, A31, A32, XXREAL_1:1; :: thesis: verum
end;
hence q in x ** A by A30, INTEGRA2:def 2; :: thesis: verum
end;
A35: x * s <= x * r by A2, A24, XREAL_1:66;
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 A36: q in x ** A ; :: thesis: q in [.d,g.]
then reconsider q = q as Real ;
consider z2 being Real such that
A37: z2 in A and
A38: q = x * z2 by A36, INTEGRA2:def 2;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
a <= z2 by A3, A37, XXREAL_1:1;
then consider 1o, 1ra being Real such that
A39: ( 1o = a & 1ra = z2 ) and
A40: 1o <= 1ra by A25;
z2 <= b by A3, A37, XXREAL_1:1;
then consider 2o, 2r being Real such that
A41: ( 2o = z2 & 2r = b ) and
A42: 2o <= 2r by A25;
A43: x * 2o <= x * 2r by A24, A42, XREAL_1:66;
( x * 1o is R_eal & x * 1ra is R_eal ) by XXREAL_0:def 1;
then consider 1o1, 1r1 being R_eal such that
A44: ( 1o1 = x * 1o & 1r1 = x * 1ra ) ;
1o1 <= 1r1 by A24, A40, A44, XREAL_1:66;
hence q in [.d,g.] by A26, A38, A39, A41, A43, A44, XXREAL_1:1; :: thesis: verum
end;
then x ** A = [.d,g.] by A27, XBOOLE_0:def 10;
hence x ** A is closed_interval by A26, A35, MEASURE5:def 6; :: thesis: verum
end;
end;
end;
hence x ** A is closed_interval ; :: thesis: verum
end;
end;
end;
hence x ** A is closed_interval ; :: thesis: verum