English
If d > 0 and d is not a square, then there exists a Pell solution x^2 - d y^2 = 1 with y ≠ 0.
Русский
Если d > 0 и не является квадратом, существует решение Пелля x^2 - d y^2 = 1 с y ≠ 0.
LaTeX
$$$\forall d\in \mathbb{Z},\; d>0\land \neg \IsSquare(d) \Rightarrow \exists x,y\in \mathbb{Z}, x^2 - d y^2 = 1 \land y \neq 0$$$
Lean4
/-- If `d` is a positive integer, then there is a nontrivial solution
to the Pell equation `x^2 - d*y^2 = 1` if and only if `d` is not a square. -/
theorem exists_iff_not_isSquare (h₀ : 0 < d) : (∃ x y : ℤ, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) ↔ ¬IsSquare d :=
by
refine ⟨?_, exists_of_not_isSquare h₀⟩
rintro ⟨x, y, hxy, hy⟩ ⟨a, rfl⟩
rw [← sq, ← mul_pow, sq_sub_sq] at hxy
simpa [hy, mul_self_pos.mp h₀, sub_eq_add_neg, eq_neg_self_iff] using Int.eq_of_mul_eq_one hxy
