let X be RealNormSpace; :: 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 norm_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 norm_summable )

assume that

A1: for n being Nat holds seq . n <> 0. X and

A2: ex m being Nat st

for n being Nat st n >= m holds

(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 ; :: thesis: not seq is norm_summable

consider m being Nat such that

A3: for n being Nat st n >= m holds

(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 by A2;

for n being Nat st n >= m holds

(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 holds

not seq is norm_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 norm_summable )

assume that

A1: for n being Nat holds seq . n <> 0. X and

A2: ex m being Nat st

for n being Nat st n >= m holds

(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 ; :: thesis: not seq is norm_summable

consider m being Nat such that

A3: for n being Nat st n >= m holds

(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 by A2;

A4: now :: thesis: for n being Nat st n >= m holds

((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1

((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1

let n be Nat; :: thesis: ( n >= m implies ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 )

assume A5: n >= m ; :: thesis: ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1

A6: 0 <= ||.seq.|| . n by Th2;

A7: 0 <= ||.seq.|| . (n + 1) by Th2;

A8: (abs ||.seq.||) . (n + 1) = |.(||.seq.|| . (n + 1)).| by SEQ_1:12

.= ||.seq.|| . (n + 1) by A7, ABSVALUE:def 1 ;

(abs ||.seq.||) . n = |.(||.seq.|| . n).| by SEQ_1:12

.= ||.seq.|| . n by A6, ABSVALUE:def 1 ;

hence ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 by A3, A5, A8; :: thesis: verum

end;assume A5: n >= m ; :: thesis: ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1

A6: 0 <= ||.seq.|| . n by Th2;

A7: 0 <= ||.seq.|| . (n + 1) by Th2;

A8: (abs ||.seq.||) . (n + 1) = |.(||.seq.|| . (n + 1)).| by SEQ_1:12

.= ||.seq.|| . (n + 1) by A7, ABSVALUE:def 1 ;

(abs ||.seq.||) . n = |.(||.seq.|| . n).| by SEQ_1:12

.= ||.seq.|| . n by A6, ABSVALUE:def 1 ;

hence ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 by A3, A5, A8; :: thesis: verum

now :: thesis: for n being Nat holds ||.seq.|| . n <> 0

hence
not ||.seq.|| is summable
by A4, SERIES_1:39; :: according to LOPBAN_3:def 3 :: thesis: verumlet n be Nat; :: thesis: ||.seq.|| . n <> 0

seq . n <> 0. X by A1;

then ||.(seq . n).|| <> 0 by NORMSP_0:def 5;

hence ||.seq.|| . n <> 0 by NORMSP_0:def 4; :: thesis: verum

end;seq . n <> 0. X by A1;

then ||.(seq . n).|| <> 0 by NORMSP_0:def 5;

hence ||.seq.|| . n <> 0 by NORMSP_0:def 4; :: thesis: verum