let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X st ( for n being Nat holds seq . n <> 0. X ) & ex m being Nat st
for n being Nat st n >= m holds
||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 holds
not seq is summable
let seq be sequence of X; :: thesis: ( ( for n being Nat holds seq . n <> 0. X ) & ex m being Nat st
for n being Nat st n >= m holds
||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 implies not seq is summable )
assume A1: for n being Nat holds seq . n <> H1(X) ; :: thesis: ( for m being Nat ex n being Nat st
( n >= m & not ||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 ) or not seq is summable )
given m being Nat such that A2: for n being Nat st n >= m holds
||.(seq . (n + 1)).|| / ||.(seq . n).|| >= 1 ; :: thesis: not seq is summable
A3: now :: thesis: for n being Nat st n >= m holds
||.(seq . n).|| >= ||.(seq . m).||
defpred S1[ Nat] means ||.(seq . (m + $1)).|| >= ||.(seq . m).||;
let n be Nat; :: thesis: ( n >= m implies ||.(seq . n).|| >= ||.(seq . m).|| )
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: ||.(seq . (m + k)).|| >= ||.(seq . m).|| ; :: thesis: S1[k + 1]
seq . (m + k) <> H1(X) by A1;
then A6: ||.(seq . (m + k)).|| <> 0 by CSSPACE:42;
( ||.(seq . ((m + k) + 1)).|| / ||.(seq . (m + k)).|| >= 1 & ||.(seq . (m + k)).|| >= 0 ) by A2, CSSPACE:44, NAT_1:11;
then ||.(seq . ((m + k) + 1)).|| >= ||.(seq . (m + k)).|| by A6, XREAL_1:191;
hence S1[k + 1] by A5, XXREAL_0:2; :: thesis: verum
end;
A7: S1[ 0 ] ;
A8: for k being Nat holds S1[k] from NAT_1:sch 2(A7, A4);
assume n >= m ; :: thesis: ||.(seq . n).|| >= ||.(seq . m).||
then consider k being Nat such that
A9: n = m + k by NAT_1:10;
thus ||.(seq . n).|| >= ||.(seq . m).|| by A8, A9; :: thesis: verum
end;
seq . m <> H1(X) by A1;
then ||.(seq . m).|| <> 0 by CSSPACE:42;
then ||.(seq . m).|| > 0 by CSSPACE:44;
then ( not seq is convergent or lim seq <> H1(X) ) by A3, Th29;
hence not seq is summable by Th9; :: thesis: verum