let X be set ; :: thesis: for r being Real st 0 < r & r < 1 holds

X -powers r is summable

let r be Real; :: thesis: ( 0 < r & r < 1 implies X -powers r is summable )

assume that

A1: 0 < r and

A2: r < 1 ; :: thesis: X -powers r is summable

then r GeoSeq is summable by A2, SERIES_1:24;

hence X -powers r is summable by A4, A3, SERIES_1:19; :: thesis: verum

X -powers r is summable

let r be Real; :: thesis: ( 0 < r & r < 1 implies X -powers r is summable )

assume that

A1: 0 < r and

A2: r < 1 ; :: thesis: X -powers r is summable

A3: now :: thesis: for n being Nat holds 0 <= (X -powers r) . n

let n be Nat; :: thesis: 0 <= (X -powers r) . n

( ( n in X & (X -powers r) . n = r |^ n ) or ( not n in X & (X -powers r) . n = 0 ) ) by Def5;

hence 0 <= (X -powers r) . n by A1, PREPOWER:6; :: thesis: verum

end;( ( n in X & (X -powers r) . n = r |^ n ) or ( not n in X & (X -powers r) . n = 0 ) ) by Def5;

hence 0 <= (X -powers r) . n by A1, PREPOWER:6; :: thesis: verum

A4: now :: thesis: ex m being Nat st

for n being Nat st m <= n holds

(X -powers r) . n <= (r GeoSeq) . n

|.r.| = r
by A1, ABSVALUE:def 1;for n being Nat st m <= n holds

(X -powers r) . n <= (r GeoSeq) . n

reconsider m = 1 as Nat ;

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

(X -powers r) . n <= (r GeoSeq) . n

let n be Nat; :: thesis: ( m <= n implies (X -powers r) . n <= (r GeoSeq) . n )

assume m <= n ; :: thesis: (X -powers r) . n <= (r GeoSeq) . n

A5: (r GeoSeq) . n = r |^ n by PREPOWER:def 1;

( ( n in X & (X -powers r) . n = r |^ n ) or ( not n in X & (X -powers r) . n = 0 ) ) by Def5;

hence (X -powers r) . n <= (r GeoSeq) . n by A1, A5, PREPOWER:6; :: thesis: verum

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

(X -powers r) . n <= (r GeoSeq) . n

let n be Nat; :: thesis: ( m <= n implies (X -powers r) . n <= (r GeoSeq) . n )

assume m <= n ; :: thesis: (X -powers r) . n <= (r GeoSeq) . n

A5: (r GeoSeq) . n = r |^ n by PREPOWER:def 1;

( ( n in X & (X -powers r) . n = r |^ n ) or ( not n in X & (X -powers r) . n = 0 ) ) by Def5;

hence (X -powers r) . n <= (r GeoSeq) . n by A1, A5, PREPOWER:6; :: thesis: verum

then r GeoSeq is summable by A2, SERIES_1:24;

hence X -powers r is summable by A4, A3, SERIES_1:19; :: thesis: verum