let seq be Complex_Sequence; for z being Complex st 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Nat holds seq . (n + 1) = (seq . n) * z ) holds
( seq is convergent & lim seq = 0c )
let z be Complex; ( 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Nat holds seq . (n + 1) = (seq . n) * z ) implies ( seq is convergent & lim seq = 0c ) )
assume that
A1:
0 < |.z.|
and
A2:
|.z.| < 1
; ( not seq . 0 = z or ex n being Nat st not seq . (n + 1) = (seq . n) * z or ( seq is convergent & lim seq = 0c ) )
deffunc H1( Nat) -> object = |.z.| to_power ($1 + 1);
consider rseq1 being Real_Sequence such that
A3:
for n being Nat holds rseq1 . n = H1(n)
from SEQ_1:sch 1();
assume that
A4:
seq . 0 = z
and
A5:
for n being Nat holds seq . (n + 1) = (seq . n) * z
; ( seq is convergent & lim seq = 0c )
A6:
for n being Nat holds |.(seq . n).| = |.z.| to_power (n + 1)
(seq_const 0) . 0 = 0
;
then A14:
lim (seq_const 0) = 0
by SEQ_4:25;
A15:
( rseq1 is convergent & lim rseq1 = 0 )
by A1, A2, A3, SERIES_1:1;
then A16:
( abs (Re seq) is convergent & lim (abs (Re seq)) = 0 )
by A14, A15, A10, SEQ_2:19, SEQ_2:20;
then A17:
Re seq is convergent
by SEQ_4:15;
then A18:
( abs (Im seq) is convergent & lim (abs (Im seq)) = 0 )
by A14, A15, A12, SEQ_2:19, SEQ_2:20;
then A19:
Im seq is convergent
by SEQ_4:15;
lim (Im seq) = 0
by A18, SEQ_4:15;
then A20:
Im (lim seq) = 0
by A17, A19, Th42;
lim (Re seq) = 0
by A16, SEQ_4:15;
then
Re (lim seq) = 0
by A17, A19, Th42;
hence
( seq is convergent & lim seq = 0c )
by A17, A19, A20, Lm1, Th42, COMPLEX1:13; verum