let s be Real_Sequence; :: thesis: ( ex n being Nat st s ^\ n is summable implies s is summable )
given n being Nat such that A1: s ^\ n is summable ; :: thesis: s is summable
reconsider PS = (Partial_Sums s) . n as Element of REAL ;
set s1 = seq_const ((Partial_Sums s) . n);
for k being Nat holds ((Partial_Sums s) ^\ (n + 1)) . k = ((Partial_Sums (s ^\ (n + 1))) . k) + ((seq_const ((Partial_Sums s) . n)) . k)
proof
defpred S1[ Nat] means ((Partial_Sums s) ^\ (n + 1)) . $1 = ((Partial_Sums (s ^\ (n + 1))) . $1) + ((seq_const ((Partial_Sums s) . n)) . $1);
A2: (Partial_Sums (s ^\ (n + 1))) . 0 = (s ^\ (n + 1)) . 0 by Def1
.= s . (0 + (n + 1)) by NAT_1:def 3
.= s . (n + 1) ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: ((Partial_Sums s) ^\ (n + 1)) . k = ((Partial_Sums (s ^\ (n + 1))) . k) + ((seq_const ((Partial_Sums s) . n)) . k) ; :: thesis: S1[k + 1]
((Partial_Sums (s ^\ (n + 1))) . (k + 1)) + ((seq_const ((Partial_Sums s) . n)) . (k + 1)) = ((seq_const ((Partial_Sums s) . n)) . (k + 1)) + (((Partial_Sums (s ^\ (n + 1))) . k) + ((s ^\ (n + 1)) . (k + 1))) by Def1
.= (((seq_const ((Partial_Sums s) . n)) . (k + 1)) + ((Partial_Sums (s ^\ (n + 1))) . k)) + ((s ^\ (n + 1)) . (k + 1))
.= (((Partial_Sums s) . n) + ((Partial_Sums (s ^\ (n + 1))) . k)) + ((s ^\ (n + 1)) . (k + 1)) by SEQ_1:57
.= (((Partial_Sums s) ^\ (n + 1)) . k) + ((s ^\ (n + 1)) . (k + 1)) by A4, SEQ_1:57
.= ((Partial_Sums s) . (k + (n + 1))) + ((s ^\ (n + 1)) . (k + 1)) by NAT_1:def 3
.= ((Partial_Sums s) . (k + (n + 1))) + (s . ((k + 1) + (n + 1))) by NAT_1:def 3
.= (Partial_Sums s) . ((k + (n + 1)) + 1) by Def1
.= (Partial_Sums s) . ((k + 1) + (n + 1))
.= ((Partial_Sums s) ^\ (n + 1)) . (k + 1) by NAT_1:def 3 ;
hence S1[k + 1] ; :: thesis: verum
end;
((Partial_Sums s) ^\ (n + 1)) . 0 = (Partial_Sums s) . (0 + (n + 1)) by NAT_1:def 3
.= (s . (n + 1)) + ((Partial_Sums s) . n) by Def1
.= ((Partial_Sums (s ^\ (n + 1))) . 0) + ((seq_const ((Partial_Sums s) . n)) . 0) by A2, SEQ_1:57 ;
then A5: S1[ 0 ] ;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A5, A3); :: thesis: verum
end;
then A6: (Partial_Sums s) ^\ (n + 1) = (Partial_Sums (s ^\ (n + 1))) + (seq_const ((Partial_Sums s) . n)) by SEQ_1:7
.= (Partial_Sums ((s ^\ n) ^\ 1)) + (seq_const ((Partial_Sums s) . n)) by NAT_1:48 ;
(s ^\ n) ^\ 1 is summable by A1, Th12;
then Partial_Sums ((s ^\ n) ^\ 1) is convergent ;
then (Partial_Sums s) ^\ (n + 1) is convergent by A6;
then Partial_Sums s is convergent by SEQ_4:21;
hence s is summable ; :: thesis: verum