let seq be Real_Sequence; :: thesis: ( seq is non-zero & seq is convergent & lim seq = 0 & seq is non-decreasing implies for n being Nat holds seq . n < 0 )
assume that
A1: seq is non-zero and
A2: ( seq is convergent & lim seq = 0 ) and
A3: seq is non-decreasing and
A4: not for n being Nat holds seq . n < 0 ; :: thesis: contradiction
consider n being Nat such that
A5: not seq . n < 0 by A4;
now :: thesis: contradiction
per cases ( 0 < seq . n or seq . n = 0 ) by A5;
suppose A6: 0 < seq . n ; :: thesis: contradiction
then consider n1 being Nat such that
A7: for m being Nat st n1 <= m holds
|.((seq . m) - 0).| < seq . n by A2, SEQ_2:def 7;
|.((seq . (n1 + n)) - 0).| < seq . n by A7, NAT_1:12;
then ( n <= n1 + n & seq . (n1 + n) < seq . n ) by A6, ABSVALUE:def 1, NAT_1:12;
hence contradiction by A3, SEQM_3:6; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum