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: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

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: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

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:4;
A21: ((f . x2) - (f . a)) / (x2 - a) <= abs (((f . x2) - (f . a)) / (x2 - a)) by ABSVALUE:4;
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:47;
((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:24;
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:5;
then A27: (abs ((f . x) - (f . a))) / (abs (x - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) by COMPLEX1:67;
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:81; :: 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:5;
then A28: (abs ((f . x) - (f . a))) / (abs (x - a)) <= abs (((f . x1) - (f . a)) / (x1 - a)) by COMPLEX1:67;
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:81; :: 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:46;
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: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 ((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:5;
then A39: x <= x2 by XREAL_1:9;

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:64, 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:68;
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:74;
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:74;
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:2; :: 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: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

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:139; :: 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:46; :: 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: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 abs (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

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:2; :: 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: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 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