let a be Real; for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x > 0 & x <> 0 ) ) holds
( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) )
let Z be open Subset of REAL; for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x > 0 & x <> 0 ) ) holds
( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) )
let f1, f2 be PartFunc of REAL,REAL; ( Z c= dom (ln * (f1 / f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x > 0 & x <> 0 ) ) implies ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) ) )
assume that
A1:
Z c= dom (ln * (f1 / f2))
and
A2:
f2 = #Z 2
and
A3:
for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x > 0 & x <> 0 )
; ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) )
A4:
for x being Real st x in Z holds
f2 is_differentiable_in x
by A2, TAYLOR_1:2;
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 A5:
Z c= (dom f1) /\ ((dom f2) \ (f2 " {0}))
by RFUNCT_1:def 1;
then A6:
Z c= dom f1
by XBOOLE_1:18;
A7:
for x being Real st x in Z holds
f1 . x = (1 * x) + (- a)
proof
let x be
Real;
( x in Z implies f1 . x = (1 * x) + (- a) )
A8:
(1 * x) + (- a) = (1 * x) - a
;
assume
x in Z
;
f1 . x = (1 * x) + (- a)
hence
f1 . x = (1 * x) + (- a)
by A3, A8;
verum
end;
then A9:
f1 is_differentiable_on Z
by A6, FDIFF_1:23;
A10:
Z c= dom f2
by A5, XBOOLE_1:1;
then A11:
f2 is_differentiable_on Z
by A4, FDIFF_1:9;
for x being Real st x in Z holds
f2 . x <> 0
by A3;
then A12:
f1 / f2 is_differentiable_on Z
by A9, A11, FDIFF_2:21;
A13:
f2 is_differentiable_on Z
by A10, A4, FDIFF_1:9;
A14:
for x being Real st x in Z holds
(f2 `| Z) . x = 2 * x
A16:
for x being Real st x in Z holds
((f1 / f2) `| Z) . x = ((2 * a) - x) / (x |^ 3)
proof
let x be
Real;
( x in Z implies ((f1 / f2) `| Z) . x = ((2 * a) - x) / (x |^ 3) )
A17:
f2 is_differentiable_in x
by A2, TAYLOR_1:2;
A18:
f2 . x =
x #Z 2
by A2, TAYLOR_1:def 1
.=
x |^ 2
by PREPOWER:36
;
assume A19:
x in Z
;
((f1 / f2) `| Z) . x = ((2 * a) - x) / (x |^ 3)
then A20:
x <> 0
by A3;
(
f1 is_differentiable_in x &
f2 . x <> 0 )
by A3, A9, A19, FDIFF_1:9;
then diff (
(f1 / f2),
x) =
(((diff (f1,x)) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2)
by A17, FDIFF_2:14
.=
((((f1 `| Z) . x) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2)
by A9, A19, FDIFF_1:def 7
.=
((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2)
by A11, A19, FDIFF_1:def 7
.=
((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2)
by A6, A7, A19, FDIFF_1:23
.=
((1 * (f2 . x)) - ((2 * x) * (f1 . x))) / ((f2 . x) ^2)
by A14, A19
.=
((x |^ (1 + 1)) - ((2 * x) * (x - a))) / ((x |^ 2) ^2)
by A3, A19, A18
.=
(((x |^ 1) * x) - ((2 * x) * (x - a))) / ((x |^ 2) ^2)
by NEWTON:6
.=
((x * x) - ((2 * x) * (x - a))) / ((x |^ 2) ^2)
.=
(x * ((2 * a) - x)) / (x |^ (2 + 2))
by NEWTON:8
.=
(x * ((2 * a) - x)) / (x |^ (3 + 1))
.=
(x * ((2 * a) - x)) / ((x |^ 3) * x)
by NEWTON:6
.=
((2 * a) - x) / (x |^ 3)
by A20, XCMPLX_1:91
;
hence
((f1 / f2) `| Z) . x = ((2 * a) - x) / (x |^ 3)
by A12, A19, FDIFF_1:def 7;
verum
end;
A21:
for x being Real st x in Z holds
(f1 / f2) . x > 0
A24:
for x being Real st x in Z holds
ln * (f1 / f2) is_differentiable_in x
then A25:
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 = ((2 * a) - x) / (x * (x - a))
proof
let x be
Real;
( x in Z implies ((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) )
assume A26:
x in Z
;
((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a))
then A27:
x in dom (f1 / f2)
by A1, FUNCT_1:11;
A28:
f2 . x =
x #Z 2
by A2, TAYLOR_1:def 1
.=
x |^ 2
by PREPOWER:36
;
then A29:
x |^ 2
> 0
by A3, A26;
A30:
f1 . x = x - a
by A3, A26;
(
f1 / f2 is_differentiable_in x &
(f1 / f2) . x > 0 )
by A12, A21, A26, 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, A26, FDIFF_1:def 7
.=
(((2 * a) - x) / (x |^ 3)) / ((f1 / f2) . x)
by A16, A26
.=
(((2 * a) - x) / (x |^ 3)) / ((f1 . x) * ((f2 . x) "))
by A27, RFUNCT_1:def 1
.=
(((2 * a) - x) / (x |^ (2 + 1))) / ((x - a) / (x |^ 2))
by A28, A30, XCMPLX_0:def 9
.=
(((2 * a) - x) / ((x |^ 2) * x)) / ((x - a) / (x |^ 2))
by NEWTON:6
.=
((((2 * a) - x) / (x |^ 2)) / x) / ((x - a) / (x |^ 2))
by XCMPLX_1:78
.=
((((2 * a) - x) / (x |^ 2)) / ((x - a) / (x |^ 2))) / x
by XCMPLX_1:48
.=
(((2 * a) - x) / (x - a)) / x
by A29, XCMPLX_1:55
.=
((2 * a) - x) / (x * (x - a))
by XCMPLX_1:78
;
hence
((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a))
by A25, A26, 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 = ((2 * a) - x) / (x * (x - a)) ) )
by A1, A24, FDIFF_1:9; verum