let s1, s be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
s1 . n >= 1 implies not s is summable )
assume A1: for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ; :: thesis: ( for m being Element of NAT ex n being Element of NAT st
( m <= n & not s1 . n >= 1 ) or not s is summable )
given m being Element of NAT such that A2: for n being Element of NAT st m <= n holds
s1 . n >= 1 ; :: thesis: not s is summable

now

let n be Element of NAT ; :: thesis: ( n >= m + 1 implies abs (s . n) >= 1 )
assume A3: n >= m + 1 ; :: thesis: abs (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 (abs (s . n)) by SEQ_1:12 ;
then ( abs (s . n) >= 0 & (n -root (abs (s . n))) |^ n >= 1 ) by A2, A5, COMPLEX1:46, PREPOWER:11;
hence abs (s . n) >= 1 by A4, POWER:4; :: thesis: verum

end;

then ( not s is convergent or lim s <> 0 ) by Th43;
hence not s is summable by Th7; :: thesis: verum