let f be Real_Sequence; :: thesis: for a, r being positive real number st r < 1 & ( for n being natural number holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( f is convergent & ( for n being natural number holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) )
let a, r be positive real number ; :: thesis: ( r < 1 & ( for n being natural number holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) implies ( f is convergent & ( for n being natural number holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) )
assume A1: r < 1 ; :: thesis: ( ex n being natural number st not |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) or ( f is convergent & ( for n being natural number holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) )
assume A2: for n being natural number holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ; :: thesis: ( f is convergent & ( for n being natural number holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) )
deffunc H₁( Nat, Real) -> Element of REAL = (f . ($1 + 1)) - (f . $1);
consider g being Function of NAT ,REAL such that
A3: ( g . 0 = f . 0 & ( for n being Nat holds g . (n + 1) = H₁(n,g . n) ) ) from NAT_1:sch 12();

now

let n be Element of NAT ; :: thesis: f . (n + 1) = (f . n) + (g . (n + 1))
thus f . (n + 1) = ((f . (n + 1)) - (f . n)) + (f . n)
.= (f . n) + (g . (n + 1)) by A3 ; :: thesis: verum

end;

then A4: f = Partial_Sums g by A3, SERIES_1:def 1;
A5: |.r.| = r by COMPLEX1:129;
then A6: r GeoSeq is summable by A1, SERIES_1:28;
then A7: (a * (r " )) (#) (r GeoSeq ) is summable by SERIES_1:13;

A8: now

let n be Element of NAT ; :: thesis: 0 <= (abs g) . n
(abs g) . n = abs (g . n) by SEQ_1:16;
hence 0 <= (abs g) . n by COMPLEX1:132; :: thesis: verum

end;

now

set m = 1;
let n be Element of NAT ; :: thesis: ( 1 <= n implies (abs g) . n <= ((a * (r " )) (#) (r GeoSeq )) . n )
assume 1 <= n ; :: thesis: (abs g) . n <= ((a * (r " )) (#) (r GeoSeq )) . n
then consider k being Nat such that
A9: n = 1 + k by NAT_1:10;
g . n = H₁(k,g . k) by A3, A9;
then (abs g) . n = |.((f . n) - (f . k)).| by A9, SEQ_1:16
.= |.((f . k) - (f . n)).| by COMPLEX1:146 ;
then A10: (abs g) . n <= a * (r to_power k) by A2, A9;
(a * 1) * (r to_power k) = (a * ((r " ) * r)) * (r to_power k) by XCMPLX_0:def 7
.= (a * (r " )) * (r * (r to_power k))
.= (a * (r " )) * ((r to_power 1) * (r to_power k)) by POWER:30
.= (a * (r " )) * (r to_power n) by A9, POWER:32
.= (a * (r " )) * (r |^ n) by POWER:46
.= (a * (r " )) * ((r GeoSeq ) . n) by PREPOWER:def 1 ;
hence (abs g) . n <= ((a * (r " )) (#) (r GeoSeq )) . n by A10, SEQ_1:13; :: thesis: verum

end;

then abs g is summable by A7, A8, SERIES_1:22;
then A11: g is absolutely_summable by SERIES_1:def 5;
then g is summable by SERIES_1:40;
hence f is convergent by A4, SERIES_1:def 2; :: thesis: for n being natural number holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r)
let n be natural number ; :: thesis: |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r)
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
lim f = Sum g by A4, SERIES_1:def 3;
then A12: lim f = (f . n) + (Sum (g ^\ (n' + 1))) by A4, A11, SERIES_1:18, SERIES_1:40;
A13: (a * (r to_power n)) (#) (r GeoSeq ) is summable by A6, SERIES_1:13;

now

let k be Element of NAT ; :: thesis: ( 0 <= (abs (g ^\ (n' + 1))) . k & (abs (g ^\ (n' + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq )) . k )
(abs (g ^\ (n' + 1))) . k = |.((g ^\ (n' + 1)) . k).| by SEQ_1:16;
hence 0 <= (abs (g ^\ (n' + 1))) . k by COMPLEX1:132; :: thesis: (abs (g ^\ (n' + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq )) . k
(abs (g ^\ (n' + 1))) . k = |.((g ^\ (n' + 1)) . k).| by SEQ_1:16
.= |.(g . ((n' + 1) + k)).| by NAT_1:def 3
.= |.((f . ((n' + k) + 1)) - (f . (n' + k))).| by A3
.= |.((f . (n' + k)) - (f . ((n' + k) + 1))).| by UNIFORM1:13 ;
then (abs (g ^\ (n' + 1))) . k <= a * (r to_power (n' + k)) by A2;
then (abs (g ^\ (n' + 1))) . k <= a * ((r to_power n') * (r to_power k)) by POWER:32;
then (abs (g ^\ (n' + 1))) . k <= (a * (r to_power n')) * (r to_power k) ;
then (abs (g ^\ (n' + 1))) . k <= (a * (r to_power n')) * (r |^ k) by POWER:46;
then (abs (g ^\ (n' + 1))) . k <= (a * (r to_power n')) * ((r GeoSeq ) . k) by PREPOWER:def 1;
hence (abs (g ^\ (n' + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq )) . k by SEQ_1:13; :: thesis: verum

end;

then A14: ( Sum (abs (g ^\ (n' + 1))) <= Sum ((a * (r to_power n)) (#) (r GeoSeq )) & abs (g ^\ (n' + 1)) is summable ) by A13, SERIES_1:24;
then A15: ( Sum (abs (g ^\ (n' + 1))) <= Sum ((a * (r to_power n)) (#) (r GeoSeq )) & g ^\ (n' + 1) is absolutely_summable ) by SERIES_1:def 5;
A16: Sum ((a * (r to_power n)) (#) (r GeoSeq )) = (a * (r to_power n)) * (Sum (r GeoSeq )) by A6, SERIES_1:13
.= (a * (r to_power n)) * (1 / (1 - r)) by A1, A5, SERIES_1:28
.= (a * (r to_power n)) / (1 - r) by XCMPLX_1:100 ;
|.((lim f) - (f . n)).| <= Sum (abs (g ^\ (n' + 1))) by A12, A15, Th8;
hence |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) by A14, A16, XXREAL_0:2; :: thesis: verum