two_mul_sq_add_one_le_two_pow_two_mul

English

For every natural k, the inequality 2k^2 + 1 ≤ 2^{2k} holds.

Русский

Для каждого натурального k выполняется неравенство 2k^2 + 1 ≤ 2^{2k}.

LaTeX

$$$ 2k^{2} + 1 \le 2^{2k} $$$

Lean4

theorem two_mul_sq_add_one_le_two_pow_two_mul (k : ℕ) : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k) := by
  induction k with
  | zero => simp
  | succ k hk =>
    rw [add_pow_two, one_pow, mul_one, add_assoc, mul_add, add_right_comm]
    refine (add_le_add_right hk _).trans ?_
    rw [mul_add 2 k, pow_add, mul_one, pow_two, ← mul_assoc, mul_two, mul_two, add_assoc]
    gcongr
    rw [← two_mul, ← pow_succ']
    exact le_add_of_le_right (mul_le_pow (by simp) _)

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