let seq be Complex_Sequence; :: thesis: for z being Element of COMPLEX st 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ) holds
( seq is convergent & lim seq = 0c )
let z be Element of COMPLEX ; :: thesis: ( 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ) implies ( seq is convergent & lim seq = 0c ) )
assume A1: ( 0 < |.z.| & |.z.| < 1 ) ; :: thesis: ( not seq . 0 = z or ex n being Element of NAT st not seq . (n + 1) = (seq . n) * z or ( seq is convergent & lim seq = 0c ) )
assume A2: ( seq . 0 = z & ( for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ) ) ; :: thesis: ( seq is convergent & lim seq = 0c )
A3: for n being Element of NAT holds |.(seq . n).| = |.z.| to_power (n + 1)

proof

defpred S₁[ Element of NAT ] means |.(seq . $1).| = |.z.| to_power ($1 + 1);
A4: S₁[ 0 ] by A2, POWER:30;
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
|.(seq . (k + 1)).| = |.((seq . k) * z).| by A2
.= (|.z.| to_power (k + 1)) * |.z.| by A6, COMPLEX1:151
.= (|.z.| to_power (k + 1)) * (|.z.| to_power 1) by POWER:30
.= |.z.| to_power ((k + 1) + 1) by A1, POWER:32 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A5);
hence for n being Element of NAT holds |.(seq . n).| = |.z.| to_power (n + 1) ; :: thesis: verum

end;

C . 0 = 0 by FUNCOP_1:13;
then A7: ( C is convergent & lim C = 0 ) by SEQ_4:40;
deffunc H₁( Element of NAT ) -> Element of REAL = |.z.| to_power ($1 + 1);
consider rseq1 being Real_Sequence such that
A8: for n being Element of NAT holds rseq1 . n = H₁(n) from SEQ_1:sch 1();
A9: ( rseq1 is convergent & lim rseq1 = 0 ) by A1, A8, SERIES_1:1;
A10: ( ( for n being Element of NAT holds C . n <= (abs (Re seq)) . n ) & ( for n being Element of NAT holds (abs (Re seq)) . n <= rseq1 . n ) )

proof

A11: now

let n be Element of NAT ; :: thesis: C . n <= (abs (Re seq)) . n
0 <= (abs (Re seq)) . n

proof

(abs (Re seq)) . n = abs ((Re seq) . n) by SEQ_1:16;
hence 0 <= (abs (Re seq)) . n by COMPLEX1:132; :: thesis: verum

end;

hence C . n <= (abs (Re seq)) . n by FUNCOP_1:13; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: (abs (Re seq)) . n <= rseq1 . n
(abs (Re seq)) . n = abs ((Re seq) . n) by SEQ_1:16;
then A12: (abs (Re seq)) . n = abs (Re (seq . n)) by Def3;
A13: abs (Re (seq . n)) <= |.(seq . n).| by Th13;
|.(seq . n).| = |.z.| to_power (n + 1) by A3;
hence (abs (Re seq)) . n <= rseq1 . n by A8, A12, A13; :: thesis: verum

end;

hence ( ( for n being Element of NAT holds C . n <= (abs (Re seq)) . n ) & ( for n being Element of NAT holds (abs (Re seq)) . n <= rseq1 . n ) ) by A11; :: thesis: verum

end;

A14: ( ( for n being Element of NAT holds C . n <= (abs (Im seq)) . n ) & ( for n being Element of NAT holds (abs (Im seq)) . n <= rseq1 . n ) )

proof

A15: now

let n be Element of NAT ; :: thesis: C . n <= (abs (Im seq)) . n
0 <= (abs (Im seq)) . n

proof

(abs (Im seq)) . n = abs ((Im seq) . n) by SEQ_1:16;
hence 0 <= (abs (Im seq)) . n by COMPLEX1:132; :: thesis: verum

end;

hence C . n <= (abs (Im seq)) . n by FUNCOP_1:13; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: (abs (Im seq)) . n <= rseq1 . n
A16: (abs (Im seq)) . n = abs ((Im seq) . n) by SEQ_1:16;
A17: abs (Im (seq . n)) <= |.(seq . n).| by Th13;
|.(seq . n).| = |.z.| to_power (n + 1) by A3;
then (abs (Im seq)) . n <= |.z.| to_power (n + 1) by A16, A17, Def4;
hence (abs (Im seq)) . n <= rseq1 . n by A8; :: thesis: verum

end;

hence ( ( for n being Element of NAT holds C . n <= (abs (Im seq)) . n ) & ( for n being Element of NAT holds (abs (Im seq)) . n <= rseq1 . n ) ) by A15; :: thesis: verum

end;

A18: abs (Re seq) is convergent by A7, A9, A10, SEQ_2:33;
A19: lim (abs (Re seq)) = 0 by A7, A9, A10, SEQ_2:34;
A20: abs (Im seq) is convergent by A7, A9, A14, SEQ_2:33;
A21: lim (abs (Im seq)) = 0 by A7, A9, A14, SEQ_2:34;
A22: ( Re seq is convergent & lim (Re seq) = 0 ) by A18, A19, SEQ_4:28;
( Im seq is convergent & lim (Im seq) = 0 ) by A20, A21, SEQ_4:28;
then ( seq is convergent & Re (lim seq) = 0 & Im (lim seq) = 0 ) by A22, Th42;
hence ( seq is convergent & lim seq = 0c ) by Lm1, COMPLEX1:29; :: thesis: verum