let seq be Complex_Sequence; :: thesis: for z being Complex st |.z.| < 1 & ( for n being Nat holds seq . (n + 1) = z * (seq . n) ) holds
( seq is summable & Sum seq = (seq . 0) / (1r - z) )
let z be Complex; :: thesis: ( |.z.| < 1 & ( for n being Nat holds seq . (n + 1) = z * (seq . n) ) implies ( seq is summable & Sum seq = (seq . 0) / (1r - z) ) )
assume that
A1: |.z.| < 1 and
A2: for n being Nat holds seq . (n + 1) = z * (seq . n) ; :: thesis: ( seq is summable & Sum seq = (seq . 0) / (1r - z) )
now :: thesis: for n being Element of NAT holds (Partial_Sums seq) . n = ((seq . 0) (#) (Partial_Sums (z GeoSeq))) . n
let n be Element of NAT ; :: thesis: (Partial_Sums seq) . n = ((seq . 0) (#) (Partial_Sums (z GeoSeq))) . n
thus (Partial_Sums seq) . n = (seq . 0) * ((1r - (z |^ (n + 1))) / (1r - z)) by A1, A2, Th37, COMPLEX1:48
.= (seq . 0) * ((Partial_Sums (z GeoSeq)) . n) by A1, Th36, COMPLEX1:48
.= ((seq . 0) (#) (Partial_Sums (z GeoSeq))) . n by VALUED_1:6 ; :: thesis: verum
end;
then A3: Partial_Sums seq = (seq . 0) (#) (Partial_Sums (z GeoSeq)) ;
A4: z GeoSeq is summable by A1, Th64;
hence seq is summable by A3; :: thesis: Sum seq = (seq . 0) / (1r - z)
Sum seq = (seq . 0) * (Sum (z GeoSeq)) by A3, A4, COMSEQ_2:18
.= (seq . 0) * (1r / (1r - z)) by A1, Th64
.= ((seq . 0) * 1r) / (1r - z) by XCMPLX_1:74
.= (seq . 0) / (1r - z) by COMPLEX1:def 4 ;
hence Sum seq = (seq . 0) / (1r - z) ; :: thesis: verum