let n, b be Nat; :: thesis: ( b > 1 & n >= 1 implies Sum ((b - 1) (#) ((powerfact b) ^\ (n + 1))) < 1 / ((b to_power (n !)) to_power n) )
assume A0: ( b > 1 & n >= 1 ) ; :: thesis: Sum ((b - 1) (#) ((powerfact b) ^\ (n + 1))) < 1 / ((b to_power (n !)) to_power n)
then (powerfact b) ^\ (n + 1) is summable by Th26, SERIES_1:12;
then A2: Sum ((b - 1) (#) ((powerfact b) ^\ (n + 1))) = (b - 1) * (Sum ((powerfact b) ^\ (n + 1))) by SERIES_1:10;
1 < b - 0 by A0;
then A3: b - 1 > 0 by XREAL_1:12;
set s1 = (powerfact b) ^\ (n + 1);
set s2 = ((1 / b) GeoSeq) ^\ ((n + 1) !);
A4: |.(1 / b).| < 1 / 1 by A0, XREAL_1:76;
then A5: (1 / b) GeoSeq is summable by SERIES_1:24;
A6: for k being Nat holds
( 0 <= ((powerfact b) ^\ (n + 1)) . k & ((powerfact b) ^\ (n + 1)) . k <= (((1 / b) GeoSeq) ^\ ((n + 1) !)) . k )

proof

let k be Nat; :: thesis: ( 0 <= ((powerfact b) ^\ (n + 1)) . k & ((powerfact b) ^\ (n + 1)) . k <= (((1 / b) GeoSeq) ^\ ((n + 1) !)) . k )
A7: ((powerfact b) ^\ (n + 1)) . k = (powerfact b) . (k + (n + 1)) by NAT_1:def 3
.= 1 / (b to_power ((k + (n + 1)) !)) by DefPower ;
( k = 0 or k >= 1 + 0 ) by NAT_1:13;

per cases then ( k >= 1 or k = 0 ) ;

suppose A8: k >= 1 ; :: thesis: ( 0 <= ((powerfact b) ^\ (n + 1)) . k & ((powerfact b) ^\ (n + 1)) . k <= (((1 / b) GeoSeq) ^\ ((n + 1) !)) . k )

A9: (((1 / b) GeoSeq) ^\ ((n + 1) !)) . k = ((1 / b) GeoSeq) . (k + ((n + 1) !)) by NAT_1:def 3
.= (1 / b) |^ (k + ((n + 1) !)) by PREPOWER:def 1
.= 1 / (b |^ (k + ((n + 1) !))) by PREPOWER:7 ;
n + 1 >= 1 by A0, NAT_1:16;
then b to_power (k + ((n + 1) !)) <= b to_power ((k + (n + 1)) !) by PRE_FF:8, A0, Th8, A8;
then (b |^ (k + ((n + 1) !))) " >= (b |^ ((k + (n + 1)) !)) " by A0, XREAL_1:85;
then 1 / (b |^ (k + ((n + 1) !))) >= (b |^ ((k + (n + 1)) !)) " by XCMPLX_1:215;
hence ( 0 <= ((powerfact b) ^\ (n + 1)) . k & ((powerfact b) ^\ (n + 1)) . k <= (((1 / b) GeoSeq) ^\ ((n + 1) !)) . k ) by A7, A9, XCMPLX_1:215; :: thesis: verum

end;

suppose A10: k = 0 ; :: thesis: ( 0 <= ((powerfact b) ^\ (n + 1)) . k & ((powerfact b) ^\ (n + 1)) . k <= (((1 / b) GeoSeq) ^\ ((n + 1) !)) . k )

then A11: ((powerfact b) ^\ (n + 1)) . k = (powerfact b) . (0 + (n + 1)) by NAT_1:def 3
.= 1 / (b to_power ((n + 1) !)) by DefPower ;
hence ((powerfact b) ^\ (n + 1)) . k >= 0 ; :: thesis: ((powerfact b) ^\ (n + 1)) . k <= (((1 / b) GeoSeq) ^\ ((n + 1) !)) . k
(((1 / b) GeoSeq) ^\ ((n + 1) !)) . k = ((1 / b) GeoSeq) . (0 + ((n + 1) !)) by NAT_1:def 3, A10
.= (1 / b) |^ (0 + ((n + 1) !)) by PREPOWER:def 1
.= 1 / (b |^ (0 + ((n + 1) !))) by PREPOWER:7 ;
hence ((powerfact b) ^\ (n + 1)) . k <= (((1 / b) GeoSeq) ^\ ((n + 1) !)) . k by A11; :: thesis: verum

end;

end;

end;

A12: ((1 / b) GeoSeq) ^\ ((n + 1) !) is summable by A4, SERIES_1:12, SERIES_1:24;
ex k being Nat st
( 1 <= k & ((powerfact b) ^\ (n + 1)) . k < (((1 / b) GeoSeq) ^\ ((n + 1) !)) . k )

proof

take k = 2; :: thesis: ( 1 <= k & ((powerfact b) ^\ (n + 1)) . k < (((1 / b) GeoSeq) ^\ ((n + 1) !)) . k )
A13: ((powerfact b) ^\ (n + 1)) . k = (powerfact b) . (k + (n + 1)) by NAT_1:def 3
.= 1 / (b to_power ((k + (n + 1)) !)) by DefPower ;
A14: (((1 / b) GeoSeq) ^\ ((n + 1) !)) . k = ((1 / b) GeoSeq) . (k + ((n + 1) !)) by NAT_1:def 3
.= (1 / b) |^ (k + ((n + 1) !)) by PREPOWER:def 1
.= 1 / (b |^ (k + ((n + 1) !))) by PREPOWER:7 ;
n + 1 > 0 + 1 by A0, XREAL_1:8;
then b to_power (k + ((n + 1) !)) < b to_power ((k + (n + 1)) !) by POWER:39, A0, Th6;
then (b |^ (k + ((n + 1) !))) " > (b |^ ((k + (n + 1)) !)) " by A0, XREAL_1:88;
then 1 / (b |^ (k + ((n + 1) !))) > (b |^ ((k + (n + 1)) !)) " by XCMPLX_1:215;
hence ( 1 <= k & ((powerfact b) ^\ (n + 1)) . k < (((1 / b) GeoSeq) ^\ ((n + 1) !)) . k ) by A13, A14, XCMPLX_1:215; :: thesis: verum

end;

then Sum ((powerfact b) ^\ (n + 1)) < Sum (((1 / b) GeoSeq) ^\ ((n + 1) !)) by A6, A12, Th11;
then A15: (b - 1) * (Sum ((powerfact b) ^\ (n + 1))) < (b - 1) * (Sum (((1 / b) GeoSeq) ^\ ((n + 1) !))) by XREAL_1:68, A3;
reconsider bn = b |^ ((n + 1) !) as Nat ;
A16: ((1 / b) GeoSeq) ^\ ((n + 1) !) = (1 / bn) (#) ((1 / b) GeoSeq)

proof

now :: thesis: for i being Element of NAT holds (((1 / b) GeoSeq) ^\ ((n + 1) !)) . i = ((1 / (b |^ ((n + 1) !))) (#) ((1 / b) GeoSeq)) . i

let i be Element of NAT ; :: thesis: (((1 / b) GeoSeq) ^\ ((n + 1) !)) . i = ((1 / (b |^ ((n + 1) !))) (#) ((1 / b) GeoSeq)) . i
thus (((1 / b) GeoSeq) ^\ ((n + 1) !)) . i = ((1 / b) GeoSeq) . (i + ((n + 1) !)) by NAT_1:def 3
.= (1 / b) |^ (i + ((n + 1) !)) by PREPOWER:def 1
.= ((1 / b) |^ i) * ((1 / b) |^ ((n + 1) !)) by NEWTON:8
.= ((1 / b) |^ i) * (1 / (b |^ ((n + 1) !))) by PREPOWER:7
.= (1 / (b |^ ((n + 1) !))) * (((1 / b) GeoSeq) . i) by PREPOWER:def 1
.= ((1 / (b |^ ((n + 1) !))) (#) ((1 / b) GeoSeq)) . i by VALUED_1:6 ; :: thesis: verum

end;

hence ((1 / b) GeoSeq) ^\ ((n + 1) !) = (1 / bn) (#) ((1 / b) GeoSeq) by FUNCT_2:63; :: thesis: verum

end;

Sum (((1 / b) GeoSeq) ^\ ((n + 1) !)) = (1 / (b |^ ((n + 1) !))) * (Sum ((1 / b) GeoSeq)) by A16, A5, SERIES_1:10
.= (1 / (b |^ ((n + 1) !))) * (b / (b - 1)) by Th13, A0
.= (1 * b) / ((b |^ ((n + 1) !)) * (b - 1)) by XCMPLX_1:76
.= b / ((b |^ ((n + 1) !)) * (b - 1)) ;
then A17: (b - 1) * (Sum (((1 / b) GeoSeq) ^\ ((n + 1) !))) = (b - 1) * ((b / bn) / (b - 1)) by XCMPLX_1:78
.= ((b - 1) * (b / bn)) / (b - 1) by XCMPLX_1:74
.= b / (b |^ ((n + 1) !)) by A3, XCMPLX_1:89 ;
n ! >= 1 by Th2;
then A18: b / (b |^ ((n + 1) !)) <= (b |^ (n !)) / (b |^ ((n + 1) !)) by XREAL_1:72, A0, PREPOWER:12;
(b |^ (n !)) / (b |^ ((n + 1) !)) = (b to_power (n !)) / (b to_power ((n + 1) !))
.= b to_power ((n !) - ((n + 1) !)) by POWER:29, A0
.= b to_power (- (((n + 1) !) - (n !)))
.= b to_power (- (n * (n !))) by Th3
.= 1 / (b to_power (n * (n !))) by POWER:28, A0
.= 1 / ((b to_power (n !)) to_power n) by POWER:33, A0 ;
hence Sum ((b - 1) (#) ((powerfact b) ^\ (n + 1))) < 1 / ((b to_power (n !)) to_power n) by A2, A15, XXREAL_0:2, A17, A18; :: thesis: verum