English
Let d be an integer and a1 a fundamental solution of the Pell equation x^2 − d y^2 = 1. Then for every other positive solution a with x-coordinate greater than 1, the x-coordinate of a1 is no larger than the x-coordinate of a; i.e., a1.x ≤ a.x whenever 1 < a.x.
Русский
Пусть d — целое число, а1 — фундаментальное решение уравнения Пелля x^2 − d y^2 = 1. Тогда для любого другого положительного решения a с x-координатой > 1 имеем a1.x ≤ a.x.
LaTeX
$$$\forall d \in \mathbb{Z},\; \forall a_1 \in \text{Solution}_1(d),\; \text{IsFundamental}(a_1) \Rightarrow \forall a \in \text{Solution}_1(d),\; 1 < a.x \Rightarrow a_1.x \le a.x.$$$
Lean4
/-- The `x`-coordinate of a fundamental solution is a lower bound for the `x`-coordinate
of any positive solution. -/
theorem x_le_x {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : 1 < a.x) : a₁.x ≤ a.x :=
h.2.2 hax
