fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq

English

F_{n+2} = F_{n+1}^2 − 2(F_n − 1)^2.

Русский

F_{n+2} = F_{n+1}^2 − 2(F_n − 1)^2.

LaTeX

$$$\\mathrm{fermatNumber}(n+2) = (\\mathrm{fermatNumber}(n+1))^2 - 2\\cdot(\\mathrm{fermatNumber}(n) - 1)^2$$$

Lean4

theorem fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq (n : ℕ) :
    fermatNumber (n + 2) = (fermatNumber (n + 1)) ^ 2 - 2 * (fermatNumber n - 1) ^ 2 :=
  by
  simp only [fermatNumber, add_sub_self_right]
  rw [← add_sub_self_right (2 ^ 2 ^ (n + 2) + 1) <| 2 * 2 ^ 2 ^ (n + 1)]
  ring_nf

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