d_nonsquare_of_one_lt_x — Mathlib

English

Let d be an integer. If there exists a solution a = (x, y) to the Pell equation x^2 - d y^2 = 1 with x > 1, then d is not a perfect square.

Русский

Пусть d — целое число. Если существует решение a = (x, y) уравнения Пелля x^2 - d y^2 = 1 с x > 1, то d не является квадратом.

LaTeX

$$$\big(\exists x,y\in \mathbb{Z},\; x^2 - d y^2 = 1 \ \land\ x > 1\big) \rightarrow \neg \IsSquare(d)$$$

Lean4

/-- If a solution has `x > 1`, then `d` is not a square. -/
theorem d_nonsquare_of_one_lt_x {a : Solution₁ d} (ha : 1 < a.x) : ¬IsSquare d :=
  by
  have hp := a.prop
  rintro ⟨b, rfl⟩
  simp_rw [← sq, ← mul_pow, sq_sub_sq, Int.mul_eq_one_iff_eq_one_or_neg_one] at hp
  cutsat

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