let s, s1 be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds
( s . n >= 0 & s1 . n = n -root (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 that
A1: for n being Element of NAT holds
( s . n >= 0 & s1 . n = n -root (s . n) ) and
A2: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
s1 . n >= 1 ; :: thesis: not s is summable
consider m being Element of NAT such that
A3: for n being Element of NAT st m <= n holds
s1 . n >= 1 by A2;
A4: for n being Element of NAT st m + 1 <= n holds
s . n >= 1

proof

let n be Element of NAT ; :: thesis: ( m + 1 <= n implies s . n >= 1 )
assume A5: m + 1 <= n ; :: thesis: s . n >= 1
1 <= 1 + m by NAT_1:11;
then A6: 1 <= n by A5, XXREAL_0:2;
A7: s . n >= 0 by A1;
m <= m + 1 by NAT_1:11;
then m <= n by A5, XXREAL_0:2;
then s1 . n >= 1 by A3;
then A8: n -root (s . n) >= 1 by A1;

now

per cases ( n -root (s . n) = 1 or n -root (s . n) > 1 ) by A8, XXREAL_0:1;

suppose n -root (s . n) = 1 ; :: thesis: s . n >= 1

then s . n = 1 |^ n by A6, A7, POWER:5;
hence s . n >= 1 by NEWTON:15; :: thesis: verum

end;

suppose n -root (s . n) > 1 ; :: thesis: s . n >= 1

then (n -root (s . n)) to_power n > 1 by A5, POWER:40;
hence s . n >= 1 by A6, A7, POWER:5; :: thesis: verum

end;

end;

end;

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

end;

for k being Element of NAT ex n being Element of NAT st
( k <= n & not abs ((s . n) - 0 ) < 1 )

proof

let k be Element of NAT ; :: thesis: ex n being Element of NAT st
( k <= n & not abs ((s . n) - 0 ) < 1 )
take n = (m + 1) + k; :: thesis: ( k <= n & not abs ((s . n) - 0 ) < 1 )
not s . n < 1 by A4, NAT_1:11;
hence ( k <= n & not abs ((s . n) - 0 ) < 1 ) by NAT_1:11, SEQ_2:9; :: thesis: verum

end;

then ( not s is convergent or not lim s = 0 ) by SEQ_2:def 7;
hence not s is summable by Th7; :: thesis: verum