let p be Real; :: thesis: ( 0 < p implies for a, ap being Real_Sequence st a is convergent & ( for n being Nat holds 0 <= a . n ) & ( for n being Nat holds ap . n = (a . n) to_power p ) holds
( ap is convergent & lim ap = (lim a) to_power p ) )
assume A1: 0 < p ; :: thesis: for a, ap being Real_Sequence st a is convergent & ( for n being Nat holds 0 <= a . n ) & ( for n being Nat holds ap . n = (a . n) to_power p ) holds
( ap is convergent & lim ap = (lim a) to_power p )
let a, ap be Real_Sequence; :: thesis: ( a is convergent & ( for n being Nat holds 0 <= a . n ) & ( for n being Nat holds ap . n = (a . n) to_power p ) implies ( ap is convergent & lim ap = (lim a) to_power p ) )
assume that
A2: a is convergent and
A3: for n being Nat holds 0 <= a . n and
A4: for n being Nat holds ap . n = (a . n) to_power p ; :: thesis: ( ap is convergent & lim ap = (lim a) to_power p )
now :: thesis: ( ( lim a = 0 & ap is convergent & lim ap = (lim a) to_power p ) or ( lim a <> 0 & ap is convergent & lim ap = (lim a) to_power p ) )
per cases ( lim a = 0 or lim a <> 0 ) ;
case A5: lim a = 0 ; :: thesis: ( ap is convergent & lim ap = (lim a) to_power p )
now :: thesis: ( ( ex n being Nat st
for m being Nat st n <= m holds
a . m = 0 & ap is convergent & lim ap = (lim a) to_power p ) or ( ( for n being Nat ex m being Nat st
( n <= m & a . m <> 0 ) ) & ap is convergent & lim ap = (lim a) to_power p ) )
per cases ( ex n being Nat st
for m being Nat st n <= m holds
a . m = 0 or for n being Nat ex m being Nat st
( n <= m & a . m <> 0 ) ) ;
case ex n being Nat st
for m being Nat st n <= m holds
a . m = 0 ; :: thesis: ( ap is convergent & lim ap = (lim a) to_power p )
then consider N being Nat such that
A6: for m being Nat st N <= m holds
a . m = 0 ;
A7: for n being Nat holds (a ^\ N) . n = 0
proof
let n be Nat; :: thesis: (a ^\ N) . n = 0
a . (n + N) = 0 by A6, NAT_1:12;
hence (a ^\ N) . n = 0 by NAT_1:def 3; :: thesis: verum
end;
A8: now :: thesis: for e being Real st e > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e
let e be Real; :: thesis: ( e > 0 implies ex n being Nat st
for m being Nat st n <= m holds
|.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e )
assume A9: e > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e
reconsider n = 0 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e
let m be Nat; :: thesis: ( n <= m implies |.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e )
assume n <= m ; :: thesis: |.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e
A10: (lim a) to_power p = 0 by A1, A5, POWER:def 2;
(ap ^\ N) . m = ap . (m + N) by NAT_1:def 3
.= (a . (m + N)) to_power p by A4
.= ((a ^\ N) . m) to_power p by NAT_1:def 3
.= 0 to_power p by A7
.= 0 by A1, POWER:def 2 ;
hence |.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e by A9, A10, ABSVALUE:2; :: thesis: verum
end;
then A11: ap ^\ N is convergent by SEQ_2:def 6;
then (lim a) to_power p = lim (ap ^\ N) by A8, SEQ_2:def 7;
hence ( ap is convergent & lim ap = (lim a) to_power p ) by A11, SEQ_4:20, SEQ_4:21; :: thesis: verum
end;
case A12: for n being Nat ex m being Nat st
( n <= m & a . m <> 0 ) ; :: thesis: ( ap is convergent & lim ap = (lim a) to_power p )
defpred S1[ set ] means a . $1 <> 0 ;
ex m1 being Nat st
( 0 <= m1 & a . m1 <> 0 ) by A12;
then A13: ex m being Nat st S1[m] ;
consider M being Nat such that
A14: ( S1[M] & ( for n being Nat st S1[n] holds
M <= n ) ) from NAT_1:sch 5(A13);
defpred S2[ set , set , set ] means for n, m being Nat st $2 = n & $3 = m holds
( n < m & a . m <> 0 & ( for k being Nat st n < k & a . k <> 0 holds
m <= k ) );
A15: (lim a) to_power p = 0 by A1, A5, POWER:def 2;
reconsider M = M as Nat ;
A16: now :: thesis: for n being Nat ex m being Nat st
( n < m & a . m <> 0 )
let n be Nat; :: thesis: ex m being Nat st
( n < m & a . m <> 0 )
consider m being Nat such that
A17: ( n + 1 <= m & a . m <> 0 ) by A12;
take m = m; :: thesis: ( n < m & a . m <> 0 )
thus ( n < m & a . m <> 0 ) by A17, NAT_1:13; :: thesis: verum
end;
A18: for n being Nat
for x being Element of NAT ex y being Element of NAT st S2[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S2[n,x,y]
let x be Element of NAT ; :: thesis: ex y being Element of NAT st S2[n,x,y]
defpred S3[ Nat] means ( x < $1 & a . $1 <> 0 );
ex m being Nat st S3[m] by A16;
then A19: ex m being Nat st S3[m] ;
consider l being Nat such that
A20: ( S3[l] & ( for k being Nat st S3[k] holds
l <= k ) ) from NAT_1:sch 5(A19);
 take l ; :: thesis: ( l is Element of NAT & S2[n,x,l] )
l in NAT by ORDINAL1:def 12;
hence ( l is Element of NAT & S2[n,x,l] ) by A20; :: thesis: verum
end;
reconsider zz = 0 as Element of NAT ;
consider F being sequence of NAT such that
A21: ( F . 0 = In (M,NAT) & ( for n being Nat holds S2[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A18);
 rng F c= NAT by RELAT_1:def 19;
then A22: rng F c= REAL by NUMBERS:19;
dom F = NAT by FUNCT_2:def 1;
then reconsider F = F as Real_Sequence by A22, RELSET_1:4;
for n being Nat holds F . n < F . (n + 1) by A21;
then reconsider F = F as V46() sequence of NAT by SEQM_3:def 6;
A23: for n being Nat st a . n <> 0 holds
ex m being Nat st F . m = n
proof
defpred S3[ set ] means ( a . $1 <> 0 & ( for m being Nat holds F . m <> $1 ) );
assume ex n being Nat st S3[n] ; :: thesis: contradiction
then A24: ex n being Nat st S3[n] ;
consider M1 being Nat such that
A25: ( S3[M1] & ( for n being Nat st S3[n] holds
M1 <= n ) ) from NAT_1:sch 5(A24);
 defpred S4[ Nat] means ( $1 < M1 & a . $1 <> 0 & ex m being Nat st F . m = $1 );
A26: ex n being Nat st S4[n]
proof
take M ; :: thesis: S4[M]
( M <= M1 & M <> M1 ) by A14, A21, A25;
hence M < M1 by XXREAL_0:1; :: thesis: ( a . M <> 0 & ex m being Nat st F . m = M )
thus a . M <> 0 by A14; :: thesis: ex m being Nat st F . m = M
take 0 ; :: thesis: F . 0 = M
thus F . 0 = M by A21; :: thesis: verum
end;
A27: for n being Nat st S4[n] holds
n <= M1 ;
consider MX being Nat such that
A28: ( S4[MX] & ( for n being Nat st S4[n] holds
n <= MX ) ) from NAT_1:sch 6(A27, A26);
 A29: for k being Nat st MX < k & k < M1 holds
a . k = 0
proof
given k being Nat such that A30: MX < k and
A31: ( k < M1 & a . k <> 0 ) ; :: thesis: contradiction
now :: thesis: ( ( ex m being Nat st F . m = k & contradiction ) or ( ( for m being Nat holds F . m <> k ) & contradiction ) )
per cases ( ex m being Nat st F . m = k or for m being Nat holds F . m <> k ) ;
case for m being Nat holds F . m <> k ; :: thesis: contradiction
hence contradiction by A25, A31; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
consider m being Nat such that
A32: F . m = MX by A28;
A33: ( MX < F . (m + 1) & a . (F . (m + 1)) <> 0 ) by A21, A32;
A34: F . (m + 1) <= M1 by A21, A25, A28, A32;
now :: thesis: not F . (m + 1) <> M1
assume F . (m + 1) <> M1 ; :: thesis: contradiction
then F . (m + 1) < M1 by A34, XXREAL_0:1;
hence contradiction by A29, A33; :: thesis: verum
end;
hence contradiction by A25; :: thesis: verum
end;
A35: ( a * F is convergent & lim (a * F) = 0 ) by A2, A5, SEQ_4:16, SEQ_4:17;
A36: now :: thesis: for e being Real st 0 < e holds
ex k being Nat st
for m being Nat st k <= m holds
|.((ap . m) - ((lim a) to_power p)).| < e
let e be Real; :: thesis: ( 0 < e implies ex k being Nat st
for m being Nat st k <= m holds
|.((ap . m) - ((lim a) to_power p)).| < e )
assume A37: 0 < e ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.((ap . m) - ((lim a) to_power p)).| < e
then 0 < e to_power (1 / p) by POWER:34;
then consider n being Nat such that
A38: for m being Nat st n <= m holds
|.(((a * F) . m) - 0).| < e to_power (1 / p) by A35, SEQ_2:def 7;
reconsider k = F . n as Nat ;
take k = k; :: thesis: for m being Nat st k <= m holds
|.((ap . m) - ((lim a) to_power p)).| < e
let m be Nat; :: thesis: ( k <= m implies |.((ap . m) - ((lim a) to_power p)).| < e )
assume A39: k <= m ; :: thesis: |.((ap . m) - ((lim a) to_power p)).| < e
now :: thesis: ( ( a . m = 0 & |.((ap . m) - ((lim a) to_power p)).| < e ) or ( a . m <> 0 & |.((ap . m) - ((lim a) to_power p)).| < e ) )
per cases ( a . m = 0 or a . m <> 0 ) ;
case a . m = 0 ; :: thesis: |.((ap . m) - ((lim a) to_power p)).| < e
then ap . m = 0 to_power p by A4
.= 0 by A1, POWER:def 2 ;
hence |.((ap . m) - ((lim a) to_power p)).| < e by A15, A37, ABSVALUE:2; :: thesis: verum
end;
case A40: a . m <> 0 ; :: thesis: |.((ap . m) - ((lim a) to_power p)).| < e
then consider l being Nat such that
A41: m = F . l by A23;
A42: l in NAT by ORDINAL1:def 12;
n <= l by A39, A41, SEQM_3:1;
then |.(((a * F) . l) - 0).| < e to_power (1 / p) by A38;
then A43: |.(a . (F . l)).| < e to_power (1 / p) by FUNCT_2:15, A42;
A44: (a . m) to_power p = ap . m by A4;
A45: a . m > 0 by A3, A40;
then A46: 0 < ap . m by A44, POWER:34;
|.(a . m).| > 0 by A40, COMPLEX1:47;
then |.(a . m).| to_power p < (e to_power (1 / p)) to_power p by A1, A41, A43, POWER:37;
then |.(a . m).| to_power p < e to_power ((1 / p) * p) by A37, POWER:33;
then |.(a . m).| to_power p < e to_power 1 by A1, XCMPLX_1:106;
then |.(a . m).| to_power p < e by POWER:25;
then ap . m < e by A45, A44, ABSVALUE:def 1;
hence |.((ap . m) - ((lim a) to_power p)).| < e by A15, A46, ABSVALUE:def 1; :: thesis: verum
end;
end;
end;
hence |.((ap . m) - ((lim a) to_power p)).| < e ; :: thesis: verum
end;
hence ap is convergent by SEQ_2:def 6; :: thesis: lim ap = (lim a) to_power p
hence lim ap = (lim a) to_power p by A36, SEQ_2:def 7; :: thesis: verum
end;
end;
end;
hence ( ap is convergent & lim ap = (lim a) to_power p ) ; :: thesis: verum
end;
case A47: lim a <> 0 ; :: thesis: ( ap is convergent & lim ap = (lim a) to_power p )
A48: 0 <= lim a by A2, A3, SEQ_2:17;
ex k being Nat st rng (a ^\ k) c= dom (#R p)
proof
set e0 = lim a;
A49: (lim a) / 2 > 0 by A47, A48, XREAL_1:215;
then consider k being Nat such that
A50: for m being Nat st k <= m holds
|.((a . m) - (lim a)).| < (lim a) / 2 by A2, SEQ_2:def 7;
take k ; :: thesis: rng (a ^\ k) c= dom (#R p)
A51: now :: thesis: for m being Nat holds 0 < (a ^\ k) . m
let m be Nat; :: thesis: 0 < (a ^\ k) . m
|.((a . (k + m)) - (lim a)).| < (lim a) / 2 by A50, NAT_1:12;
then - ((lim a) / 2) <= (a . (k + m)) - (lim a) by ABSVALUE:5;
then (- ((lim a) / 2)) + (lim a) <= ((a . (k + m)) - (lim a)) + (lim a) by XREAL_1:7;
hence 0 < (a ^\ k) . m by A49, NAT_1:def 3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (a ^\ k) or x in dom (#R p) )
assume x in rng (a ^\ k) ; :: thesis: x in dom (#R p)
then consider n being Element of NAT such that
A52: x = (a ^\ k) . n by FUNCT_2:113;
0 < (a ^\ k) . n by A51;
then (a ^\ k) . n in { g where g is Real : 0 < g } ;
then (a ^\ k) . n in right_open_halfline 0 by XXREAL_1:230;
hence x in dom (#R p) by A52, TAYLOR_1:def 4; :: thesis: verum
end;
then consider k being Nat such that
A53: rng (a ^\ k) c= dom (#R p) ;
now :: thesis: for x being object st x in NAT holds
((#R p) /* (a ^\ k)) . x = (ap ^\ k) . x
let x be object ; :: thesis: ( x in NAT implies ((#R p) /* (a ^\ k)) . x = (ap ^\ k) . x )
assume x in NAT ; :: thesis: ((#R p) /* (a ^\ k)) . x = (ap ^\ k) . x
then reconsider n = x as Element of NAT ;
(a ^\ k) . n in rng (a ^\ k) by VALUED_0:28;
then (a ^\ k) . n in dom (#R p) by A53;
then A54: (a ^\ k) . n in right_open_halfline 0 by TAYLOR_1:def 4;
then a . (k + n) in right_open_halfline 0 by NAT_1:def 3;
then a . (k + n) in { g where g is Real : 0 < g } by XXREAL_1:230;
then A55: ex g being Real st
( a . (k + n) = g & g > 0 ) ;
thus ((#R p) /* (a ^\ k)) . x = (#R p) . ((a ^\ k) . n) by A53, FUNCT_2:108
.= ((a ^\ k) . n) #R p by A54, TAYLOR_1:def 4
.= (a . (k + n)) #R p by NAT_1:def 3
.= (a . (k + n)) to_power p by A55, POWER:def 2
.= ap . (k + n) by A4
.= (ap ^\ k) . x by NAT_1:def 3 ; :: thesis: verum
end;
then A56: (#R p) /* (a ^\ k) = ap ^\ k by FUNCT_2:12;
A57: lim (a ^\ k) = lim a by A2, SEQ_4:20;
lim a > 0 by A2, A3, A47, SEQ_2:17;
then #R p is_continuous_in lim (a ^\ k) by A57, FDIFF_1:24, TAYLOR_1:21;
then A58: ( (#R p) /* (a ^\ k) is convergent & (#R p) . (lim (a ^\ k)) = lim ((#R p) /* (a ^\ k)) ) by A2, A53, FCONT_1:def 1;
lim a in { g where g is Real : 0 < g } by A47, A48;
then lim a in right_open_halfline 0 by XXREAL_1:230;
then (#R p) . (lim (a ^\ k)) = (lim a) #R p by A57, TAYLOR_1:def 4
.= (lim a) to_power p by A47, A48, POWER:def 2 ;
hence ( ap is convergent & lim ap = (lim a) to_power p ) by A58, A56, SEQ_4:21, SEQ_4:22; :: thesis: verum
end;
end;
end;
hence ( ap is convergent & lim ap = (lim a) to_power p ) ; :: thesis: verum