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;

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

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

then A6:
(r GeoSeq) ^\ n = (r |^ n) (#) (r GeoSeq)
by FUNCT_2:63;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;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

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