let n, k, b be Nat; :: thesis: ( b > 1 & k > 0 & n > 0 implies Sum (digits (((k * (b |^ n)) -' 1),b)) >= n * (b - 1) )
assume A1: ( b > 1 & k > 0 & n > 0 ) ; :: thesis: Sum (digits (((k * (b |^ n)) -' 1),b)) >= n * (b - 1)
set D = digits ((k -' 1),b);
set V = (n --> (b -' 1)) ^ (digits ((k -' 1),b));
k * (b |^ n) >= 1 + 0 by A1, NAT_1:13;
then A2: ( value (((n --> (b -' 1)) ^ (digits ((k -' 1),b))),b) = (k * (b |^ n)) - 1 & (k * (b |^ n)) - 1 = (k * (b |^ n)) -' 1 ) by A1, Th16, XREAL_1:233;
A3: k >= 1 + 0 by A1, NAT_1:13;
then A4: k -' 1 = k - 1 by XREAL_1:233;
A5: n >= 1 + 0 by A1, NAT_1:13;
then b |^ n >= b by A1, PREPOWER:12;
then A6: ( b |^ n > 1 & 0 + 1 <= k ) by A1, NAT_1:13, XXREAL_0:2;
then A7: k * (b |^ n) >= 1 * (b |^ n) by XREAL_1:64;
A8: (k * (b |^ n)) - 1 = (k * (b |^ n)) -' 1 by A7, A6, XXREAL_0:2, XREAL_1:233;
A9: b -' 1 = b - 1 by A1, XREAL_1:233;
then (b -' 1) + 1 = b ;
then A10: b -' 1 < b by NAT_1:13;
A11: len (n --> (b -' 1)) = n ;

per cases ( k = 1 or k > 1 ) by A3, XXREAL_0:1;

suppose k = 1 ; :: thesis: Sum (digits (((k * (b |^ n)) -' 1),b)) >= n * (b - 1)

then A12: digits (((k * (b |^ n)) -' 1),b) = digits ((value ((n --> (b -' 1)),b)),b) by A8, A1, NUMBER11:7;
set N = n --> (b -' 1);
A13: for i being Nat st i in dom (n --> (b -' 1)) holds
(n --> (b -' 1)) . i < b by A10, FUNCOP_1:7;
A14: n - 1 = n -' 1 by A5, XREAL_1:233;
then ( n -' 1 < (n -' 1) + 1 & (n -' 1) + 1 = n ) by NAT_1:13;
then ( n -' 1 in Segm n & Segm n = n ) by NAT_1:44, ORDINAL1:def 17;
then (n --> (b -' 1)) . ((len (n --> (b -' 1))) - 1) = b -' 1 by A14, FUNCOP_1:7;
then ( len (n --> (b -' 1)) > 0 & (n --> (b -' 1)) . ((len (n --> (b -' 1))) - 1) <> 0 & ( for i being Nat st i in dom (n --> (b -' 1)) holds
(n --> (b -' 1)) . i < b ) ) by A13, A1, A9;
then digits ((value ((n --> (b -' 1)),b)),b) = n --> (b -' 1) by NUMBER11:5, A1;
hence Sum (digits (((k * (b |^ n)) -' 1),b)) >= n * (b - 1) by A9, A12, AFINSQ_2:58; :: thesis: verum

end;

suppose A15: k > 1 ; :: thesis: Sum (digits (((k * (b |^ n)) -' 1),b)) >= n * (b - 1)

A16: k -' 1 <> 0 by A4, A15;
A17: len (digits ((k -' 1),b)) >= 1 by A1, NUMERAL1:4;
A18: len ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) = (len (n --> (b -' 1))) + (len (digits ((k -' 1),b))) by AFINSQ_1:17;
len ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) >= (len (n --> (b -' 1))) + 1 by A18, A17, XREAL_1:6;
then A19: (len ((n --> (b -' 1)) ^ (digits ((k -' 1),b)))) - 1 >= ((len (n --> (b -' 1))) + 1) - 1 by XREAL_1:9;
(len ((n --> (b -' 1)) ^ (digits ((k -' 1),b)))) - 0 > (len ((n --> (b -' 1)) ^ (digits ((k -' 1),b)))) - 1 by XREAL_1:10;
then ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) . ((len ((n --> (b -' 1)) ^ (digits ((k -' 1),b)))) - 1) = (digits ((k -' 1),b)) . (((len ((n --> (b -' 1)) ^ (digits ((k -' 1),b)))) - 1) - n) by AFINSQ_1:18, A18, A19;
then A20: ( ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) . ((len ((n --> (b -' 1)) ^ (digits ((k -' 1),b)))) - 1) = (digits ((k -' 1),b)) . ((len (digits ((k -' 1),b))) - 1) & (digits ((k -' 1),b)) . ((len (digits ((k -' 1),b))) - 1) <> 0 ) by A18, A16, A1, NUMERAL1:def 2;
A21: for i being Nat st i in dom ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) holds
((n --> (b -' 1)) ^ (digits ((k -' 1),b))) . i < b

proof

let i be Nat; :: thesis: ( i in dom ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) implies ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) . i < b )
assume i in dom ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) ; :: thesis: ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) . i < b

per cases then ( i in dom (n --> (b -' 1)) or ex m being Nat st
( m in dom (digits ((k -' 1),b)) & i = n + m ) ) by AFINSQ_1:20;

suppose A22: i in dom (n --> (b -' 1)) ; :: thesis: ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) . i < b

then ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) . i = (n --> (b -' 1)) . i by AFINSQ_1:def 3;
hence ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) . i < b by A10, A22, FUNCOP_1:7; :: thesis: verum

end;

suppose ex m being Nat st
( m in dom (digits ((k -' 1),b)) & i = n + m ) ; :: thesis: ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) . i < b

then consider m being Nat such that
A23: ( m in dom (digits ((k -' 1),b)) & i = n + m ) ;
(digits ((k -' 1),b)) . m < b by A16, A23, A1, NUMERAL1:def 2;
hence ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) . i < b by A23, A11, AFINSQ_1:def 3; :: thesis: verum

end;

end;

end;

Sum (n --> (b -' 1)) = n * (b -' 1) by AFINSQ_2:58;
then ( Sum ((n --> (b -' 1)) ^ (digits ((k -' 1),b))) = (Sum (n --> (b -' 1))) + (Sum (digits ((k -' 1),b))) & (Sum (n --> (b -' 1))) + (Sum (digits ((k -' 1),b))) >= (n * (b -' 1)) + 0 ) by XREAL_1:6, AFINSQ_2:55;
hence Sum (digits (((k * (b |^ n)) -' 1),b)) >= n * (b - 1) by A21, A9, A2, A20, A1, NUMBER11:5; :: thesis: verum

end;

end;