mul_add_one_le_add_one_pow — Mathlib

English

If a ≥ 0, then a b + 1 ≤ (a+1)^b for all natural b.

Русский

Если a ≥ 0, то для любого натурального b выполняется a b + 1 ≤ (a+1)^b.

LaTeX

$$$0 \le a \Rightarrow \forall b \in \mathbb{N},\ ab+1 \le (a+1)^b$$$

Lean4

theorem mul_add_one_le_add_one_pow {a : ℝ} (ha : 0 ≤ a) (b : ℕ) : a * b + 1 ≤ (a + 1) ^ b :=
  by
  rcases ha.eq_or_lt with rfl | ha'
  · simp
  clear ha
  induction b generalizing a with
  | zero => simp
  | succ b hb =>
    calc
      a * ↑(b + 1) + 1 = (0 + 1) ^ b * a + (a * b + 1) := by simp [mul_add, add_assoc, add_left_comm]
      _ ≤ (a + 1) ^ b * a + (a + 1) ^ b := by
        gcongr
        · norm_num
        · exact hb ha'
      _ = (a + 1) ^ (b + 1) := by simp [pow_succ, mul_add]

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