English
For a positive integer d, there exists a nontrivial solution to x^2 - d y^2 = 1 iff d is not a square.
Русский
Для положительного d не являющегося квадратом существует решение x^2 - d y^2 = 1 тогда и только тогда, когда d не квадрат.
LaTeX
$$$\exists x,y\in \mathbb{Z}, x^2 - d y^2 = 1 \land y \neq 0 \quad\text{iff}\quad \neg \IsSquare(d)$$$
Lean4
/-- If `d` is positive and not a square, then a fundamental solution exists. -/
theorem exists_of_not_isSquare (h₀ : 0 < d) (hd : ¬IsSquare d) : ∃ a : Solution₁ d, IsFundamental a :=
by
obtain ⟨a, ha₁, ha₂⟩ := exists_pos_of_not_isSquare h₀ hd
have P : ∃ x' : ℕ, 1 < x' ∧ ∃ y' : ℤ, 0 < y' ∧ (x' : ℤ) ^ 2 - d * y' ^ 2 = 1 :=
by
have hax := a.prop
lift a.x to ℕ using by positivity with ax
norm_cast at ha₁
exact ⟨ax, ha₁, a.y, ha₂, hax⟩
classical
-- to avoid having to show that the predicate is decidable
let x₁ := Nat.find P
obtain ⟨hx, y₁, hy₀, hy₁⟩ := Nat.find_spec P
refine ⟨mk x₁ y₁ hy₁, by rw [x_mk]; exact mod_cast hx, hy₀, fun {b} hb => ?_⟩
rw [x_mk]
have hb' := (Int.toNat_of_nonneg <| zero_le_one.trans hb.le).symm
have hb'' := hb
rw [hb'] at hb ⊢
norm_cast at hb ⊢
refine Nat.find_min' P ⟨hb, |b.y|, abs_pos.mpr <| y_ne_zero_of_one_lt_x hb'', ?_⟩
rw [← hb', sq_abs]
exact b.prop
