let s, s1 be Real_Sequence; :: thesis: ( ( for n being Nat holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 > 1 implies not s is summable )

assume that

A1: for n being Nat holds s1 . n = n -root ((abs s) . n) and

A2: s1 is convergent and

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

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

then consider m being Nat such that

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

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

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

assume that

A1: for n being Nat holds s1 . n = n -root ((abs s) . n) and

A2: s1 is convergent and

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

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

then consider m being Nat such that

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

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

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

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

then
( not s is convergent or lim s <> 0 )
by Th38;|.(s . n).| >= 1

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

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

A6: s1 . n = n -root ((abs s) . n) by A1

.= n -root |.(s . n).| by SEQ_1:12 ;

m + 1 >= m by NAT_1:11;

then n >= m by A5, XXREAL_0:2;

then |.((n -root |.(s . n).|) - (lim s1)).| < (lim s1) - 1 by A4, A6;

then - ((lim s1) - 1) < (n -root |.(s . n).|) - (lim s1) by SEQ_2:1;

then (1 - (lim s1)) + (lim s1) < ((n -root |.(s . n).|) - (lim s1)) + (lim s1) by XREAL_1:6;

then A7: ( |.(s . n).| >= 0 & (n -root |.(s . n).|) |^ n >= 1 ) by COMPLEX1:46, PREPOWER:11;

m + 1 >= 1 by NAT_1:11;

then n >= 1 by A5, XXREAL_0:2;

hence |.(s . n).| >= 1 by A7, POWER:4; :: thesis: verum

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

A6: s1 . n = n -root ((abs s) . n) by A1

.= n -root |.(s . n).| by SEQ_1:12 ;

m + 1 >= m by NAT_1:11;

then n >= m by A5, XXREAL_0:2;

then |.((n -root |.(s . n).|) - (lim s1)).| < (lim s1) - 1 by A4, A6;

then - ((lim s1) - 1) < (n -root |.(s . n).|) - (lim s1) by SEQ_2:1;

then (1 - (lim s1)) + (lim s1) < ((n -root |.(s . n).|) - (lim s1)) + (lim s1) by XREAL_1:6;

then A7: ( |.(s . n).| >= 0 & (n -root |.(s . n).|) |^ n >= 1 ) by COMPLEX1:46, PREPOWER:11;

m + 1 >= 1 by NAT_1:11;

then n >= 1 by A5, XXREAL_0:2;

hence |.(s . n).| >= 1 by A7, POWER:4; :: thesis: verum

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