let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = 0 iff ( abs seq is convergent & lim (abs seq) = 0 ) )

thus ( seq is convergent & lim seq = 0 implies ( abs seq is convergent & lim (abs seq) = 0 ) ) :: thesis: ( abs seq is convergent & lim (abs seq) = 0 implies ( seq is convergent & lim seq = 0 ) )

thus ( seq is convergent & lim seq = 0 implies ( abs seq is convergent & lim (abs seq) = 0 ) ) :: thesis: ( abs seq is convergent & lim (abs seq) = 0 implies ( seq is convergent & lim seq = 0 ) )

proof

thus
( abs seq is convergent & lim (abs seq) = 0 implies ( seq is convergent & lim seq = 0 ) )
by SEQ_4:15; :: thesis: verum
assume that

A1: seq is convergent and

A2: lim seq = 0 ; :: thesis: ( abs seq is convergent & lim (abs seq) = 0 )

lim (abs seq) = |.0.| by A1, A2, SEQ_4:14

.= 0 by ABSVALUE:2 ;

hence ( abs seq is convergent & lim (abs seq) = 0 ) by A1; :: thesis: verum

end;A1: seq is convergent and

A2: lim seq = 0 ; :: thesis: ( abs seq is convergent & lim (abs seq) = 0 )

lim (abs seq) = |.0.| by A1, A2, SEQ_4:14

.= 0 by ABSVALUE:2 ;

hence ( abs seq is convergent & lim (abs seq) = 0 ) by A1; :: thesis: verum