let Z be open Subset of REAL; for f being PartFunc of REAL,REAL st f is_differentiable_on 2,Z & ( for x0 being Real st x0 in Z holds
f . x0 <> 0 ) holds
(diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))
let f be PartFunc of REAL,REAL; ( f is_differentiable_on 2,Z & ( for x0 being Real st x0 in Z holds
f . x0 <> 0 ) implies (diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)) )
assume that
A1:
f is_differentiable_on 2,Z
and
A2:
for x0 being Real st x0 in Z holds
f . x0 <> 0
; (diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))
A3:
f is_differentiable_on Z
by A1, Th7;
then A4:
f ^ is_differentiable_on Z
by A2, FDIFF_2:22;
A5:
Z c= dom f
by A3, FDIFF_1:def 6;
A6:
for x0 being Real st x0 in Z holds
(f (#) f) . x0 <> 0
(diff (f,Z)) . 1 =
(diff (f,Z)) . (1 + 0)
.=
((diff (f,Z)) . 0) `| Z
by TAYLOR_1:def 5
.=
(f | Z) `| Z
by TAYLOR_1:def 5
.=
f `| Z
by A3, FDIFF_2:16
;
then A9:
f `| Z is_differentiable_on Z
by A1;
then
(f | Z) `| Z is_differentiable_on Z
by A3, FDIFF_2:16;
then A10:
((diff (f,Z)) . 0) `| Z is_differentiable_on Z
by TAYLOR_1:def 5;
A11:
f (#) f is_differentiable_on Z
by A3, FDIFF_2:20;
then A12:
(f `| Z) / (f (#) f) is_differentiable_on Z
by A9, A6, FDIFF_2:21;
(diff ((f ^),Z)) . 2 =
(diff ((f ^),Z)) . (1 + 1)
.=
((diff ((f ^),Z)) . (1 + 0)) `| Z
by TAYLOR_1:def 5
.=
(((diff ((f ^),Z)) . 0) `| Z) `| Z
by TAYLOR_1:def 5
.=
(((f ^) | Z) `| Z) `| Z
by TAYLOR_1:def 5
.=
((f ^) `| Z) `| Z
by A4, FDIFF_2:16
.=
(- ((f `| Z) / (f (#) f))) `| Z
by A2, A3, FDIFF_2:22
.=
(- 1) (#) (((f `| Z) / (f (#) f)) `| Z)
by A12, FDIFF_2:19
.=
(- 1) (#) (((((f `| Z) `| Z) (#) (f (#) f)) - (((f (#) f) `| Z) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))
by A9, A11, A6, FDIFF_2:21
.=
(- 1) (#) (((((diff (f,Z)) . 2) (#) (f (#) f)) - (((f (#) f) `| Z) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))
by A1, Lm3, Th7
.=
(- 1) (#) (((((diff (f,Z)) . 2) (#) (f (#) f)) - ((((f `| Z) (#) f) + (f (#) (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))
by A3, FDIFF_2:20
.=
(- 1) (#) (((((diff (f,Z)) . 2) (#) (f ^2)) - ((f (#) ((f `| Z) + (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))
by RFUNCT_1:11
.=
(- 1) (#) (((((diff (f,Z)) . 2) (#) (f ^2)) - ((f (#) ((1 (#) (f `| Z)) + (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))
by RFUNCT_1:21
.=
(- 1) (#) (((((diff (f,Z)) . 2) (#) (f ^2)) - ((f (#) ((1 (#) (f `| Z)) + (1 (#) (f `| Z)))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))
by RFUNCT_1:21
.=
(- 1) (#) (((((diff (f,Z)) . 2) (#) (f ^2)) - ((f (#) ((1 + 1) (#) (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))
by Th5
.=
(- 1) (#) (((f (#) (((diff (f,Z)) . 2) (#) f)) - ((f (#) (2 (#) (f `| Z))) (#) (f `| Z))) / ((f (#) f) (#) (f (#) f)))
by RFUNCT_1:9
.=
((- 1) (#) ((f (#) (((diff (f,Z)) . 2) (#) f)) - ((f (#) (2 (#) (f `| Z))) (#) (f `| Z)))) / ((f (#) f) (#) (f (#) f))
by RFUNCT_1:32
.=
(((f (#) (2 (#) (f `| Z))) (#) (f `| Z)) - (f (#) (((diff (f,Z)) . 2) (#) f))) / ((f (#) f) (#) (f (#) f))
by RFUNCT_1:19
.=
((f (#) ((2 (#) (f `| Z)) (#) (f `| Z))) - (f (#) (((diff (f,Z)) . 2) (#) f))) / ((f (#) f) (#) (f (#) f))
by RFUNCT_1:9
.=
(f (#) (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f))) / ((f (#) f) (#) (f (#) f))
by RFUNCT_1:15
.=
(f (#) (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f))) / (f (#) (f (#) (f (#) f)))
by RFUNCT_1:9
.=
(f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))
by RFUNCT_1:34
;
then A13: (diff ((f ^),Z)) . 2 =
(f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))
.=
(((dom f) \ (f " {0})) --> 1) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))
by Lm4
;
A14: dom ((diff (f,Z)) . (1 + 1)) =
dom (((diff (f,Z)) . (0 + 1)) `| Z)
by TAYLOR_1:def 5
.=
dom ((((diff (f,Z)) . 0) `| Z) `| Z)
by TAYLOR_1:def 5
.=
Z
by A10, FDIFF_1:def 7
;
A15: dom (((diff (f,Z)) . 2) (#) f) =
(dom ((diff (f,Z)) . 2)) /\ (dom f)
by VALUED_1:def 4
.=
Z /\ (dom f)
by A14
;
A16: dom ((2 (#) (f `| Z)) (#) (f `| Z)) =
dom (2 (#) ((f `| Z) (#) (f `| Z)))
by RFUNCT_1:13
.=
dom ((f `| Z) (#) (f `| Z))
by VALUED_1:def 5
.=
(dom (f `| Z)) /\ (dom (f `| Z))
by VALUED_1:def 4
.=
dom (f `| Z)
.=
Z
by A3, FDIFF_1:def 7
;
set g1 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f));
set g2 = (f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)));
A17: dom (f (#) (f (#) f)) =
(dom f) /\ (dom (f (#) f))
by VALUED_1:def 4
.=
(dom f) /\ ((dom f) /\ (dom f))
by VALUED_1:def 4
.=
(dom f) /\ (dom f)
.=
dom f
;
A18:
f / f = ((dom f) \ (f " {0})) --> 1
by Lm4;
then A19:
dom (f / f) = (dom f) \ (f " {0})
by FUNCOP_1:13;
A20:
dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) = (dom (f / f)) /\ (dom ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))))
by VALUED_1:def 4;
then A21:
dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) c= dom (f / f)
by XBOOLE_1:17;
A22:
for x being Element of REAL st x in dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) holds
((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x
proof
let x be
Element of
REAL ;
( x in dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) implies ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x )
assume A23:
x in dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))))
;
((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x
((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x =
((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x
.=
((f / f) . x) * (((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x)
by A23, VALUED_1:def 4
.=
1
* (((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x)
by A18, A19, A21, A23, FUNCOP_1:7
.=
((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x
;
hence
((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x
;
verum
end;
dom ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) =
(dom (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f))) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0}))
by RFUNCT_1:def 1
.=
((dom ((2 (#) (f `| Z)) (#) (f `| Z))) /\ (dom (((diff (f,Z)) . 2) (#) f))) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0}))
by VALUED_1:12
.=
(Z /\ (dom (((diff (f,Z)) . 2) (#) f))) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0}))
by A16
.=
(Z /\ (Z /\ (dom f))) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0}))
by A15
.=
((Z /\ Z) /\ (dom f)) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0}))
by XBOOLE_1:16
.=
(Z /\ (dom f)) /\ ((dom (f (#) (f (#) f))) \ ((f (#) (f (#) f)) " {0}))
.=
(Z /\ (dom f)) /\ ((dom f) \ ((f (#) (f (#) f)) " {0}))
by A17
.=
((Z /\ (dom f)) /\ (dom f)) \ ((f (#) (f (#) f)) " {0})
by XBOOLE_1:49
.=
(Z /\ ((dom f) /\ (dom f))) \ ((f (#) (f (#) f)) " {0})
by XBOOLE_1:16
.=
(Z /\ (dom f)) \ ((f (#) (f (#) f)) " {0})
.=
Z \ ((f (#) (f (#) f)) " {0})
by A5, XBOOLE_1:28
.=
Z \ (f " {0})
by Lm5
;
then
dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) = dom ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))
by A5, A19, A20, XBOOLE_1:28, XBOOLE_1:33;
hence
(diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))
by A18, A13, A22, PARTFUN1:5; verum