let h, x be Real; :: thesis: ( x + (h / 2) > 0 & x - (h / 2) > 0 implies (cD (ln,h)) . x = ln . (1 + (h / (x - (h / 2)))) )
set f = ln ;
assume A1: ( x + (h / 2) > 0 & x - (h / 2) > 0 ) ; :: thesis: (cD (ln,h)) . x = ln . (1 + (h / (x - (h / 2))))
A2: x + (h / 2) in right_open_halfline 0
proof
x + (h / 2) in { g where g is Real : 0 < g } by A1;
hence x + (h / 2) in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum
end;
A3: x - (h / 2) in right_open_halfline 0
proof
x - (h / 2) in { g where g is Real : 0 < g } by A1;
hence x - (h / 2) in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum
end;
(cD (ln,h)) . x = (ln . (x + (h / 2))) - (ln . (x - (h / 2))) by A2, A3, DIFF_1:39, TAYLOR_1:18
.= ln . (((x - (h / 2)) + h) / (x - (h / 2))) by A1, Th4
.= ln . (((x - (h / 2)) / (x - (h / 2))) + (h / (x - (h / 2))))
.= ln . (1 + (h / (x - (h / 2)))) by A1, XCMPLX_1:60 ;
hence (cD (ln,h)) . x = ln . (1 + (h / (x - (h / 2)))) ; :: thesis: verum