base_pow_length_digits_le — Mathlib

English

If b > 1 and m ≠ 0, then b^{(digits b m).length} ≤ b · m.

Русский

Если b > 1 и m ≠ 0, то b^{(digits b m).length} ≤ b · m.

LaTeX

$$$ b^{(\mathrm{digits}(b, m)).\text{length}} \le b \cdot m $$$

Lean4

/-- Any non-zero natural number `m` is greater than
b^((number of digits in the base b representation of m) - 1)
-/
theorem base_pow_length_digits_le (b m : ℕ) (hb : 1 < b) : m ≠ 0 → b ^ (digits b m).length ≤ b * m :=
  by
  rcases b with (_ | _ | b) <;> try simp_all
  exact base_pow_length_digits_le' b m

Похожие утверждения