let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
let seq be sequence of X; :: thesis: for Rseq being Real_Sequence st ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
let Rseq be Real_Sequence; :: thesis: ( ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 implies not seq is summable )
assume that
A1: for n being Nat holds Rseq . n = n -root (||.seq.|| . n) and
A2: Rseq is convergent and
A3: lim Rseq > 1 ; :: thesis: not seq is summable
(lim Rseq) - 1 > 0 by A3, XREAL_1:50;
then consider m being Nat such that
A4: for n being Nat st n >= m holds
|.((Rseq . n) - (lim Rseq)).| < (lim Rseq) - 1 by A2, SEQ_2:def 7;

now :: thesis: for n being Nat st n >= m + 1 holds
||.(seq . n).|| >= 1

let n be Nat; :: thesis: ( n >= m + 1 implies ||.(seq . n).|| >= 1 )
assume A5: n >= m + 1 ; :: thesis: ||.(seq . n).|| >= 1
A6: Rseq . n = n -root (||.seq.|| . n) by A1
.= n -root ||.(seq . n).|| by CLVECT_2:def 3 ;
m + 1 >= m by NAT_1:11;
then n >= m by A5, XXREAL_0:2;
then |.((n -root ||.(seq . n).||) - (lim Rseq)).| < (lim Rseq) - 1 by A4, A6;
then - ((lim Rseq) - 1) < (n -root ||.(seq . n).||) - (lim Rseq) by SEQ_2:1;
then (1 - (lim Rseq)) + (lim Rseq) < ((n -root ||.(seq . n).||) - (lim Rseq)) + (lim Rseq) by XREAL_1:6;
then A7: ( ||.(seq . n).|| >= 0 & (n -root ||.(seq . n).||) |^ n >= 1 ) by CSSPACE:44, PREPOWER:11;
m + 1 >= 1 by NAT_1:11;
then n >= 1 by A5, XXREAL_0:2;
hence ||.(seq . n).|| >= 1 by A7, POWER:4; :: thesis: verum

end;

then ( not seq is convergent or lim seq <> H₁(X) ) by Th29;
hence not seq is summable by Th9; :: thesis: verum