let r be Real; :: thesis: for n being Element of NAT st 0 < r & r < 1 holds
Sum ((r GeoSeq) ^\ n) = (r |^ n) / (1 - r)
let n be Element of NAT ; :: thesis: ( 0 < r & r < 1 implies Sum ((r GeoSeq) ^\ n) = (r |^ n) / (1 - r) )
assume that
A1: 0 < r and
A2: r < 1 ; :: thesis: Sum ((r GeoSeq) ^\ n) = (r |^ n) / (1 - r)
A3: |.r.| = r by A1, ABSVALUE:def 1;
then A4: r GeoSeq is summable by A2, SERIES_1:24;
A5: dom ((r |^ n) (#) (r GeoSeq)) = NAT by FUNCT_2:def 1;
now :: thesis: for i being Element of NAT holds ((r GeoSeq) ^\ n) . i = ((r |^ n) (#) (r GeoSeq)) . i
let i be Element of NAT ; :: thesis: ((r GeoSeq) ^\ n) . i = ((r |^ n) (#) (r GeoSeq)) . i
thus ((r GeoSeq) ^\ n) . i = (r GeoSeq) . (i + n) by NAT_1:def 3
.= r |^ (i + n) by PREPOWER:def 1
.= (r |^ n) * (r |^ i) by NEWTON:8
.= (r |^ n) * ((r GeoSeq) . i) by PREPOWER:def 1
.= ((r |^ n) (#) (r GeoSeq)) . i by A5, VALUED_1:def 5 ; :: thesis: verum
end;
then A6: (r GeoSeq) ^\ n = (r |^ n) (#) (r GeoSeq) by FUNCT_2:63;
Sum (r GeoSeq) = 1 / (1 - r) by A3, A2, SERIES_1:24;
hence Sum ((r GeoSeq) ^\ n) = (r |^ n) * (1 / (1 - r)) by A4, A6, SERIES_1:10
.= ((r |^ n) * 1) / (1 - r) by XCMPLX_1:74
.= (r |^ n) / (1 - r) ;
:: thesis: verum