let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X st ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Nat st
for n being Nat st n >= m holds
Rseq . n >= 1 holds
not seq is summable
let X be RealUnitarySpace; :: thesis: for seq being sequence of X st ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Nat st
for n being Nat st n >= m holds
Rseq . n >= 1 holds
not seq is summable
let seq be sequence of X; :: thesis: ( ( for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ) & ex m being Nat st
for n being Nat st n >= m holds
Rseq . n >= 1 implies not seq is summable )
assume A1: for n being Nat holds Rseq . n = n -root (||.seq.|| . n) ; :: thesis: ( for m being Nat ex n being Nat st
( n >= m & not Rseq . n >= 1 ) or not seq is summable )
given m being Nat such that A2: for n being Nat st n >= m holds
Rseq . n >= 1 ; :: thesis: not seq is summable
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 A3: n >= m + 1 ; :: thesis: ||.(seq . n).|| >= 1
m + 1 >= 1 by NAT_1:11;
then A4: n >= 1 by A3, XXREAL_0:2;
m + 1 >= m by NAT_1:11;
then A5: n >= m by A3, XXREAL_0:2;
Rseq . n = n -root (||.seq.|| . n) by A1
.= n -root ||.(seq . n).|| by BHSP_2:def 3 ;
then ( ||.(seq . n).|| >= 0 & (n -root ||.(seq . n).||) |^ n >= 1 ) by A2, A5, BHSP_1:28, PREPOWER:11;
hence ||.(seq . n).|| >= 1 by A4, POWER:4; :: thesis: verum
end;
then ( not seq is convergent or lim seq <> H1(X) ) by Th29;
hence not seq is summable by Th9; :: thesis: verum