let f be PartFunc of REAL,REAL; :: thesis:
let I be Interval; :: thesis:
let a be Real; :: thesis:
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:
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) )

let x be Real; :: thesis:
assume that
A9: x1 <= x and
A10: x <= x2 and
A11: x <> a ; :: thesis:
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) )

now :: thesis:

per cases by A11, XXREAL_0:1;

suppose A13: x < a ; :: thesis:

A14: now :: thesis:

per cases by A9, XXREAL_0:1;

suppose x1 = x ; :: thesis:

hence ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) ; :: thesis:

end;

suppose A15: x1 < x ; :: thesis:

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:

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:

end;

suppose A17: x > a ; :: thesis:

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:

now :: thesis:

per cases by A10, XXREAL_0:1;

suppose x = x2 ; :: thesis:

hence ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ; :: thesis:

end;

suppose x < x2 ; :: thesis:

hence ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) by A2, A4, A7, A12, A17, Th16; :: thesis:

end;

hence ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ; :: thesis:

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:

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:

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:
assume that
A22: ( x1 <= x & x <= x2 ) and
A23: x <> a ; :: thesis:
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:

per cases <= |.(((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:

end;

suppose |.(((f . x1) - (f . a)) / (x1 - a)).| >= |.(((f . x2) - (f . a)) / (x2 - a)).| ; :: thesis:

end;

hence |.((f . x) - (f . a)).| <= (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|)) * |.(x - a).| ; :: thesis:

end;

proof

let r be Real; :: thesis:
assume A33: 0 < r ; :: thesis:
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:

per cases by A30, A29, XXREAL_0:20;

suppose A34: max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) > 0 ; :: thesis:

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

per cases ;

suppose x <> a ; :: thesis:

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:

per cases ;

suppose A41: max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) <> 0 ; :: thesis:

end;

suppose max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) = 0 ; :: thesis:

hence |.((f . x) - (f . a)).| < r by A33, A40; :: thesis:

end;

hence |.((f . x) - (f . a)).| < r ; :: thesis:

end;

suppose x = a ; :: thesis:

hence |.((f . x) - (f . a)).| < r by A33, ABSVALUE:2; :: thesis:

end;

hence |.((f . x) - (f . a)).| < r ; :: thesis:

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:

per cases by XXREAL_0:15;

suppose min ((a - x1),(x2 - a)) = a - x1 ; :: thesis:

hence min ((a - x1),(x2 - a)) > 0 by A5, XREAL_1:50; :: thesis:

end;

suppose min ((a - x1),(x2 - a)) = x2 - a ; :: thesis:

hence min ((a - x1),(x2 - a)) > 0 by A6, XREAL_1:50; :: thesis:

end;

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

end;

now :: thesis:

per cases by XXREAL_0:15;

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:

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:

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:

end;

hence min ((r / (max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|))),(min ((a - x1),(x2 - a)))) > 0 ; :: thesis:

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:

end;

suppose A44: max (|.(((f . x1) - (f . a)) / (x1 - a)).|,|.(((f . x2) - (f . a)) / (x2 - a)).|) = 0 ; :: thesis:

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

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:
assume that
x in dom f and
A47: |.(x - a).| < min ((a - x1),(x2 - a)) ; :: thesis:
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:

per cases ;

suppose x <> a ; :: thesis:

hence |.((f . x) - (f . a)).| < r by A33, A45, A48, A49; :: thesis:

end;

suppose x = a ; :: thesis:

hence |.((f . x) - (f . a)).| < r by A33, ABSVALUE:2; :: thesis:

end;

hence |.((f . x) - (f . a)).| < r ; :: thesis:

end;

min ((a - x1),(x2 - a)) > 0

proof

now :: thesis:

per cases by XXREAL_0:15;

suppose min ((a - x1),(x2 - a)) = a - x1 ; :: thesis:

hence min ((a - x1),(x2 - a)) > 0 by A5, XREAL_1:50; :: thesis:

end;

suppose min ((a - x1),(x2 - a)) = x2 - a ; :: thesis:

hence min ((a - x1),(x2 - a)) > 0 by A6, XREAL_1:50; :: thesis:

end;

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

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:

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:

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:

end;

hence f is_continuous_in a by FCONT_1:3; :: thesis: