lt_base_pow_length_digits' — Mathlib

English

For any base b>1 and number m, m < b^{(digits b m).length}.

Русский

Для любой основы b>1 и числа m выполняется m < b^{(digits b m).length}.

LaTeX

$$$ m < b^{(\mathrm{digits}\; b\; m).\text{length}} $$$

Lean4

/-- Any number m is less than (b+2)^(number of digits in the base b + 2 representation of m) -/
theorem lt_base_pow_length_digits' {b m : ℕ} : m < (b + 2) ^ (digits (b + 2) m).length :=
  by
  convert @ofDigits_lt_base_pow_length' b (digits (b + 2) m) fun _ => digits_lt_base'
  rw [ofDigits_digits (b + 2) m]

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