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
proof
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;
now :: thesis: s . n >= 1
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:4;
hence s . n >= 1 ; :: 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:35;
hence s . n >= 1 by A6, A7, POWER:4; :: thesis: verum
end;
end;
end;
hence s . n >= 1 ; :: thesis: verum
end;
for k being Nat ex n being Nat st
( k <= n & not |.((s . n) - 0).| < 1 )
proof
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;
then ( not s is convergent or not lim s = 0 ) by SEQ_2:def 7;
hence not s is summable by Th4; :: thesis: verum