English
Let a1 be a fundamental Pell solution for d and let a be any solution with x > 1 and y > 0. Then the y-coordinate of a1 is a lower bound for the y-coordinate of a: a1.y ≤ a.y.
Русский
Пусть a1 — фундаментальное решение уравнения Пелля x^2 − d y^2 = 1 и пусть a — произвольное решение с x > 1 и y > 0. Тогда y-коордaината a1 не превосходит y-координату a: a1.y ≤ a.y.
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 0 < a.y \Rightarrow a_1.y \le a.y.$$$
Lean4
/-- The `y`-coordinate of a fundamental solution is a lower bound for the `y`-coordinate
of any positive solution. -/
theorem y_le_y {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : 1 < a.x) (hay : 0 < a.y) :
a₁.y ≤ a.y :=
by
have H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2 := by rw [a.prop_x, a₁.prop_x]; ring
rw [← abs_of_pos hay, ← abs_of_pos h.2.1, ← sq_le_sq, ← mul_le_mul_iff_right₀ h.d_pos, ← sub_nonpos, ← mul_sub, H,
sub_nonpos, sq_le_sq, abs_of_pos (zero_lt_one.trans h.1), abs_of_pos (zero_lt_one.trans hax)]
exact h.x_le_x hax
