English
For base b>1 and n, (b.digits n).length ≤ k iff n < b^k.
Русский
Для основания b>1 и n: длина (b.digits n) ≤ k тогда и только тогда, когда n < b^k.
LaTeX
$$$\\forall {b k : \\mathbb{N}},\\ 1 < b \\Rightarrow \\mathrm{length}(b.digits\\; n) \\le k \\iff n < b^k$$$
Lean4
theorem digits_len (b n : ℕ) (hb : 1 < b) (hn : n ≠ 0) : (b.digits n).length = b.log n + 1 :=
by
induction n using Nat.strong_induction_on with
| _ n IH
rw [digits_eq_cons_digits_div hb hn, List.length]
by_cases h : n / b = 0
· simp [h]
aesop
· have : n / b < n := div_lt_self (Nat.pos_of_ne_zero hn) hb
rw [IH _ this h, log_div_base, tsub_add_cancel_of_le]
refine Nat.succ_le_of_lt (log_pos hb ?_)
contrapose! h
exact div_eq_of_lt h
