let a, b be Real; for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 ) ) holds
( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) )
let Z be open Subset of REAL; for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 ) ) holds
( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) )
let f1, f2 be PartFunc of REAL,REAL; ( Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 ) ) implies ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) ) )
assume that
A1:
Z c= dom (ln * (f1 / f2))
and
A2:
for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 )
; ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) )
A3:
for x being Real st x in Z holds
( f1 . x = (1 * x) + (- a) & f2 . x = (1 * x) + (- b) )
proof
let x be
Real;
( x in Z implies ( f1 . x = (1 * x) + (- a) & f2 . x = (1 * x) + (- b) ) )
A4:
(
(1 * x) + (- a) = (1 * x) - a &
(1 * x) + (- b) = (1 * x) - b )
;
assume
x in Z
;
( f1 . x = (1 * x) + (- a) & f2 . x = (1 * x) + (- b) )
hence
(
f1 . x = (1 * x) + (- a) &
f2 . x = (1 * x) + (- b) )
by A2, A4;
verum
end;
then A5:
for x being Real st x in Z holds
f1 . x = (1 * x) + (- a)
;
for y being object st y in Z holds
y in dom (f1 / f2)
by A1, FUNCT_1:11;
then
Z c= dom (f1 / f2)
by TARSKI:def 3;
then A6:
Z c= (dom f1) /\ ((dom f2) \ (f2 " {0}))
by RFUNCT_1:def 1;
then A7:
Z c= dom f1
by XBOOLE_1:18;
then A8:
f1 is_differentiable_on Z
by A5, FDIFF_1:23;
A9:
for x being Real st x in Z holds
f2 . x = (1 * x) + (- b)
by A3;
A10:
Z c= dom f2
by A6, XBOOLE_1:1;
then A11:
f2 is_differentiable_on Z
by A9, FDIFF_1:23;
for x being Real st x in Z holds
f2 . x <> 0
by A2;
then A12:
f1 / f2 is_differentiable_on Z
by A8, A11, FDIFF_2:21;
A13:
for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2)
proof
let x be
Real;
( x in Z implies ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) )
assume A14:
x in Z
;
((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2)
then A15:
f2 . x <> 0
by A2;
A16:
(
f1 . x = x - a &
f2 . x = x - b )
by A2, A14;
(
f1 is_differentiable_in x &
f2 is_differentiable_in x )
by A8, A11, A14, FDIFF_1:9;
then diff (
(f1 / f2),
x) =
(((diff (f1,x)) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2)
by A15, FDIFF_2:14
.=
((((f1 `| Z) . x) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2)
by A8, A14, FDIFF_1:def 7
.=
((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2)
by A11, A14, FDIFF_1:def 7
.=
((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2)
by A7, A5, A14, FDIFF_1:23
.=
((1 * (f2 . x)) - (1 * (f1 . x))) / ((f2 . x) ^2)
by A10, A9, A14, FDIFF_1:23
.=
(a - b) / ((x - b) ^2)
by A16
;
hence
((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2)
by A12, A14, FDIFF_1:def 7;
verum
end;
A17:
for x being Real st x in Z holds
(f1 / f2) . x > 0
A20:
for x being Real st x in Z holds
ln * (f1 / f2) is_differentiable_in x
then A21:
ln * (f1 / f2) is_differentiable_on Z
by A1, FDIFF_1:9;
for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b))
proof
let x be
Real;
( x in Z implies ((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) )
assume A22:
x in Z
;
((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b))
then A23:
(
f2 . x = x - b &
f2 . x > 0 )
by A2;
A24:
(
f1 . x = x - a &
f2 . x = x - b )
by A2, A22;
A25:
x in dom (f1 / f2)
by A1, A22, FUNCT_1:11;
(
f1 / f2 is_differentiable_in x &
(f1 / f2) . x > 0 )
by A12, A17, A22, FDIFF_1:9;
then diff (
(ln * (f1 / f2)),
x) =
(diff ((f1 / f2),x)) / ((f1 / f2) . x)
by TAYLOR_1:20
.=
(((f1 / f2) `| Z) . x) / ((f1 / f2) . x)
by A12, A22, FDIFF_1:def 7
.=
((a - b) / ((x - b) ^2)) / ((f1 / f2) . x)
by A13, A22
.=
((a - b) / ((x - b) ^2)) / ((f1 . x) * ((f2 . x) "))
by A25, RFUNCT_1:def 1
.=
((a - b) / ((x - b) * (x - b))) / ((x - a) / (x - b))
by A24, XCMPLX_0:def 9
.=
(((a - b) / (x - b)) / (x - b)) / ((x - a) / (x - b))
by XCMPLX_1:78
.=
(((a - b) / (x - b)) / ((x - a) / (x - b))) / (x - b)
by XCMPLX_1:48
.=
((a - b) / (x - a)) / (x - b)
by A23, XCMPLX_1:55
.=
(a - b) / ((x - a) * (x - b))
by XCMPLX_1:78
;
hence
((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b))
by A21, A22, FDIFF_1:def 7;
verum
end;
hence
( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) )
by A1, A20, FDIFF_1:9; verum