let x0 be Real; :: thesis: for n being Element of NAT
for Z being open Subset of REAL st not 0 in Z & x0 in Z holds
(((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0))
let n be Element of NAT ; :: thesis: for Z being open Subset of REAL st not 0 in Z & x0 in Z holds
(((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0))
let Z be open Subset of REAL; :: thesis: ( not 0 in Z & x0 in Z implies (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0)) )
assume that
A1: not 0 in Z and
A2: x0 in Z ; :: thesis: (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0))
A3: (#Z n) ^ is_differentiable_on Z by A1, Th43;
per cases ( n > 0 or n = 0 ) ;
suppose n > 0 ; :: thesis: (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0))
then 0 < 0 + n ;
then n >= 1 by NAT_1:19;
then reconsider i = n - 1 as Element of NAT by INT_1:5;
x0 #Z i <> 0 by A1, A2, PREPOWER:38;
then A4: x0 |^ i <> 0 by PREPOWER:36;
(((#Z n) ^) `| Z) . x0 = diff (((#Z n) ^),x0) by A2, A3, FDIFF_1:def 7
.= - ((n * (x0 #Z i)) / ((x0 #Z n) ^2)) by A1, A2, Th29
.= - ((n * (x0 #Z i)) / ((x0 |^ n) ^2)) by PREPOWER:36
.= - ((n * (x0 |^ i)) / ((x0 |^ n) ^2)) by PREPOWER:36
.= - ((n * (x0 |^ i)) / ((x0 |^ (i + 1)) * ((x0 |^ 1) * (x0 |^ i)))) by NEWTON:8
.= - ((n * (x0 |^ i)) / (((x0 |^ (i + 1)) * (x0 |^ 1)) * (x0 |^ i)))
.= - ((n * (x0 |^ i)) / ((x0 |^ ((i + 1) + 1)) * (x0 |^ i))) by NEWTON:8
.= - (n / (x0 |^ (i + 2))) by A4, XCMPLX_1:91
.= - (n / (x0 #Z (i + 2))) by PREPOWER:36
.= - (n / ((#Z (n + 1)) . x0)) by TAYLOR_1:def 1 ;
hence (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0)) ; :: thesis: verum
end;
suppose A5: n = 0 ; :: thesis: (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0))
(((#Z n) ^) `| Z) . x0 = diff (((#Z n) ^),x0) by A2, A3, FDIFF_1:def 7
.= - ((0 * (x0 #Z (n - 1))) / ((x0 #Z n) ^2)) by A1, A2, A5, Th29
.= - (n / ((#Z (n + 1)) . x0)) by A5 ;
hence (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0)) ; :: thesis: verum
end;
end;