fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq

English

The same recurrence holds in integers: F_{n+2} = F_{n+1}^2 − 2(F_n − 1)^2, interpreted in Z.

Русский

Та же формула выполняется в целых числах: F_{n+2} = F_{n+1}^2 − 2(F_n − 1)^2, в трактовке в Z.

LaTeX

$$$\\operatorname{fermatNumber}(n+2) \\in \\mathbb{Z} \;:\\; \\mathrm{fermatNumber}(n+2) = (\\mathrm{fermatNumber}(n+1))^2 - 2\\bigl(\\mathrm{fermatNumber}(n) - 1\\bigr)^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
  rw [Nat.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq,
    Nat.cast_sub <| two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq n]
  simp only [fermatNumber, push_cast, add_tsub_cancel_right]

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