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
A3: ( a <= b & 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
A17: ( a in REAL & b in REAL ) by Th6;
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;
A18: x ** A = [.g,d.]
proof
A19: 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 A20: q in x ** A ; :: thesis: q in [.g,d.]
then reconsider q = q as Real ;
consider z2 being Real such that
A21: ( z2 in A & q = x * z2 ) by A20, INTEGRA2:def 2;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
A22: ( a <= z2 & z2 <= b ) by A3, A21, XXREAL_1:1;
then consider 1o, 1r being Real such that
A23: ( 1o = a & 1r = z2 & 1o <= 1r ) by A17;
consider 2o, 2r being Real such that
A24: ( 2o = z2 & 2r = b & 2o <= 2r ) by A17, A22;
A25: x * 2r <= x * 2o by A4, A24, XREAL_1:67;
( x * 1o is R_eal & x * 1r is R_eal ) by XXREAL_0:def 1;
then consider 1o1, 1r1 being R_eal such that
A26: ( 1o1 = x * 1o & 1r1 = x * 1r ) ;
1r1 <= 1o1 by A4, A23, A26, XREAL_1:67;
hence q in [.g,d.] by A21, A23, A24, A25, A26, XXREAL_1:1; :: 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 A27: q in [.g,d.] ; :: thesis: q in x ** A
then reconsider q = q as Real by XREAL_0:def 1;
reconsider q1 = q as R_eal by XXREAL_0:def 1;
A28: ( g <= q1 & q1 <= d & q1 in REAL ) by A27, XXREAL_1:1;
A29: 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
A30: q3 <= b
proof
consider p, o being Real such that
A31: ( p = g & o = q1 & p <= o ) by A28;
o / x <= p / x by A4, A31, XREAL_1:75;
hence q3 <= b by A4, A31, XCMPLX_1:90; :: thesis: verum
end;
a <= q3
proof
q1 <= d by A27, XXREAL_1:1;
then consider r, o being Real such that
A32: ( r = q1 & o = d & r <= o ) ;
x * (q / x) = q by A1, XCMPLX_1:88;
hence a <= q3 by A4, A32, XREAL_1:71; :: thesis: verum
end;
hence ( a <= q3 & q3 <= b & q3 in REAL ) by A30; :: thesis: verum
end;
hence q / x in A by A3, XXREAL_1:1; :: thesis: verum
end;
hence q in x ** A by A29, INTEGRA2:def 2; :: thesis: verum
end;
hence x ** A = [.g,d.] by A19, XBOOLE_0:def 10; :: thesis: verum
end;
x * r <= x * s by A3, A4, XREAL_1:67;
hence x ** A is closed_interval by A18, MEASURE5:def 6; :: thesis: verum
end;
hence x ** A is closed_interval ; :: thesis: verum
end;
case A44: 0 < x ; :: thesis: x ** A is closed_interval
now
per cases ( a in REAL & b in REAL ) by Th6;
case A58: ( a in REAL & b in REAL ) ; :: thesis: x ** A is closed_interval
then reconsider s = a as Real ;
reconsider r = b as Real by A58;
x * s is R_eal by XXREAL_0:def 1;
then consider d being R_eal such that
A59: d = x * s ;
reconsider g = x * r as R_eal by XXREAL_0:def 1;
A60: x ** A = [.d,g.]
proof
A61: 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 A62: q in x ** A ; :: thesis: q in [.d,g.]
then reconsider q = q as Real ;
consider z2 being Real such that
A63: ( z2 in A & q = x * z2 ) by A62, INTEGRA2:def 2;
reconsider z2 = z2 as R_eal by XXREAL_0:def 1;
A64: ( a <= z2 & z2 <= b ) by A3, A63, XXREAL_1:1;
then consider 1o, 1r being Real such that
A65: ( 1o = a & 1r = z2 & 1o <= 1r ) by A58;
consider 2o, 2r being Real such that
A66: ( 2o = z2 & 2r = b & 2o <= 2r ) by A58, A64;
A67: x * 2o <= x * 2r by A44, A66, XREAL_1:66;
( x * 1o is R_eal & x * 1r is R_eal ) by XXREAL_0:def 1;
then consider 1o1, 1r1 being R_eal such that
A68: ( 1o1 = x * 1o & 1r1 = x * 1r ) ;
1o1 <= 1r1 by A44, A65, A68, XREAL_1:66;
hence q in [.d,g.] by A59, A63, A65, A66, A67, A68, XXREAL_1:1; :: 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 A69: q in [.d,g.] ; :: thesis: q in x ** A
then reconsider q = q as Real by A59, XREAL_0:def 1;
q is R_eal by XXREAL_0:def 1;
then consider q1 being R_eal such that
A70: q1 = q ;
A71: q = x * (q / x) by A1, XCMPLX_1:88;
set q2 = q / x;
q / x in A
proof
q / x is R_eal by XXREAL_0:def 1;
then consider q3 being R_eal such that
A72: q3 = q / x ;
( a <= q3 & q3 <= b & q3 in REAL )
proof
A73: q3 <= b
proof
q1 <= g by A69, A70, XXREAL_1:1;
then consider p, o being Real such that
A74: ( p = q1 & o = g & p <= o ) by A70;
p / x <= o / x by A44, A74, XREAL_1:74;
hence q3 <= b by A44, A70, A72, A74, XCMPLX_1:90; :: thesis: verum
end;
a <= q3
proof
d <= q1 by A69, A70, XXREAL_1:1;
then consider ri, o being Real such that
A75: ( ri = d & o = q1 & ri <= o ) by A59, A70;
thus a <= q3 by A44, A59, A70, A71, A72, A75, XREAL_1:70; :: thesis: verum
end;
hence ( a <= q3 & q3 <= b & q3 in REAL ) by A72, A73; :: thesis: verum
end;
hence q / x in A by A3, A72, XXREAL_1:1; :: thesis: verum
end;
hence q in x ** A by A71, INTEGRA2:def 2; :: thesis: verum
end;
hence x ** A = [.d,g.] by A61, XBOOLE_0:def 10; :: thesis: verum
end;
x * s <= x * r by A3, A44, XREAL_1:66;
hence x ** A is closed_interval by A59, A60, 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