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

Sum (X -powers r) <= Sum (r GeoSeq)

let X be set ; :: thesis: ( 0 < r & r < 1 implies Sum (X -powers r) <= Sum (r GeoSeq) )

assume that

A1: 0 < r and

A2: r < 1 ; :: thesis: Sum (X -powers r) <= Sum (r GeoSeq)

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

hence Sum (X -powers r) <= Sum (r GeoSeq) by A3, SERIES_1:20; :: thesis: verum

Sum (X -powers r) <= Sum (r GeoSeq)

let X be set ; :: thesis: ( 0 < r & r < 1 implies Sum (X -powers r) <= Sum (r GeoSeq) )

assume that

A1: 0 < r and

A2: r < 1 ; :: thesis: Sum (X -powers r) <= Sum (r GeoSeq)

A3: now :: thesis: for n being Nat holds

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

|.r.| = r
by A1, ABSVALUE:def 1;( 0 <= (X -powers r) . n & (X -powers r) . n <= (r GeoSeq) . n )

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

A4: ( ( 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: (X -powers r) . n <= (r GeoSeq) . n

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

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

end;A4: ( ( 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: (X -powers r) . n <= (r GeoSeq) . n

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

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

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

hence Sum (X -powers r) <= Sum (r GeoSeq) by A3, SERIES_1:20; :: thesis: verum