let seq be Complex_Sequence; :: thesis: for z being Complex st |.z.| < 1 & ( for n being Nat holds seq . n = z |^ (n + 1) ) holds
( seq is convergent & lim seq = 0c )
let z be Complex; :: thesis: ( |.z.| < 1 & ( for n being Nat holds seq . n = z |^ (n + 1) ) implies ( seq is convergent & lim seq = 0c ) )
assume that
A1: |.z.| < 1 and
A2: for n being Nat holds seq . n = z |^ (n + 1) ; :: thesis: ( seq is convergent & lim seq = 0c )
A3: now :: thesis: for n being Nat holds seq . (n + 1) = (seq . n) * z
let n be Nat; :: thesis: seq . (n + 1) = (seq . n) * z
thus seq . (n + 1) = z |^ ((n + 1) + 1) by A2
.= (z |^ (n + 1)) * z by NEWTON:6
.= (seq . n) * z by A2 ; :: thesis: verum
end;
A4: now :: thesis: ( |.z.| = 0 implies ( seq is convergent & seq is convergent & lim seq = 0c ) )
assume |.z.| = 0 ; :: thesis: ( seq is convergent & seq is convergent & lim seq = 0c )
then A5: z = 0c by COMPLEX1:45;
A6: now :: thesis: for n being Nat holds seq . n = 0c
let n be Nat; :: thesis: seq . n = 0c
thus seq . n = 0c |^ (n + 1) by A2, A5
.= ((0c GeoSeq) . n) * 0c by Def1
.= 0c ; :: thesis: verum
end;
hence seq is convergent by COMSEQ_2:9; :: thesis: ( seq is convergent & lim seq = 0c )
thus ( seq is convergent & lim seq = 0c ) by A6, COMSEQ_2:9, COMSEQ_2:10; :: thesis: verum
end;
A7: seq . 0 = z |^ (0 + 1) by A2
.= z ;
now :: thesis: ( |.z.| <> 0 implies ( seq is convergent & lim seq = 0c ) )
A8: 0 <= |.z.| by COMPLEX1:46;
assume |.z.| <> 0 ; :: thesis: ( seq is convergent & lim seq = 0c )
hence ( seq is convergent & lim seq = 0c ) by A1, A7, A3, A8, Th43; :: thesis: verum
end;
hence ( seq is convergent & lim seq = 0c ) by A4; :: thesis: verum