let seq be Real_Sequence; :: thesis: ( seq is convergent & ( for n being Nat holds seq . n <= 0 ) implies lim seq <= 0 )
assume that
A1: seq is convergent and
A2: for n being Nat holds seq . n <= 0 ; :: thesis: lim seq <= 0
set seq1 = - seq;
A3: now :: thesis: for n being Nat holds - 0 <= (- seq) . n
let n be Nat; :: thesis: - 0 <= (- seq) . n
( (- seq) . n = - (seq . n) & seq . n <= 0 ) by A2, SEQ_1:10;
hence - 0 <= (- seq) . n by XREAL_1:24; :: thesis: verum
end;
- seq is convergent by A1, SEQ_2:9;
then 0 <= lim (- seq) by A3, SEQ_2:17;
then - 0 <= - (lim seq) by A1, SEQ_2:10;
hence lim seq <= 0 by XREAL_1:24; :: thesis: verum