let n, m, b be Nat; ( n <> 0 & b > 1 & m < len (digits (n,b)) implies n >= b |^ m )
assume A1:
( n <> 0 & b > 1 & m < len (digits (n,b)) )
; n >= b |^ m
A2:
value ((digits (n,b)),b) = n
by A1, NUMERAL1:def 2;
len (digits (n,b)) > 0
by A1;
then A3:
len (digits (n,b)) >= 1
by NAT_1:14;
(digits (n,b)) . ((len (digits (n,b))) - 1) <> 0
by A1, NUMERAL1:def 2;
then A4:
(digits (n,b)) . ((len (digits (n,b))) - 1) >= 1
by NAT_1:14;
m + 1 <= len (digits (n,b))
by A1, NAT_1:13;
then
(m + 1) - 1 <= (len (digits (n,b))) - 1
by XREAL_1:9;
then
(len (digits (n,b))) -' 1 >= m
by A3, XREAL_1:233;
then A5:
b |^ ((len (digits (n,b))) -' 1) >= b |^ m
by A1, NAT_6:1;
for i being Nat st i in dom (digits (n,b)) holds
(digits (n,b)) . i < b
by A1, NUMERAL1:def 2;
then A6:
((digits (n,b)) . ((len (digits (n,b))) - 1)) * (b |^ ((len (digits (n,b))) -' 1)) <= n
by A1, A2, Th8;
b |^ ((len (digits (n,b))) -' 1) <= ((digits (n,b)) . ((len (digits (n,b))) - 1)) * (b |^ ((len (digits (n,b))) -' 1))
by A4, XREAL_1:151;
then
n >= b |^ ((len (digits (n,b))) -' 1)
by A6, XXREAL_0:2;
hence
n >= b |^ m
by A5, XXREAL_0:2; verum