let s be Real_Sequence; :: thesis: ( s is summable implies ( s is convergent & lim s = 0 ) )
assume s is summable ; :: thesis: ( s is convergent & lim s = 0 )
then A1: Partial_Sums s is convergent ;
now :: thesis: for n being Nat holds ((Partial_Sums s) ^\ 1) . n = ((Partial_Sums s) . n) + ((s ^\ 1) . n)
let n be Nat; :: thesis: ((Partial_Sums s) ^\ 1) . n = ((Partial_Sums s) . n) + ((s ^\ 1) . n)
(Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by Def1;
then (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + ((s ^\ 1) . n) by NAT_1:def 3;
hence ((Partial_Sums s) ^\ 1) . n = ((Partial_Sums s) . n) + ((s ^\ 1) . n) by NAT_1:def 3; :: thesis: verum
end;
then A2: (Partial_Sums s) ^\ 1 = (Partial_Sums s) + (s ^\ 1) by SEQ_1:7;
now :: thesis: for n being Element of NAT holds ((s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s))) . n = (s ^\ 1) . n
let n be Element of NAT ; :: thesis: ((s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s))) . n = (s ^\ 1) . n
thus ((s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s))) . n = ((s ^\ 1) . n) + (((Partial_Sums s) + (- (Partial_Sums s))) . n) by SEQ_1:7
.= ((s ^\ 1) . n) + (((Partial_Sums s) . n) + ((- (Partial_Sums s)) . n)) by SEQ_1:7
.= ((s ^\ 1) . n) + (((Partial_Sums s) . n) + (- ((Partial_Sums s) . n))) by SEQ_1:10
.= (s ^\ 1) . n ; :: thesis: verum
end;
then (s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s)) = s ^\ 1 ;
then A3: s ^\ 1 = ((Partial_Sums s) ^\ 1) - (Partial_Sums s) by A2, SEQ_1:31;
then A4: s ^\ 1 is convergent by A1;
hence s is convergent by SEQ_4:21; :: thesis: lim s = 0
lim ((Partial_Sums s) ^\ 1) = lim (Partial_Sums s) by A1, SEQ_4:20;
then lim (((Partial_Sums s) ^\ 1) - (Partial_Sums s)) = (lim (Partial_Sums s)) - (lim (Partial_Sums s)) by A1, SEQ_2:12
.= 0 ;
hence lim s = 0 by A3, A4, SEQ_4:22; :: thesis: verum