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 A1: ( ex x1, x2 being Real st
( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I ) ; :: thesis: f is_continuous_in a
consider x1, x2 being Real such that
A3: ( x1 in I & x2 in I & x1 < a & a < x2 ) by A1;
A4: a in I by A3, XXREAL_2:84;
A9: 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 A10: ( x1 <= x & x <= x2 & 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, 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 A10, XXREAL_0:1;

suppose 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) )

then ( ((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 A1, A3, A4, Th16, A12;
then ((f . a) - (f . x)) / (a - x) <= ((f . x2) - (f . a)) / (x2 - a) by XXREAL_0:2;
then A17: (- ((f . a) - (f . x))) / (- (a - x)) <= ((f . x2) - (f . a)) / (x2 - a) by XCMPLX_1:192;

now

per cases ( x1 = x or x1 < x ) by A10, 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 A18: x1 < x ; :: thesis: ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a)

A19: ((f . a) - (f . x)) / (a - x) = (- ((f . a) - (f . x))) / (- (a - x)) by XCMPLX_1:192
.= ((f . x) - (f . a)) / (x - a) ;
((f . a) - (f . x1)) / (a - x1) = (- ((f . a) - (f . x1))) / (- (a - x1)) by XCMPLX_1:192
.= ((f . x1) - (f . a)) / (x1 - a) ;
hence ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) by A1, A3, A4, A11, A12, A18, A19, Th16; :: 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) ) by A17; :: thesis: verum

end;

suppose A20: 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) )

A21: x in I by A12;
then A26: ( ((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 A1, A3, A4, A20, Th16;
((f . a) - (f . x1)) / (a - x1) = (- ((f . a) - (f . x1))) / (- (a - x1)) by XCMPLX_1:192
.= ((f . x1) - (f . a)) / (x1 - a) ;
hence ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) by A26, 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 A1, A3, A4, A20, A21, 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;

set M = max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)));
A27: ( abs (((f . x1) - (f . a)) / (x1 - a)) >= 0 & abs (((f . x2) - (f . a)) / (x2 - a)) >= 0 ) by COMPLEX1:132;
then A28: min (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) >= 0 by XXREAL_0:20;
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: max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) >= 0 by A28, Th1;
A31: 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

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 A32: ( x1 <= x & x <= x2 & 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;
x - a <> 0 by A32;
then A33: abs (x - a) > 0 by COMPLEX1:133;
A34: ( ((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 A9, A32;
( - (abs (((f . x1) - (f . a)) / (x1 - a))) <= ((f . x1) - (f . a)) / (x1 - a) & ((f . x2) - (f . a)) / (x2 - a) <= abs (((f . x2) - (f . a)) / (x2 - a)) ) by ABSVALUE:11;
then A35: ( - (abs (((f . x1) - (f . a)) / (x1 - a))) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= abs (((f . x2) - (f . a)) / (x2 - a)) ) by A34, 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 A35, XXREAL_0:2;
then abs (((f . x) - (f . a)) / (x - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) by A35, ABSVALUE:12;
then A36: (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 A36, 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 A33, 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 A35, XXREAL_0:2;
then abs (((f . x) - (f . a)) / (x - a)) <= abs (((f . x1) - (f . a)) / (x1 - a)) by A35, ABSVALUE:12;
then A37: (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 A37, 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 A33, 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;

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 A38: 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 A27, A29, XXREAL_0:20;

suppose A39: 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));
A40: min (r / (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))),(min (a - x1),(x2 - a)) > 0

proof

A41: 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 A3, 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 A3, 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 A38, A39, 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 A41; :: 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;

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

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 A42: ( 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)) ) ; :: thesis: abs ((f . x) - (f . a)) < r
A43: ( 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)))) & 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;
( min (a - x1),(x2 - a) <= a - x1 & 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)) <= a - x1 & 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 A43, XXREAL_0:2;
then ( abs (x - a) < a - x1 & abs (x - a) < x2 - a ) by A42, XXREAL_0:2;
then ( - (a - x1) <= x - a & x - a <= x2 - a ) by ABSVALUE:12;
then ( x1 - a <= x - a & x - a <= x2 - a ) ;
then A44: ( x1 <= x & 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 A45: abs ((f . x) - (f . a)) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) by A31, A44;

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 A46: max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))) <> 0 ; :: thesis: abs ((f . x) - (f . a)) < r

then A47: (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 A30, A42, XREAL_1:70;
(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 A28, A29, XREAL_1:66, XXREAL_0:17;
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 A47, 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 A46, XCMPLX_1:60;
hence abs ((f . x) - (f . a)) < r by A45, 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 A38, A45; :: 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 A38, ABSVALUE:7; :: thesis: verum

end;

end;

end;

hence 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 ) ) by A40; :: thesis: verum

end;

suppose A48: 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 ) )

A49: 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 A50: ( x1 <= x & x <= x2 & x <> a ) ; :: thesis: abs ((f . x) - (f . a)) = 0
abs ((f . x) - (f . a)) <= (max (abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) * (abs (x - a)) by A31, A50;
hence abs ((f . x) - (f . a)) = 0 by A48, COMPLEX1:132; :: thesis: verum

end;

set s = min (a - x1),(x2 - a);
A51: 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 A3, 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 A3, XREAL_1:52; :: thesis: verum

end;

end;

end;

hence min (a - x1),(x2 - a) > 0 ; :: thesis: verum

end;

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 A52: ( x in dom f & abs (x - a) < min (a - x1),(x2 - a) ) ; :: thesis: abs ((f . x) - (f . a)) < r
( min (a - x1),(x2 - a) <= a - x1 & min (a - x1),(x2 - a) <= x2 - a ) by XXREAL_0:17;
then ( abs (x - a) < a - x1 & abs (x - a) < x2 - a ) by A52, XXREAL_0:2;
then ( - (a - x1) <= x - a & x - a <= x2 - a ) by ABSVALUE:12;
then ( x1 - a <= x - a & x - a <= x2 - a ) ;
then A53: ( x1 <= x & 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 A38, A49, A53; :: thesis: verum

end;

suppose x = a ; :: thesis: abs ((f . x) - (f . a)) < r

hence abs ((f . x) - (f . a)) < r by A38, ABSVALUE:7; :: thesis: verum

end;

end;

end;

hence 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 ) ) by A51; :: 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