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

( s . n >= 0 & s1 . n = n -root (s . n) ) ) & ex m being Nat st

for n being Nat st m <= n holds

s1 . n >= 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: ex m being Nat st

for n being Nat st m <= n holds

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

consider m being Nat such that

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

s1 . n >= 1 by A2;

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

s . n >= 1

( k <= n & not |.((s . n) - 0).| < 1 )

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

( s . n >= 0 & s1 . n = n -root (s . n) ) ) & ex m being Nat st

for n being Nat st m <= n holds

s1 . n >= 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: ex m being Nat st

for n being Nat st m <= n holds

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

consider m being Nat such that

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

s1 . n >= 1 by A2;

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

s . n >= 1

proof

for k being Nat ex n being Nat st
let n be 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;

end;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 :: thesis: s . n >= 1

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

( k <= n & not |.((s . n) - 0).| < 1 )

proof

then
( not s is convergent or not lim s = 0 )
by SEQ_2:def 7;
let k be Nat; :: thesis: ex n being Nat st

( k <= n & not |.((s . n) - 0).| < 1 )

take n = (m + 1) + k; :: thesis: ( k <= n & not |.((s . n) - 0).| < 1 )

not s . n < 1 by A4, NAT_1:11;

hence ( k <= n & not |.((s . n) - 0).| < 1 ) by NAT_1:11, SEQ_2:1; :: thesis: verum

end;( k <= n & not |.((s . n) - 0).| < 1 )

take n = (m + 1) + k; :: thesis: ( k <= n & not |.((s . n) - 0).| < 1 )

not s . n < 1 by A4, NAT_1:11;

hence ( k <= n & not |.((s . n) - 0).| < 1 ) by NAT_1:11, SEQ_2:1; :: thesis: verum

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