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 that
A1: 0 < |.z.| and
A2: |.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 ) )
deffunc H₁( Element of NAT ) -> Element of REAL = |.z.| to_power ($1 + 1);
consider rseq1 being Real_Sequence such that
A3: for n being Element of NAT holds rseq1 . n = H₁(n) from SEQ_1:sch 1();
assume that
A4: seq . 0 = z and
A5: for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ; :: thesis: ( seq is convergent & lim seq = 0c )
A6: 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);
A7: 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 A8: S₁[k] ; :: thesis: S₁[k + 1]
|.(seq . (k + 1)).| = |.((seq . k) * z).| by A5
.= (|.z.| to_power (k + 1)) * |.z.| by A8, 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;

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

end;

A10: 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 A11: (abs (Re seq)) . n = abs (Re (seq . n)) by Def3;
( abs (Re (seq . n)) <= |.(seq . n).| & |.(seq . n).| = |.z.| to_power (n + 1) ) by A6, Th13;
hence (abs (Re seq)) . n <= rseq1 . n by A3, A11; :: thesis: verum

end;

A12: now

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

end;

C . 0 = 0 by FUNCOP_1:13;
then A14: lim C = 0 by SEQ_4:40;
A15: ( rseq1 is convergent & lim rseq1 = 0 ) by A1, A2, A3, SERIES_1:1;

now

let n be Element of NAT ; :: thesis: C . n <= (abs (Re seq)) . n
(abs (Re seq)) . n = abs ((Re seq) . n) by SEQ_1:16;
then 0 <= (abs (Re seq)) . n by COMPLEX1:132;
hence C . n <= (abs (Re seq)) . n by FUNCOP_1:13; :: thesis: verum

end;

then A16: ( abs (Re seq) is convergent & lim (abs (Re seq)) = 0 ) by A14, A15, A10, SEQ_2:33, SEQ_2:34;
then A17: Re seq is convergent by SEQ_4:28;

now

let n be Element of NAT ; :: thesis: C . n <= (abs (Im seq)) . n
(abs (Im seq)) . n = abs ((Im seq) . n) by SEQ_1:16;
then 0 <= (abs (Im seq)) . n by COMPLEX1:132;
hence C . n <= (abs (Im seq)) . n by FUNCOP_1:13; :: thesis: verum

end;

then A18: ( abs (Im seq) is convergent & lim (abs (Im seq)) = 0 ) by A14, A15, A12, SEQ_2:33, SEQ_2:34;
then A19: Im seq is convergent by SEQ_4:28;
lim (Im seq) = 0 by A18, SEQ_4:28;
then A20: Im (lim seq) = 0 by A17, A19, Th42;
lim (Re seq) = 0 by A16, SEQ_4:28;
then Re (lim seq) = 0 by A17, A19, Th42;
hence ( seq is convergent & lim seq = 0c ) by A17, A19, A20, Lm1, Th42, COMPLEX1:29; :: thesis: verum