let X be RealNormSpace; :: thesis: for seq being sequence of X

for rseq1 being Real_Sequence st ( for n being Nat holds

( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds

seq is norm_summable

let seq be sequence of X; :: thesis: for rseq1 being Real_Sequence st ( for n being Nat holds

( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds

seq is norm_summable

let rseq1 be Real_Sequence; :: thesis: ( ( for n being Nat holds

( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is norm_summable )

assume that

A1: for n being Nat holds

( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) and

A2: ( rseq1 is convergent & lim rseq1 < 1 ) ; :: thesis: seq is norm_summable

then A7: abs ||.seq.|| is summable ;

hence seq is norm_summable by A7; :: thesis: verum

for rseq1 being Real_Sequence st ( for n being Nat holds

( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds

seq is norm_summable

let seq be sequence of X; :: thesis: for rseq1 being Real_Sequence st ( for n being Nat holds

( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds

seq is norm_summable

let rseq1 be Real_Sequence; :: thesis: ( ( for n being Nat holds

( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is norm_summable )

assume that

A1: for n being Nat holds

( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) and

A2: ( rseq1 is convergent & lim rseq1 < 1 ) ; :: thesis: seq is norm_summable

now :: thesis: for n being Nat holds

( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) )

then
||.seq.|| is absolutely_summable
by A2, SERIES_1:37;( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) )

let n be Nat; :: thesis: ( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) )

A3: 0 <= ||.seq.|| . n by Th2;

A4: 0 <= ||.seq.|| . (n + 1) by Th2;

A5: (abs ||.seq.||) . (n + 1) = |.(||.seq.|| . (n + 1)).| by SEQ_1:12

.= ||.seq.|| . (n + 1) by A4, ABSVALUE:def 1 ;

A6: ( seq . n <> 0. X & ||.seq.|| . n = ||.(seq . n).|| ) by A1, NORMSP_0:def 4;

(abs ||.seq.||) . n = |.(||.seq.|| . n).| by SEQ_1:12

.= ||.seq.|| . n by A3, ABSVALUE:def 1 ;

hence ( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) ) by A1, A5, A6, NORMSP_0:def 5; :: thesis: verum

end;A3: 0 <= ||.seq.|| . n by Th2;

A4: 0 <= ||.seq.|| . (n + 1) by Th2;

A5: (abs ||.seq.||) . (n + 1) = |.(||.seq.|| . (n + 1)).| by SEQ_1:12

.= ||.seq.|| . (n + 1) by A4, ABSVALUE:def 1 ;

A6: ( seq . n <> 0. X & ||.seq.|| . n = ||.(seq . n).|| ) by A1, NORMSP_0:def 4;

(abs ||.seq.||) . n = |.(||.seq.|| . n).| by SEQ_1:12

.= ||.seq.|| . n by A3, ABSVALUE:def 1 ;

hence ( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) ) by A1, A5, A6, NORMSP_0:def 5; :: thesis: verum

then A7: abs ||.seq.|| is summable ;

now :: thesis: for n being Element of NAT holds (abs ||.seq.||) . n = ||.seq.|| . n

then
abs ||.seq.|| = ||.seq.||
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (abs ||.seq.||) . n = ||.seq.|| . n

A8: 0 <= ||.seq.|| . n by Th2;

thus (abs ||.seq.||) . n = |.(||.seq.|| . n).| by SEQ_1:12

.= ||.seq.|| . n by A8, ABSVALUE:def 1 ; :: thesis: verum

end;A8: 0 <= ||.seq.|| . n by Th2;

thus (abs ||.seq.||) . n = |.(||.seq.|| . n).| by SEQ_1:12

.= ||.seq.|| . n by A8, ABSVALUE:def 1 ; :: thesis: verum

hence seq is norm_summable by A7; :: thesis: verum