let rseq be Real_Sequence; for seq being Complex_Sequence st ( for n being Nat holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds
( seq is convergent & lim seq = 0c )
let seq be Complex_Sequence; ( ( for n being Nat holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 implies ( seq is convergent & lim seq = 0c ) )
assume that
A1:
for n being Nat holds |.(seq . n).| <= rseq . n
and
A2:
( rseq is convergent & lim rseq = 0 )
; ( seq is convergent & lim seq = 0c )
(seq_const 0) . 0 = 0
;
then A4:
lim (seq_const 0) = 0
by SEQ_4:25;
then A6:
( abs (Re seq) is convergent & lim (abs (Re seq)) = 0 )
by A2, A4, A3, SEQ_2:19, SEQ_2:20;
then A7:
Re seq is convergent
by SEQ_4:15;
then A10:
( abs (Im seq) is convergent & lim (abs (Im seq)) = 0 )
by A2, A4, A8, SEQ_2:19, SEQ_2:20;
then A11:
Im seq is convergent
by SEQ_4:15;
lim (Im seq) = 0
by A10, SEQ_4:15;
then A12:
Im (lim seq) = 0
by A7, A11, Th42;
lim (Re seq) = 0
by A6, SEQ_4:15;
then
Re (lim seq) = 0
by A7, A11, Th42;
hence
( seq is convergent & lim seq = 0c )
by A7, A11, A12, Lm1, Th42, COMPLEX1:13; verum