nat_repr_len_aux — Mathlib

English

Let b, n, e be natural numbers with b > 0. If n < b^(e+1), then n div b < b^e.

Русский

Пусть b, n, e — естественные числа и b > 0. Если n < b^(e+1), то n div b < b^e.

LaTeX

$$$\\forall n,b,e \\in \\mathbb{N},\\ 0 < b \\implies n < b^{e+1} \\Rightarrow n \\operatorname{div} b < b^{e}$$$

Lean4

theorem nat_repr_len_aux (n b e : Nat) (h_b_pos : 0 < b) : n < b ^ e.succ → n / b < b ^ e :=
  by
  simp only [Nat.pow_succ]
  exact (@Nat.div_lt_iff_lt_mul b n (b ^ e) h_b_pos).mpr

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