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 (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)));
A7: a in I by A3, A4, A5, A6, XXREAL_2:84;
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:84;
( ((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
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
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:192
.= ((f . x1) - (f . a)) / (x1 - a) ;
((f . a) - (f . x)) / (a - x) = (- ((f . a) - (f . x))) / (- (a - x)) by XCMPLX_1:192
.= ((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:192;
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:192
.= ((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
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 number st x1 <= x & x <= x2 & x <> a holds
abs ((f . x) - (f . a)) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a))
proof
A20: - (abs (((f . x1) - (f . a)) / (x1 - a))) <= ((f . x1) - (f . a)) / (x1 - a) by ABSVALUE:11;
A21: ((f . x2) - (f . a)) / (x2 - a) <= abs (((f . x2) - (f . a)) / (x2 - a)) by ABSVALUE:11;
let x be real number ; :: thesis: ( x1 <= x & x <= x2 & x <> a implies abs ((f . x) - (f . a)) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) )
assume that
A22: ( x1 <= x & x <= x2 ) and
A23: x <> a ; :: thesis: abs ((f . x) - (f . a)) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a))
reconsider x = x as Real by XREAL_0:def 1;
((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) by A8, A22, A23;
then A24: ((f . x) - (f . a)) / (x - a) <= abs (((f . x2) - (f . a)) / (x2 - a)) by A21, XXREAL_0:2;
x - a <> 0 by A23;
then A25: abs (x - a) > 0 by COMPLEX1:133;
((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) by A8, A22, A23;
then A26: - (abs (((f . x1) - (f . a)) / (x1 - a))) <= ((f . x) - (f . a)) / (x - a) by A20, XXREAL_0:2;
now
per cases ( abs (((f . x1) - (f . a)) / (x1 - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) or abs (((f . x1) - (f . a)) / (x1 - a)) >= abs (((f . x2) - (f . a)) / (x2 - a)) ) ;
suppose abs (((f . x1) - (f . a)) / (x1 - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) ; :: thesis: abs ((f . x) - (f . a)) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a))
then - (abs (((f . x1) - (f . a)) / (x1 - a))) >= - (abs (((f . x2) - (f . a)) / (x2 - a))) by XREAL_1:26;
then - (abs (((f . x2) - (f . a)) / (x2 - a))) <= ((f . x) - (f . a)) / (x - a) by A26, XXREAL_0:2;
then abs (((f . x) - (f . a)) / (x - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) by A24, ABSVALUE:12;
then A27: (abs ((f . x) - (f . a))) / (abs (x - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) by COMPLEX1:153;
abs (((f . x2) - (f . a)) / (x2 - a)) <= max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) by XXREAL_0:25;
then (abs ((f . x) - (f . a))) / (abs (x - a)) <= max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) by A27, XXREAL_0:2;
hence abs ((f . x) - (f . a)) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) by A25, XREAL_1:83; :: thesis: verum
end;
suppose abs (((f . x1) - (f . a)) / (x1 - a)) >= abs (((f . x2) - (f . a)) / (x2 - a)) ; :: thesis: abs ((f . x) - (f . a)) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a))
then ((f . x) - (f . a)) / (x - a) <= abs (((f . x1) - (f . a)) / (x1 - a)) by A24, XXREAL_0:2;
then abs (((f . x) - (f . a)) / (x - a)) <= abs (((f . x1) - (f . a)) / (x1 - a)) by A26, ABSVALUE:12;
then A28: (abs ((f . x) - (f . a))) / (abs (x - a)) <= abs (((f . x1) - (f . a)) / (x1 - a)) by COMPLEX1:153;
abs (((f . x1) - (f . a)) / (x1 - a)) <= max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) by XXREAL_0:25;
then (abs ((f . x) - (f . a))) / (abs (x - a)) <= max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) by A28, XXREAL_0:2;
hence abs ((f . x) - (f . a)) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) by A25, XREAL_1:83; :: thesis: verum
end;
end;
end;
hence abs ((f . x) - (f . a)) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) ; :: thesis: verum
end;
A29: max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) >= min (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) by Th1;
A30: ( abs (((f . x1) - (f . a)) / (x1 - a)) >= 0 & abs (((f . x2) - (f . a)) / (x2 - a)) >= 0 ) by COMPLEX1:132;
then A31: min (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) >= 0 by XXREAL_0:20;
then A32: max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) >= 0 by Th1;
for r being real number st 0 < r holds
ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) )
proof
let r be real number ; :: thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) ) )
assume A33: 0 < r ; :: thesis: ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) )
reconsider r = r as Real by XREAL_0:def 1;
ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) )
proof
now
per cases ( max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) > 0 or max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) = 0 ) by A30, A29, XXREAL_0:20;
suppose A34: max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) > 0 ; :: thesis: ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) )
set s = min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a));
A35: for x being real number st x in dom f & abs (x - a) < min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) holds
abs ((f . x) - (f . a)) < r
proof
A36: min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) <= min (a - x1),(x2 - a) by XXREAL_0:17;
let x be real number ; :: thesis: ( x in dom f & abs (x - a) < min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) implies abs ((f . x) - (f . a)) < r )
assume that
x in dom f and
A37: abs (x - a) < min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) ; :: thesis: abs ((f . x) - (f . a)) < r
min (a - x1),(x2 - a) <= a - x1 by XXREAL_0:17;
then min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) <= a - x1 by A36, XXREAL_0:2;
then abs (x - a) < a - x1 by A37, XXREAL_0:2;
then - (a - x1) <= x - a by ABSVALUE:12;
then x1 - a <= x - a ;
then A38: x1 <= x by XREAL_1:11;
min (a - x1),(x2 - a) <= x2 - a by XXREAL_0:17;
then min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) <= x2 - a by A36, XXREAL_0:2;
then abs (x - a) < x2 - a by A37, XXREAL_0:2;
then x - a <= x2 - a by ABSVALUE:12;
then A39: x <= x2 by XREAL_1:11;
now
per cases ( x <> a or x = a ) ;
suppose x <> a ; :: thesis: abs ((f . x) - (f . a)) < r
then A40: abs ((f . x) - (f . a)) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) by A19, A38, A39;
now
per cases ( max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) <> 0 or max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) = 0 ) ;
suppose A41: max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) <> 0 ; :: thesis: abs ((f . x) - (f . a)) < r
A42: (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a))) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) by A31, A29, XREAL_1:66, XXREAL_0:17;
(max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) < (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a))) by A32, A37, A41, XREAL_1:70;
then (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) < (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) by A42, XXREAL_0:2;
then (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) < (r * (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) by XCMPLX_1:75;
then (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) < r * ((max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) by XCMPLX_1:75;
then (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) < r * 1 by A41, XCMPLX_1:60;
hence abs ((f . x) - (f . a)) < r by A40, XXREAL_0:2; :: thesis: verum
end;
suppose max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) = 0 ; :: thesis: abs ((f . x) - (f . a)) < r
hence abs ((f . x) - (f . a)) < r by A33, A40; :: thesis: verum
end;
end;
end;
hence abs ((f . x) - (f . a)) < r ; :: thesis: verum
end;
suppose x = a ; :: thesis: abs ((f . x) - (f . a)) < r
hence abs ((f . x) - (f . a)) < r by A33, ABSVALUE:7; :: thesis: verum
end;
end;
end;
hence abs ((f . x) - (f . a)) < r ; :: thesis: verum
end;
min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) > 0
proof
A43: min (a - x1),(x2 - a) > 0
proof
now
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:52; :: 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:52; :: thesis: verum
end;
end;
end;
hence min (a - x1),(x2 - a) > 0 ; :: thesis: verum
end;
now
per cases ( min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) = r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) or min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) = min (a - x1),(x2 - a) ) by XXREAL_0:15;
suppose min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) = r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) ; :: thesis: min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) > 0
hence min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) > 0 by A33, A34, XREAL_1:141; :: thesis: verum
end;
suppose min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) = min (a - x1),(x2 - a) ; :: thesis: min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) > 0
hence min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) > 0 by A43; :: thesis: verum
end;
end;
end;
hence min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) > 0 ; :: thesis: verum
end;
hence ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) ) by A35; :: thesis: verum
end;
suppose A44: max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) = 0 ; :: thesis: ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) )
set s = min (a - x1),(x2 - a);
A45: for x being real number st x1 <= x & x <= x2 & x <> a holds
abs ((f . x) - (f . a)) = 0
proof
let x be real number ; :: thesis: ( x1 <= x & x <= x2 & x <> a implies abs ((f . x) - (f . a)) = 0 )
assume ( x1 <= x & x <= x2 & x <> a ) ; :: thesis: abs ((f . x) - (f . a)) = 0
then abs ((f . x) - (f . a)) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) by A19;
hence abs ((f . x) - (f . a)) = 0 by A44, COMPLEX1:132; :: thesis: verum
end;
A46: for x being real number st x in dom f & abs (x - a) < min (a - x1),(x2 - a) holds
abs ((f . x) - (f . a)) < r
proof
let x be real number ; :: thesis: ( x in dom f & abs (x - a) < min (a - x1),(x2 - a) implies abs ((f . x) - (f . a)) < r )
assume that
x in dom f and
A47: abs (x - a) < min (a - x1),(x2 - a) ; :: thesis: abs ((f . x) - (f . a)) < r
min (a - x1),(x2 - a) <= a - x1 by XXREAL_0:17;
then abs (x - a) < a - x1 by A47, XXREAL_0:2;
then - (a - x1) <= x - a by ABSVALUE:12;
then x1 - a <= x - a ;
then A48: x1 <= x by XREAL_1:11;
min (a - x1),(x2 - a) <= x2 - a by XXREAL_0:17;
then abs (x - a) < x2 - a by A47, XXREAL_0:2;
then x - a <= x2 - a by ABSVALUE:12;
then A49: x <= x2 by XREAL_1:11;
now
per cases ( x <> a or x = a ) ;
suppose x <> a ; :: thesis: abs ((f . x) - (f . a)) < r
hence abs ((f . x) - (f . a)) < r by A33, A45, A48, A49; :: thesis: verum
end;
suppose x = a ; :: thesis: abs ((f . x) - (f . a)) < r
hence abs ((f . x) - (f . a)) < r by A33, ABSVALUE:7; :: thesis: verum
end;
end;
end;
hence abs ((f . x) - (f . a)) < r ; :: thesis: verum
end;
min (a - x1),(x2 - a) > 0
proof
now
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:52; :: 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:52; :: thesis: verum
end;
end;
end;
hence min (a - x1),(x2 - a) > 0 ; :: thesis: verum
end;
hence ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) ) by A46; :: thesis: verum
end;
end;
end;
hence ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) ) ; :: thesis: verum
end;
hence ex s being real number st
( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds
abs ((f . x) - (f . a)) < r ) ) ; :: thesis: verum
end;
hence f is_continuous_in a by FCONT_1:3; :: thesis: verum