English
For a > 1, if x^2 − d(a1) y^2 = 1, then there exists n with x = x_n(a1, n) and y = y_n(a1, n).
Русский
Пусть a > 1. Если x^2 − d(a1) y^2 = 1, то существует n такое, что x = x_n(a1, n) и y = y_n(a1, n).
LaTeX
$$$ \exists n\, (x = x_n(a1,n) \land y = y_n(a1,n)) $$$
Lean4
/-- Every solution to **Pell's equation** is recursively obtained from the initial solution
`(1,0)` using the recursion `pell`. -/
theorem eq_pell {x y : ℕ} (hp : x * x - d a1 * y * y = 1) : ∃ n, x = xn a1 n ∧ y = yn a1 n :=
have : (1 : ℤ√(d a1)) ≤ ⟨x, y⟩ :=
match x, hp with
| 0, (hp : 0 - _ = 1) => by rw [zero_tsub] at hp; contradiction
| x + 1, _hp => Zsqrtd.le_of_le_le (Int.ofNat_le_ofNat_of_le <| Nat.succ_pos x) (Int.ofNat_zero_le _)
let ⟨m, e⟩ := eq_pellZd a1 ⟨x, y⟩ this ((isPell_nat a1).2 hp)
⟨m,
match x, y, e with
| _, _, rfl => ⟨rfl, rfl⟩⟩
