let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds Rseq . n = n -root (||.seq.|| . n) ) & Rseq is convergent & lim Rseq > 1 holds
not seq is summable
let X be RealUnitarySpace; :: thesis: for seq being sequence of X st ( for n being Element of 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 n being Element of 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 Element of 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 Element of NAT such that
A4: for n being Element of NAT st n >= m holds
abs ((Rseq . n) - (lim Rseq)) < (lim Rseq) - 1 by A2, SEQ_2:def 7;

now

let n be Element of 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 BHSP_2:def 3 ;
m + 1 >= m by NAT_1:11;
then n >= m by A5, XXREAL_0:2;
then abs ((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 BHSP_1:28, 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 Th31;
hence not seq is summable by Th9; :: thesis: verum