let a be real number ; :: thesis: ( abs a < 1 implies ( a GeoSeq is summable & Sum (a GeoSeq ) = 1 / (1 - a) ) )
assume A1:
abs a < 1
; :: thesis: ( a GeoSeq is summable & Sum (a GeoSeq ) = 1 / (1 - a) )
deffunc H1( Element of NAT ) -> set = a to_power ($1 + 1);
consider s being Real_Sequence such that
A2:
for n being Element of NAT holds s . n = H1(n)
from SEQ_1:sch 1();
A3:
( s is convergent & lim s = 0 )
by A1, A2, Th3;
A4:
now let r be
real number ;
:: thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs (((Partial_Sums (a GeoSeq )) . n) - (1 / (1 - a))) < r )assume A5:
r > 0
;
:: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
abs (((Partial_Sums (a GeoSeq )) . n) - (1 / (1 - a))) < r
a < 1
by A1, SEQ_2:9;
then A6:
1
- a > 0
by XREAL_1:52;
then
r * (1 - a) > 0 * r
by A5, XREAL_1:70;
then consider m being
Element of
NAT such that A7:
for
n being
Element of
NAT st
n >= m holds
abs ((s . n) - 0 ) < r * (1 - a)
by A3, SEQ_2:def 7;
take m =
m;
:: thesis: for n being Element of NAT st n >= m holds
abs (((Partial_Sums (a GeoSeq )) . n) - (1 / (1 - a))) < rA8:
a <> 1
by A1, SEQ_2:9;
A9:
1
- a <> 0
by A1, SEQ_2:9;
let n be
Element of
NAT ;
:: thesis: ( n >= m implies abs (((Partial_Sums (a GeoSeq )) . n) - (1 / (1 - a))) < r )assume A10:
n >= m
;
:: thesis: abs (((Partial_Sums (a GeoSeq )) . n) - (1 / (1 - a))) < rA11:
abs (((Partial_Sums (a GeoSeq )) . n) - (1 / (1 - a))) =
abs (((1 - (a to_power (n + 1))) / (1 - a)) - (1 / (1 - a)))
by A8, Th26
.=
abs (((1 + (- (a to_power (n + 1)))) - 1) / (1 - a))
.=
abs (- ((a to_power (n + 1)) / (1 - a)))
.=
abs ((a to_power (n + 1)) / (1 - a))
by COMPLEX1:138
.=
(abs (a to_power (n + 1))) / (abs (1 - a))
by COMPLEX1:153
.=
(abs (a to_power (n + 1))) / (1 - a)
by A6, ABSVALUE:def 1
;
abs ((s . n) - 0 ) < r * (1 - a)
by A7, A10;
then
abs ((a to_power (n + 1)) - 0 ) < r * (1 - a)
by A2;
then
(abs (a to_power (n + 1))) / (1 - a) < (r * (1 - a)) / (1 - a)
by A6, XREAL_1:76;
hence
abs (((Partial_Sums (a GeoSeq )) . n) - (1 / (1 - a))) < r
by A9, A11, XCMPLX_1:90;
:: thesis: verum end;
then A12:
Partial_Sums (a GeoSeq ) is convergent
by SEQ_2:def 6;
hence
a GeoSeq is summable
by Def2; :: thesis: Sum (a GeoSeq ) = 1 / (1 - a)
thus
Sum (a GeoSeq ) = 1 / (1 - a)
by A4, A12, SEQ_2:def 7; :: thesis: verum