two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq

English

For all n, 2(F_n − 1)^2 ≤ (F_{n+1})^2.

Русский

Для всех n верно 2(F_n − 1)^2 ≤ (F_{n+1})^2.

LaTeX

$$$2\\,(\\mathrm{fermatNumber}(n) - 1)^2 \\le (\\mathrm{fermatNumber}(n+1))^2$$$

Lean4

theorem two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq (n : ℕ) :
    2 * (fermatNumber n - 1) ^ 2 ≤ (fermatNumber (n + 1)) ^ 2 :=
  by
  simp only [fermatNumber, add_tsub_cancel_right]
  have : 0 ≤ 1 + 2 ^ (2 ^ n * 4) := le_add_left _ _
  ring_nf
  cutsat

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