let a be Real; :: thesis: ( |.a.| < 1 implies ( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) ) )

deffunc H_{1}( Nat) -> object = a to_power ($1 + 1);

consider s being Real_Sequence such that

A1: for n being Nat holds s . n = H_{1}(n)
from SEQ_1:sch 1();

assume A2: |.a.| < 1 ; :: thesis: ( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) )

then A3: ( s is convergent & lim s = 0 ) by A1, Th3;

hence a GeoSeq is summable ; :: thesis: Sum (a GeoSeq) = 1 / (1 - a)

thus Sum (a GeoSeq) = 1 / (1 - a) by A4, A9, SEQ_2:def 7; :: thesis: verum

deffunc H

consider s being Real_Sequence such that

A1: for n being Nat holds s . n = H

assume A2: |.a.| < 1 ; :: thesis: ( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) )

then A3: ( s is convergent & lim s = 0 ) by A1, Th3;

A4: now :: thesis: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

|.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r

then A9:
Partial_Sums (a GeoSeq) is convergent
by SEQ_2:def 6;ex m being Nat st

for n being Nat st n >= m holds

|.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r

a < 1
by A2, SEQ_2:1;

then A5: 1 - a > 0 by XREAL_1:50;

let r be Real; :: thesis: ( r > 0 implies ex m being Nat st

for n being Nat st n >= m holds

|.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r )

assume r > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

|.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r

then r * (1 - a) > 0 * r by A5;

then consider m being Nat such that

A6: for n being Nat st n >= m holds

|.((s . n) - 0).| < r * (1 - a) by A3, SEQ_2:def 7;

take m = m; :: thesis: for n being Nat st n >= m holds

|.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r

let n be Nat; :: thesis: ( n >= m implies |.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r )

assume n >= m ; :: thesis: |.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r

then |.((s . n) - 0).| < r * (1 - a) by A6;

then |.((a to_power (n + 1)) - 0).| < r * (1 - a) by A1;

then A7: |.(a to_power (n + 1)).| / (1 - a) < (r * (1 - a)) / (1 - a) by A5, XREAL_1:74;

a <> 1 by A2, SEQ_2:1;

then A8: |.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| = |.(((1 - (a to_power (n + 1))) / (1 - a)) - (1 / (1 - a))).| by Th22

.= |.(((1 + (- (a to_power (n + 1)))) - 1) / (1 - a)).|

.= |.(- ((a to_power (n + 1)) / (1 - a))).|

.= |.((a to_power (n + 1)) / (1 - a)).| by COMPLEX1:52

.= |.(a to_power (n + 1)).| / |.(1 - a).| by COMPLEX1:67

.= |.(a to_power (n + 1)).| / (1 - a) by A5, ABSVALUE:def 1 ;

1 - a <> 0 by A2, SEQ_2:1;

hence |.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r by A8, A7, XCMPLX_1:89; :: thesis: verum

end;then A5: 1 - a > 0 by XREAL_1:50;

let r be Real; :: thesis: ( r > 0 implies ex m being Nat st

for n being Nat st n >= m holds

|.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r )

assume r > 0 ; :: thesis: ex m being Nat st

for n being Nat st n >= m holds

|.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r

then r * (1 - a) > 0 * r by A5;

then consider m being Nat such that

A6: for n being Nat st n >= m holds

|.((s . n) - 0).| < r * (1 - a) by A3, SEQ_2:def 7;

take m = m; :: thesis: for n being Nat st n >= m holds

|.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r

let n be Nat; :: thesis: ( n >= m implies |.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r )

assume n >= m ; :: thesis: |.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r

then |.((s . n) - 0).| < r * (1 - a) by A6;

then |.((a to_power (n + 1)) - 0).| < r * (1 - a) by A1;

then A7: |.(a to_power (n + 1)).| / (1 - a) < (r * (1 - a)) / (1 - a) by A5, XREAL_1:74;

a <> 1 by A2, SEQ_2:1;

then A8: |.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| = |.(((1 - (a to_power (n + 1))) / (1 - a)) - (1 / (1 - a))).| by Th22

.= |.(((1 + (- (a to_power (n + 1)))) - 1) / (1 - a)).|

.= |.(- ((a to_power (n + 1)) / (1 - a))).|

.= |.((a to_power (n + 1)) / (1 - a)).| by COMPLEX1:52

.= |.(a to_power (n + 1)).| / |.(1 - a).| by COMPLEX1:67

.= |.(a to_power (n + 1)).| / (1 - a) by A5, ABSVALUE:def 1 ;

1 - a <> 0 by A2, SEQ_2:1;

hence |.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r by A8, A7, XCMPLX_1:89; :: thesis: verum

hence a GeoSeq is summable ; :: thesis: Sum (a GeoSeq) = 1 / (1 - a)

thus Sum (a GeoSeq) = 1 / (1 - a) by A4, A9, SEQ_2:def 7; :: thesis: verum