English
If digits are bounded by b+2, then the value of ofDigits(b+2,l) is less than (b+2)^{|l|}.
Русский
Если цифры ограничены b+2, то значение ofDigits(b+2,l) меньше (b+2)^{|l|}.
LaTeX
$$$ \forall \; l:\mathrm{List}\ \mathbb{N},\ (\forall x\in l,\ x < b+2)\Rightarrow \mathrm{ofDigits}(b+2,l) < (b+2)^{|l|} $$$
Lean4
/-- an n-digit number in base b + 2 is less than (b + 2)^n -/
theorem ofDigits_lt_base_pow_length' {b : ℕ} {l : List ℕ} (hl : ∀ x ∈ l, x < b + 2) :
ofDigits (b + 2) l < (b + 2) ^ l.length := by
induction l with
| nil => simp [ofDigits]
| cons hd tl IH =>
rw [ofDigits, List.length_cons, pow_succ]
have : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2) :=
mul_le_mul (IH fun x hx => hl _ (List.mem_cons_of_mem _ hx)) (by rfl) (by simp only [zero_le]) (Nat.zero_le _)
suffices ↑hd < b + 2 by linarith
exact hl hd List.mem_cons_self
