let s, s1 be Real_Sequence; :: thesis: ( ( for n being Nat holds s1 . n = n -root ((abs s) . n) ) & ex m being Nat st

for n being Nat st m <= n holds

s1 . n >= 1 implies not s is summable )

assume A1: for n being Nat holds s1 . n = n -root ((abs s) . n) ; :: thesis: ( for m being Nat ex n being Nat st

( m <= n & not s1 . n >= 1 ) or not s is summable )

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

s1 . n >= 1 ; :: thesis: not s is summable

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

for n being Nat st m <= n holds

s1 . n >= 1 implies not s is summable )

assume A1: for n being Nat holds s1 . n = n -root ((abs s) . n) ; :: thesis: ( for m being Nat ex n being Nat st

( m <= n & not s1 . n >= 1 ) or not s is summable )

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

s1 . n >= 1 ; :: thesis: not s is summable

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 A3: n >= m + 1 ; :: thesis: |.(s . n).| >= 1

m + 1 >= 1 by NAT_1:11;

then A4: n >= 1 by A3, XXREAL_0:2;

m + 1 >= m by NAT_1:11;

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

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

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

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

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

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

m + 1 >= 1 by NAT_1:11;

then A4: n >= 1 by A3, XXREAL_0:2;

m + 1 >= m by NAT_1:11;

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

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

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

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

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

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