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
proof
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;
A4: for i being Nat holds (powerfact b) . i <= ((1 / b) GeoSeq) . i by A1, Th25;
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