let b be Nat; :: thesis: ( b > 1 implies ( powerfact b is summable & Sum (powerfact b) <= b / (b - 1) ) )

assume A1: b > 1 ; :: thesis: ( powerfact b is summable & Sum (powerfact b) <= b / (b - 1) )

then |.(1 / b).| < 1 / 1 by XREAL_1:76;

then A3: (1 / b) GeoSeq is summable by SERIES_1:24;

A2: for i being Nat holds 0 <= (powerfact b) . i

then Sum (powerfact b) <= Sum ((1 / b) GeoSeq) by A2, A3, SERIES_1:20;

hence ( powerfact b is summable & Sum (powerfact b) <= b / (b - 1) ) by Th13, A1, A2, A3, A4, SERIES_1:20; :: thesis: verum

assume A1: b > 1 ; :: thesis: ( powerfact b is summable & Sum (powerfact b) <= b / (b - 1) )

then |.(1 / b).| < 1 / 1 by XREAL_1:76;

then A3: (1 / b) GeoSeq is summable by SERIES_1:24;

A2: for i being Nat holds 0 <= (powerfact b) . i

proof

A4:
for i being Nat holds (powerfact b) . i <= ((1 / b) GeoSeq) . i
by A1, Th25;
let i be Nat; :: thesis: 0 <= (powerfact b) . i

(powerfact b) . i = 1 / (b to_power (i !)) by DefPower;

hence 0 <= (powerfact b) . i ; :: thesis: verum

end;(powerfact b) . i = 1 / (b to_power (i !)) by DefPower;

hence 0 <= (powerfact b) . i ; :: thesis: verum

then Sum (powerfact b) <= Sum ((1 / b) GeoSeq) by A2, A3, SERIES_1:20;

hence ( powerfact b is summable & Sum (powerfact b) <= b / (b - 1) ) by Th13, A1, A2, A3, A4, SERIES_1:20; :: thesis: verum