let Z be open Subset of REAL ; :: thesis: ( not 0 in Z implies ((#Z 2) ^ ) `| Z = ((- 2) (#) ((#Z 3) ^ )) | Z )
assume A2:
not 0 in Z
; :: thesis: ((#Z 2) ^ ) `| Z = ((- 2) (#) ((#Z 3) ^ )) | Z
then
(#Z 2) ^ is_differentiable_on Z
by Th34;
then A4:
dom (((#Z 2) ^ ) `| Z) = Z
by FDIFF_1:def 8;
Z c= REAL \ {0 }
by A2, ZFMISC_1:40;
then XX:
Z c= dom ((#Z 3) ^ )
by Th36;
A5: dom (((- 2) (#) ((#Z 3) ^ )) | Z) =
(dom ((- 2) (#) ((#Z 3) ^ ))) /\ Z
by RELAT_1:90
.=
(dom ((#Z 3) ^ )) /\ Z
by VALUED_1:def 5
.=
Z
by XX, XBOOLE_1:28
;
for x0 being Real st x0 in Z holds
(((#Z 2) ^ ) `| Z) . x0 = (((- 2) (#) ((#Z 3) ^ )) | Z) . x0
proof
let x0 be
Real;
:: thesis: ( x0 in Z implies (((#Z 2) ^ ) `| Z) . x0 = (((- 2) (#) ((#Z 3) ^ )) | Z) . x0 )
assume A8:
x0 in Z
;
:: thesis: (((#Z 2) ^ ) `| Z) . x0 = (((- 2) (#) ((#Z 3) ^ )) | Z) . x0
A9:
(#Z 2) ^ is_differentiable_on Z
by A2, Th34;
A11:
x0 <> 0
by A2, A8;
A13:
dom ((- 2) (#) ((#Z 3) ^ )) = dom ((#Z 3) ^ )
by VALUED_1:def 5;
reconsider i = 2
- 1 as
Element of
NAT ;
A16:
x0 #Z i <> 0
by A11, PREPOWER:48;
A17:
x0 |^ i <> 0
by A16, PREPOWER:46;
(((#Z 2) ^ ) `| Z) . x0 =
diff ((#Z 2) ^ ),
x0
by A9, A8, FDIFF_1:def 8
.=
- ((2 * x0) / ((x0 #Z 2) ^2 ))
by ThB, A11
.=
- ((2 * (x0 #Z 1)) / ((x0 #Z 2) ^2 ))
by PREPOWER:45
.=
- ((2 * (x0 #Z 1)) / ((x0 |^ 2) ^2 ))
by PREPOWER:46
.=
- ((2 * (x0 |^ 1)) / ((x0 |^ 2) * (x0 |^ (1 + 1))))
by PREPOWER:46
.=
- ((2 * (x0 |^ 1)) / ((x0 |^ 2) * ((x0 |^ 1) * (x0 |^ 1))))
by NEWTON:13
.=
- ((2 * (x0 |^ 1)) / (((x0 |^ 2) * (x0 |^ 1)) * (x0 |^ 1)))
.=
- ((2 * (x0 |^ 1)) / ((x0 |^ (2 + 1)) * (x0 |^ 1)))
by NEWTON:13
.=
- (2 / (x0 |^ (1 + 2)))
by A17, XCMPLX_1:92
.=
- (2 / (x0 #Z 3))
by PREPOWER:46
.=
- (2 / ((#Z 3) . x0))
by TAYLOR_1:def 1
.=
- (2 * (((#Z 3) . x0) " ))
by XCMPLX_0:def 9
.=
- (2 * (((#Z 3) ^ ) . x0))
by A8, XX, RFUNCT_1:def 8
.=
(- 2) * (((#Z 3) ^ ) . x0)
.=
((- 2) (#) ((#Z 3) ^ )) . x0
by A8, A13, XX, VALUED_1:def 5
.=
(((- 2) (#) ((#Z 3) ^ )) | Z) . x0
by A8, FUNCT_1:72
;
hence
(((#Z 2) ^ ) `| Z) . x0 = (((- 2) (#) ((#Z 3) ^ )) | Z) . x0
;
:: thesis: verum
end;
hence
((#Z 2) ^ ) `| Z = ((- 2) (#) ((#Z 3) ^ )) | Z
by A5, A4, PARTFUN1:34; :: thesis: verum