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

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

let n be Nat; :: thesis: ( n >= m + 1 implies ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 )
A6: m + 1 >= m by NAT_1:11;
A7: Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| by A2;
assume n >= m + 1 ; :: thesis: ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1
then n >= m by A6, XXREAL_0:2;
then |.((||.(seq . (n + 1)).|| / ||.(seq . n).||) - (lim Rseq)).| < (lim Rseq) - 1 by A5, A7;
then - ((lim Rseq) - 1) < (||.(seq . (n + 1)).|| / ||.(seq . n).||) - (lim Rseq) by SEQ_2:1;
then (1 - (lim Rseq)) + (lim Rseq) < ((||.(seq . (n + 1)).|| / ||.(seq . n).||) - (lim Rseq)) + (lim Rseq) by XREAL_1:6;
hence ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 ; :: thesis: verum

end;

hence not seq is summable by A1, Th30; :: thesis: verum