theorem :: NUMBER19:17

for n, k, b being Nat st b > 1 & k > 0 & n > 0 holds
Sum (digits (((k * (b |^ n)) -' 1),b)) >= n * (b - 1)