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