let p be Real; ( 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
; 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; ( 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
; ( ap is convergent & lim ap = (lim a) to_power p )
now ( ( 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
;
( ap is convergent & lim ap = (lim a) to_power p )now ( ( 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 A12:
for
n being
Nat ex
m being
Nat st
(
n <= m &
a . m <> 0 )
;
( 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 ;
A18:
for
n being
Nat for
x being
Element of
NAT ex
y being
Element of
NAT st
S2[
n,
x,
y]
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]
;
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]
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 )
;
contradiction
now ( ( 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
ex
m being
Nat st
F . m = k
;
contradictionend; case
for
m being
Nat holds
F . m <> k
;
contradictionhence
contradiction
by A25, A31;
verum end; end; end;
hence
contradiction
;
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;
hence
contradiction
by A25;
verum
end; A35:
(
a * F is
convergent &
lim (a * F) = 0 )
by A2, A5, SEQ_4:16, SEQ_4:17;
A36:
now 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)).| < elet e be
Real;
( 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
;
ex k being Nat st
for m being Nat st k <= m holds
|.((ap . m) - ((lim a) to_power p)).| < ethen
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;
for m being Nat st k <= m holds
|.((ap . m) - ((lim a) to_power p)).| < elet m be
Nat;
( k <= m implies |.((ap . m) - ((lim a) to_power p)).| < e )assume A39:
k <= m
;
|.((ap . m) - ((lim a) to_power p)).| < enow ( ( 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 A40:
a . m <> 0
;
|.((ap . m) - ((lim a) to_power p)).| < ethen 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;
verum end; end; end; hence
|.((ap . m) - ((lim a) to_power p)).| < e
;
verum end; hence
ap is
convergent
by SEQ_2:def 6;
lim ap = (lim a) to_power phence
lim ap = (lim a) to_power p
by A36, SEQ_2:def 7;
verum end; end; end; hence
(
ap is
convergent &
lim ap = (lim a) to_power p )
;
verum end; case A47:
lim a <> 0
;
( 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)
then consider k being
Nat such that A53:
rng (a ^\ k) c= dom (#R p)
;
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;
verum end; end; end;
hence
( ap is convergent & lim ap = (lim a) to_power p )
; verum