let s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n <> 0 ) & ex m being Nat st

for n being Nat st n >= m holds

((abs s) . (n + 1)) / ((abs s) . n) >= 1 implies not s is summable )

assume A1: for n being Nat holds s . n <> 0 ; :: thesis: ( for m being Nat ex n being Nat st

( n >= m & not ((abs s) . (n + 1)) / ((abs s) . n) >= 1 ) or not s is summable )

given m being Nat such that A2: for n being Nat st n >= m holds

((abs s) . (n + 1)) / ((abs s) . n) >= 1 ; :: thesis: not s is summable

then |.(s . m).| > 0 by COMPLEX1:47;

then ( not s is convergent or lim s <> 0 ) by A3, Th38;

hence not s is summable by Th4; :: thesis: verum

for n being Nat st n >= m holds

((abs s) . (n + 1)) / ((abs s) . n) >= 1 implies not s is summable )

assume A1: for n being Nat holds s . n <> 0 ; :: thesis: ( for m being Nat ex n being Nat st

( n >= m & not ((abs s) . (n + 1)) / ((abs s) . n) >= 1 ) or not s is summable )

given m being Nat such that A2: for n being Nat st n >= m holds

((abs s) . (n + 1)) / ((abs s) . n) >= 1 ; :: thesis: not s is summable

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

|.(s . n).| >= |.(s . m).|

s . m <> 0
by A1;|.(s . n).| >= |.(s . m).|

defpred S_{1}[ Nat] means |.(s . (m + $1)).| >= |.(s . m).|;

A4: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

assume n >= m ; :: thesis: |.(s . n).| >= |.(s . m).|

then consider k being Nat such that

A7: n = m + k by NAT_1:10;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A8: n = m + k by A7;

A9: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A9, A4);

hence |.(s . n).| >= |.(s . m).| by A8; :: thesis: verum

end;A4: for k being Nat st S

S

proof

let n be Nat; :: thesis: ( n >= m implies |.(s . n).| >= |.(s . m).| )
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: |.(s . (m + k)).| >= |.(s . m).| ; :: thesis: S_{1}[k + 1]

((abs s) . ((m + k) + 1)) / ((abs s) . (m + k)) >= 1 by A2, NAT_1:11;

then |.(s . ((m + k) + 1)).| / ((abs s) . (m + k)) >= 1 by SEQ_1:12;

then A6: |.(s . ((m + k) + 1)).| / |.(s . (m + k)).| >= 1 by SEQ_1:12;

s . (m + k) <> 0 by A1;

then |.(s . (m + k)).| > 0 by COMPLEX1:47;

then |.(s . ((m + k) + 1)).| >= |.(s . (m + k)).| by A6, XREAL_1:191;

hence S_{1}[k + 1]
by A5, XXREAL_0:2; :: thesis: verum

end;assume A5: |.(s . (m + k)).| >= |.(s . m).| ; :: thesis: S

((abs s) . ((m + k) + 1)) / ((abs s) . (m + k)) >= 1 by A2, NAT_1:11;

then |.(s . ((m + k) + 1)).| / ((abs s) . (m + k)) >= 1 by SEQ_1:12;

then A6: |.(s . ((m + k) + 1)).| / |.(s . (m + k)).| >= 1 by SEQ_1:12;

s . (m + k) <> 0 by A1;

then |.(s . (m + k)).| > 0 by COMPLEX1:47;

then |.(s . ((m + k) + 1)).| >= |.(s . (m + k)).| by A6, XREAL_1:191;

hence S

assume n >= m ; :: thesis: |.(s . n).| >= |.(s . m).|

then consider k being Nat such that

A7: n = m + k by NAT_1:10;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A8: n = m + k by A7;

A9: S

for k being Nat holds S

hence |.(s . n).| >= |.(s . m).| by A8; :: thesis: verum

then |.(s . m).| > 0 by COMPLEX1:47;

then ( not s is convergent or lim s <> 0 ) by A3, Th38;

hence not s is summable by Th4; :: thesis: verum