let seq be Complex_Sequence; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 H₁( Nat) -> object = |.z.| to_power ($1 + 1);
consider rseq1 being Real_Sequence such that
A3: for n being Nat holds rseq1 . n = H₁(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 ; :: thesis: ( seq is convergent & lim seq = 0c )
A6: for n being Nat holds |.(seq . n).| = |.z.| to_power (n + 1)

proof

defpred S₁[ Nat] means |.(seq . $1).| = |.z.| to_power ($1 + 1);
A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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:65
.= (|.z.| to_power (k + 1)) * (|.z.| to_power 1) by POWER:25
.= |.z.| to_power ((k + 1) + 1) by A1, POWER:27 ;
hence S₁[k + 1] ; :: thesis: verum

end;

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

end;

A10: now :: thesis: for n being Nat holds (abs (Re seq)) . n <= rseq1 . n

let n be Nat; :: thesis: (abs (Re seq)) . n <= rseq1 . n
(abs (Re seq)) . n = |.((Re seq) . n).| by SEQ_1:12;
then A11: (abs (Re seq)) . n = |.(Re (seq . n)).| by Def5;
( |.(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 :: thesis: for n being Nat holds (abs (Im seq)) . n <= rseq1 . n

let n be Nat; :: thesis: (abs (Im seq)) . n <= rseq1 . n
A13: |.(seq . n).| = |.z.| to_power (n + 1) by A6;
( (abs (Im seq)) . n = |.((Im seq) . n).| & |.(Im (seq . n)).| <= |.(seq . n).| ) by Th13, SEQ_1:12;
then (abs (Im seq)) . n <= |.z.| to_power (n + 1) by A13, Def6;
hence (abs (Im seq)) . n <= rseq1 . n by A3; :: thesis: verum

end;

(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;

now :: thesis: for n being Nat holds (seq_const 0) . n <= (abs (Re seq)) . n

let n be Nat; :: thesis: (seq_const 0) . n <= (abs (Re seq)) . n
(abs (Re seq)) . n = |.((Re seq) . n).| by SEQ_1:12;
then 0 <= (abs (Re seq)) . n by COMPLEX1:46;
hence (seq_const 0) . n <= (abs (Re seq)) . n ; :: thesis: verum

end;

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;

now :: thesis: for n being Nat holds (seq_const 0) . n <= (abs (Im seq)) . n

let n be Nat; :: thesis: (seq_const 0) . n <= (abs (Im seq)) . n
(abs (Im seq)) . n = |.((Im seq) . n).| by SEQ_1:12;
then 0 <= (abs (Im seq)) . n by COMPLEX1:46;
hence (seq_const 0) . n <= (abs (Im seq)) . n ; :: thesis: verum

end;

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; :: thesis: verum