let s, s1 be Real_Sequence; :: thesis: ( ( for n being Nat holds

( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 > 1 implies not s is summable )

assume that

A1: for n being Nat holds

( s . n >= 0 & s1 . n = n -root (s . n) ) and

A2: s1 is convergent and

A3: lim s1 > 1 ; :: thesis: not s is summable

set r = (lim s1) - 1;

(lim s1) - 1 > 0 by A3, XREAL_1:50;

then consider m being Nat such that

A4: for n being Nat st m <= n holds

|.((s1 . n) - (lim s1)).| < (lim s1) - 1 by A2, SEQ_2:def 7;

for n being Nat st m <= n holds

s1 . n >= 1

( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 > 1 implies not s is summable )

assume that

A1: for n being Nat holds

( s . n >= 0 & s1 . n = n -root (s . n) ) and

A2: s1 is convergent and

A3: lim s1 > 1 ; :: thesis: not s is summable

set r = (lim s1) - 1;

(lim s1) - 1 > 0 by A3, XREAL_1:50;

then consider m being Nat such that

A4: for n being Nat st m <= n holds

|.((s1 . n) - (lim s1)).| < (lim s1) - 1 by A2, SEQ_2:def 7;

for n being Nat st m <= n holds

s1 . n >= 1

proof

hence
not s is summable
by A1, Th29; :: thesis: verum
let n be Nat; :: thesis: ( m <= n implies s1 . n >= 1 )

assume m <= n ; :: thesis: s1 . n >= 1

then |.((s1 . n) - (lim s1)).| < (lim s1) - 1 by A4;

then (s1 . n) - (lim s1) > - ((lim s1) - 1) by SEQ_2:1;

then ((s1 . n) - (lim s1)) + (lim s1) > (- ((lim s1) - 1)) + (lim s1) by XREAL_1:6;

hence s1 . n >= 1 ; :: thesis: verum

end;assume m <= n ; :: thesis: s1 . n >= 1

then |.((s1 . n) - (lim s1)).| < (lim s1) - 1 by A4;

then (s1 . n) - (lim s1) > - ((lim s1) - 1) by SEQ_2:1;

then ((s1 . n) - (lim s1)) + (lim s1) > (- ((lim s1) - 1)) + (lim s1) by XREAL_1:6;

hence s1 . n >= 1 ; :: thesis: verum