let seq be Real_Sequence; :: thesis: ( abs seq is convergent & lim (abs seq) = 0 implies ( seq is convergent & lim seq = 0 ) )
assume that
A1: abs seq is convergent and
A2: lim (abs seq) = 0 ; :: thesis: ( seq is convergent & lim seq = 0 )
A3: now :: thesis: for n being Nat holds
( (- (abs seq)) . n <= seq . n & seq . n <= (abs seq) . n )
let n be Nat; :: thesis: ( (- (abs seq)) . n <= seq . n & seq . n <= (abs seq) . n )
- |.(seq . n).| <= seq . n by ABSVALUE:4;
then A4: - ((abs seq) . n) <= seq . n by SEQ_1:12;
seq . n <= |.(seq . n).| by ABSVALUE:4;
hence ( (- (abs seq)) . n <= seq . n & seq . n <= (abs seq) . n ) by A4, SEQ_1:10, SEQ_1:12; :: thesis: verum
end;
A5: ( - (abs seq) is convergent & lim (- (abs seq)) = - (lim (abs seq)) ) by A1, SEQ_2:10;
hence seq is convergent by A1, A2, A3, SEQ_2:19; :: thesis: lim seq = 0
thus lim seq = 0 by A1, A2, A5, A3, SEQ_2:20; :: thesis: verum