base_pow_length_digits_le' — Mathlib

English

For any natural numbers b and m with m ≠ 0, the base a = b + 2 satisfies a^{(digits(a) m).length} ≤ a · m.

Русский

Для любых натуральных b и m с m ≠ 0 выполняется (b+2)^{(digits(b+2) m).length} ≤ (b+2) · m.

LaTeX

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

Lean4

/-- Any non-zero natural number `m` is greater than
(b+2)^((number of digits in the base (b+2) representation of m) - 1)
-/
theorem base_pow_length_digits_le' (b m : ℕ) (hm : m ≠ 0) : (b + 2) ^ (digits (b + 2) m).length ≤ (b + 2) * m :=
  by
  have : digits (b + 2) m ≠ [] := digits_ne_nil_iff_ne_zero.mpr hm
  convert @pow_length_le_mul_ofDigits b (digits (b + 2) m) this (getLast_digit_ne_zero _ hm)
  rw [ofDigits_digits]

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