let f be PartFunc of REAL,REAL; :: thesis: for I being Interval
for a being Real st ex x1, x2 being Real st
( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I holds
f is_continuous_in a
let I be Interval; :: thesis: for a being Real st ex x1, x2 being Real st
( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I holds
f is_continuous_in a
let a be Real; :: thesis: ( ex x1, x2 being Real st
( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I implies f is_continuous_in a )
assume that
A1: ex x1, x2 being Real st
( x1 in I & x2 in I & x1 < a & a < x2 ) and
A2: f is_convex_on I ; :: thesis: f is_continuous_in a
consider x1, x2 being Real such that
A3: x1 in I and
A4: x2 in I and
A5: x1 < a and
A6: a < x2 by A1;
set M = max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|);
A7: a in I by A3, A4, A5, A6, XXREAL_2:80;
A8: for x being Real st x1 <= x & x <= x2 & x <> a holds
( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) )
proof
let x be Real; :: thesis: ( x1 <= x & x <= x2 & x <> a implies ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) )
assume that
A9: x1 <= x and
A10: x <= x2 and
A11: x <> a ; :: thesis: ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) )
A12: x in I by A3, A4, A9, A10, XXREAL_2:80;
( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) )
proof
now :: thesis: ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) )
per cases ( x < a or x > a ) by A11, XXREAL_0:1;
suppose A13: x < a ; :: thesis: ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) )
A14: now :: thesis: ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a)
per cases ( x1 = x or x1 < x ) by A9, XXREAL_0:1;
suppose x1 = x ; :: thesis: ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a)
hence ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) ; :: thesis: verum
end;
suppose A15: x1 < x ; :: thesis: ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a)
A16: ((f . a) - (f . x1)) / (a - x1) = (- ((f . a) - (f . x1))) / (- (a - x1)) by XCMPLX_1:191
.= ((f . x1) - (f . a)) / (x1 - a) ;
((f . a) - (f . x)) / (a - x) = (- ((f . a) - (f . x))) / (- (a - x)) by XCMPLX_1:191
.= ((f . x) - (f . a)) / (x - a) ;
hence ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) by A2, A3, A7, A12, A13, A15, A16, Th16; :: thesis: verum
end;
end;
end;
( ((f . a) - (f . x)) / (a - x) <= ((f . x2) - (f . x)) / (x2 - x) & ((f . x2) - (f . x)) / (x2 - x) <= ((f . x2) - (f . a)) / (x2 - a) ) by A2, A4, A6, A7, A12, A13, Th16;
then ((f . a) - (f . x)) / (a - x) <= ((f . x2) - (f . a)) / (x2 - a) by XXREAL_0:2;
then (- ((f . a) - (f . x))) / (- (a - x)) <= ((f . x2) - (f . a)) / (x2 - a) by XCMPLX_1:191;
hence ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) by A14; :: thesis: verum
end;
suppose A17: x > a ; :: thesis: ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) )
A18: ((f . a) - (f . x1)) / (a - x1) = (- ((f . a) - (f . x1))) / (- (a - x1)) by XCMPLX_1:191
.= ((f . x1) - (f . a)) / (x1 - a) ;
( ((f . a) - (f . x1)) / (a - x1) <= ((f . x) - (f . x1)) / (x - x1) & ((f . x) - (f . x1)) / (x - x1) <= ((f . x) - (f . a)) / (x - a) ) by A2, A3, A5, A7, A12, A17, Th16;
hence ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) by A18, XXREAL_0:2; :: thesis: ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a)
now :: thesis: ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a)
per cases ( x = x2 or x < x2 ) by A10, XXREAL_0:1;
suppose x = x2 ; :: thesis: ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a)
hence ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ; :: thesis: verum
end;
suppose x < x2 ; :: thesis: ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a)
hence ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) by A2, A4, A7, A12, A17, Th16; :: thesis: verum
end;
end;
end;
hence ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ; :: thesis: verum
end;
end;
end;
hence ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) ; :: thesis: verum
end;
hence ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) ; :: thesis: verum
end;
A19: for x being Real st x1 <= x & x <= x2 & x <> a holds
|.((f . x) - (f . a)).| <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).|
proof
A20: - |.(((f . x1) - (f . a)) / (x1 - a)).| <= ((f . x1) - (f . a)) / (x1 - a) by ABSVALUE:4;
A21: ((f . x2) - (f . a)) / (x2 - a) <= |.(((f . x2) - (f . a)) / (x2 - a)).| by ABSVALUE:4;
let x be Real; :: thesis: ( x1 <= x & x <= x2 & x <> a implies |.((f . x) - (f . a)).| <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).| )
assume that
A22: ( x1 <= x & x <= x2 ) and
A23: x <> a ; :: thesis: |.((f . x) - (f . a)).| <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).|
reconsider x = x as Real ;
((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) by A8, A22, A23;
then A24: ((f . x) - (f . a)) / (x - a) <= |.(((f . x2) - (f . a)) / (x2 - a)).| by A21, XXREAL_0:2;
x - a <> 0 by A23;
then A25: |.(x - a).| > 0 by COMPLEX1:47;
((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) by A8, A22, A23;
then A26: - |.(((f . x1) - (f . a)) / (x1 - a)).| <= ((f . x) - (f . a)) / (x - a) by A20, XXREAL_0:2;
now :: thesis: |.((f . x) - (f . a)).| <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).|
per cases ( |.(((f . x1) - (f . a)) / (x1 - a)).| <= |.(((f . x2) - (f . a)) / (x2 - a)).| or |.(((f . x1) - (f . a)) / (x1 - a)).| >= |.(((f . x2) - (f . a)) / (x2 - a)).| ) ;
suppose |.(((f . x1) - (f . a)) / (x1 - a)).| <= |.(((f . x2) - (f . a)) / (x2 - a)).| ; :: thesis: |.((f . x) - (f . a)).| <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).|
then - |.(((f . x1) - (f . a)) / (x1 - a)).| >= - |.(((f . x2) - (f . a)) / (x2 - a)).| by XREAL_1:24;
then - |.(((f . x2) - (f . a)) / (x2 - a)).| <= ((f . x) - (f . a)) / (x - a) by A26, XXREAL_0:2;
then |.(((f . x) - (f . a)) / (x - a)).| <= |.(((f . x2) - (f . a)) / (x2 - a)).| by A24, ABSVALUE:5;
then A27: |.((f . x) - (f . a)).| / |.(x - a).| <= |.(((f . x2) - (f . a)) / (x2 - a)).| by COMPLEX1:67;
|.(((f . x2) - (f . a)) / (x2 - a)).| <= max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) by XXREAL_0:25;
then |.((f . x) - (f . a)).| / |.(x - a).| <= max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) by A27, XXREAL_0:2;
hence |.((f . x) - (f . a)).| <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).| by A25, XREAL_1:81; :: thesis: verum
end;
suppose |.(((f . x1) - (f . a)) / (x1 - a)).| >= |.(((f . x2) - (f . a)) / (x2 - a)).| ; :: thesis: |.((f . x) - (f . a)).| <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).|
then ((f . x) - (f . a)) / (x - a) <= |.(((f . x1) - (f . a)) / (x1 - a)).| by A24, XXREAL_0:2;
then |.(((f . x) - (f . a)) / (x - a)).| <= |.(((f . x1) - (f . a)) / (x1 - a)).| by A26, ABSVALUE:5;
then A28: |.((f . x) - (f . a)).| / |.(x - a).| <= |.(((f . x1) - (f . a)) / (x1 - a)).| by COMPLEX1:67;
|.(((f . x1) - (f . a)) / (x1 - a)).| <= max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) by XXREAL_0:25;
then |.((f . x) - (f . a)).| / |.(x - a).| <= max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) by A28, XXREAL_0:2;
hence |.((f . x) - (f . a)).| <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).| by A25, XREAL_1:81; :: thesis: verum
end;
end;
end;
hence |.((f . x) - (f . a)).| <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).| ; :: thesis: verum
end;
A29: max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) >= min (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) by Th1;
A30: ( |.(((f . x1) - (f . a)) / (x1 - a)).| >= 0 & |.(((f . x2) - (f . a)) / (x2 - a)).| >= 0 ) by COMPLEX1:46;
then A31: min (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) >= 0 by XXREAL_0:20;
then A32: max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) >= 0 by Th1;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(x - a).| < s holds
|.((f . x) - (f . a)).| < r ) )
proof
let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(x - a).| < s holds
|.((f . x) - (f . a)).| < r ) ) )
assume A33: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(x - a).| < s holds
|.((f . x) - (f . a)).| < r ) )
reconsider r = r as Real ;
ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(x - a).| < s holds
|.((f . x) - (f . a)).| < r ) )
proof
now :: thesis: ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(x - a).| < s holds
|.((f . x) - (f . a)).| < r ) )
per cases ( max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) > 0 or max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) = 0 ) by A30, A29, XXREAL_0:20;
suppose A34: max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) > 0 ; :: thesis: ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(x - a).| < s holds
|.((f . x) - (f . a)).| < r ) )
set s = min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a))));
A35: for x being Real st x in dom f & |.(x - a).| < min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) holds
|.((f . x) - (f . a)).| < r
proof
A36: min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) <= min ((a - x1),(x2 - a)) by XXREAL_0:17;
let x be Real; :: thesis: ( x in dom f & |.(x - a).| < min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) implies |.((f . x) - (f . a)).| < r )
assume that
x in dom f and
A37: |.(x - a).| < min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) ; :: thesis: |.((f . x) - (f . a)).| < r
min ((a - x1),(x2 - a)) <= a - x1 by XXREAL_0:17;
then min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) <= a - x1 by A36, XXREAL_0:2;
then |.(x - a).| < a - x1 by A37, XXREAL_0:2;
then - (a - x1) <= x - a by ABSVALUE:5;
then x1 - a <= x - a ;
then A38: x1 <= x by XREAL_1:9;
min ((a - x1),(x2 - a)) <= x2 - a by XXREAL_0:17;
then min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) <= x2 - a by A36, XXREAL_0:2;
then |.(x - a).| < x2 - a by A37, XXREAL_0:2;
then x - a <= x2 - a by ABSVALUE:5;
then A39: x <= x2 by XREAL_1:9;
now :: thesis: |.((f . x) - (f . a)).| < r
per cases ( x <> a or x = a ) ;
suppose x <> a ; :: thesis: |.((f . x) - (f . a)).| < r
then A40: |.((f . x) - (f . a)).| <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).| by A19, A38, A39;
now :: thesis: |.((f . x) - (f . a)).| < r
per cases ( max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) <> 0 or max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) = 0 ) ;
suppose A41: max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) <> 0 ; :: thesis: |.((f . x) - (f . a)).| < r
A42: (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * (min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a))))) <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * (r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))) by A31, A29, XREAL_1:64, XXREAL_0:17;
(max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).| < (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * (min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a))))) by A32, A37, A41, XREAL_1:68;
then (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).| < (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * (r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))) by A42, XXREAL_0:2;
then (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).| < (r * (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))) / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) by XCMPLX_1:74;
then (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).| < r * ((max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))) by XCMPLX_1:74;
then (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).| < r * 1 by A41, XCMPLX_1:60;
hence |.((f . x) - (f . a)).| < r by A40, XXREAL_0:2; :: thesis: verum
end;
suppose max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) = 0 ; :: thesis: |.((f . x) - (f . a)).| < r
hence |.((f . x) - (f . a)).| < r by A33, A40; :: thesis: verum
end;
end;
end;
hence |.((f . x) - (f . a)).| < r ; :: thesis: verum
end;
suppose x = a ; :: thesis: |.((f . x) - (f . a)).| < r
hence |.((f . x) - (f . a)).| < r by A33, ABSVALUE:2; :: thesis: verum
end;
end;
end;
hence |.((f . x) - (f . a)).| < r ; :: thesis: verum
end;
min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) > 0
proof
A43: min ((a - x1),(x2 - a)) > 0
proof
now :: thesis: min ((a - x1),(x2 - a)) > 0
per cases ( min ((a - x1),(x2 - a)) = a - x1 or min ((a - x1),(x2 - a)) = x2 - a ) by XXREAL_0:15;
suppose min ((a - x1),(x2 - a)) = a - x1 ; :: thesis: min ((a - x1),(x2 - a)) > 0
hence min ((a - x1),(x2 - a)) > 0 by A5, XREAL_1:50; :: thesis: verum
end;
suppose min ((a - x1),(x2 - a)) = x2 - a ; :: thesis: min ((a - x1),(x2 - a)) > 0
hence min ((a - x1),(x2 - a)) > 0 by A6, XREAL_1:50; :: thesis: verum
end;
end;
end;
hence min ((a - x1),(x2 - a)) > 0 ; :: thesis: verum
end;
now :: thesis: min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) > 0
per cases ( min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) = r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) or min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) = min ((a - x1),(x2 - a)) ) by XXREAL_0:15;
suppose min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) = r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) ; :: thesis: min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) > 0
hence min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) > 0 by A33, A34, XREAL_1:139; :: thesis: verum
end;
suppose min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) = min ((a - x1),(x2 - a)) ; :: thesis: min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) > 0
hence min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) > 0 by A43; :: thesis: verum
end;
end;
end;
hence min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) > 0 ; :: thesis: verum
end;
hence ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(x - a).| < s holds
|.((f . x) - (f . a)).| < r ) ) by A35; :: thesis: verum
end;
suppose A44: max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) = 0 ; :: thesis: ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(x - a).| < s holds
|.((f . x) - (f . a)).| < r ) )
set s = min ((a - x1),(x2 - a));
A45: for x being Real st x1 <= x & x <= x2 & x <> a holds
|.((f . x) - (f . a)).| = 0
proof
let x be Real; :: thesis: ( x1 <= x & x <= x2 & x <> a implies |.((f . x) - (f . a)).| = 0 )
assume ( x1 <= x & x <= x2 & x <> a ) ; :: thesis: |.((f . x) - (f . a)).| = 0
then |.((f . x) - (f . a)).| <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).| by A19;
hence |.((f . x) - (f . a)).| = 0 by A44, COMPLEX1:46; :: thesis: verum
end;
A46: for x being Real st x in dom f & |.(x - a).| < min ((a - x1),(x2 - a)) holds
|.((f . x) - (f . a)).| < r
proof
let x be Real; :: thesis: ( x in dom f & |.(x - a).| < min ((a - x1),(x2 - a)) implies |.((f . x) - (f . a)).| < r )
assume that
x in dom f and
A47: |.(x - a).| < min ((a - x1),(x2 - a)) ; :: thesis: |.((f . x) - (f . a)).| < r
min ((a - x1),(x2 - a)) <= a - x1 by XXREAL_0:17;
then |.(x - a).| < a - x1 by A47, XXREAL_0:2;
then - (a - x1) <= x - a by ABSVALUE:5;
then x1 - a <= x - a ;
then A48: x1 <= x by XREAL_1:9;
min ((a - x1),(x2 - a)) <= x2 - a by XXREAL_0:17;
then |.(x - a).| < x2 - a by A47, XXREAL_0:2;
then x - a <= x2 - a by ABSVALUE:5;
then A49: x <= x2 by XREAL_1:9;
now :: thesis: |.((f . x) - (f . a)).| < r
per cases ( x <> a or x = a ) ;
suppose x <> a ; :: thesis: |.((f . x) - (f . a)).| < r
hence |.((f . x) - (f . a)).| < r by A33, A45, A48, A49; :: thesis: verum
end;
suppose x = a ; :: thesis: |.((f . x) - (f . a)).| < r
hence |.((f . x) - (f . a)).| < r by A33, ABSVALUE:2; :: thesis: verum
end;
end;
end;
hence |.((f . x) - (f . a)).| < r ; :: thesis: verum
end;
min ((a - x1),(x2 - a)) > 0
proof
now :: thesis: min ((a - x1),(x2 - a)) > 0
per cases ( min ((a - x1),(x2 - a)) = a - x1 or min ((a - x1),(x2 - a)) = x2 - a ) by XXREAL_0:15;
suppose min ((a - x1),(x2 - a)) = a - x1 ; :: thesis: min ((a - x1),(x2 - a)) > 0
hence min ((a - x1),(x2 - a)) > 0 by A5, XREAL_1:50; :: thesis: verum
end;
suppose min ((a - x1),(x2 - a)) = x2 - a ; :: thesis: min ((a - x1),(x2 - a)) > 0
hence min ((a - x1),(x2 - a)) > 0 by A6, XREAL_1:50; :: thesis: verum
end;
end;
end;
hence min ((a - x1),(x2 - a)) > 0 ; :: thesis: verum
end;
hence ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(x - a).| < s holds
|.((f . x) - (f . a)).| < r ) ) by A46; :: thesis: verum
end;
end;
end;
hence ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(x - a).| < s holds
|.((f . x) - (f . a)).| < r ) ) ; :: thesis: verum
end;
hence ex s being Real st
( 0 < s & ( for x being Real st x in dom f & |.(x - a).| < s holds
|.((f . x) - (f . a)).| < r ) ) ; :: thesis: verum
end;
hence f is_continuous_in a by FCONT_1:3; :: thesis: verum