English
Let a1 be a fundamental Pell solution for d and a a solution with 1 < a.x and a.y > 0. Then the x-coordinate of a a1^{-1} is positive: (a a1^{-1}).x > 0.
Русский
Пусть a1 — фундаментальное решение Пелля, а a — решение с 1 < a.x и a.y > 0. Тогда x-координата (a a1^{-1}) положительна: (a a1^{-1}).x > 0.
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 \cdot a_1^{-1}).x.$$$
Lean4
/-- If we multiply a positive solution with the inverse of a fundamental solution,
the `x`-coordinate stays positive. -/
theorem mul_inv_x_pos {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : 1 < a.x) (hay : 0 < a.y) :
0 < (a * a₁⁻¹).x :=
by
simp only [x_mul, x_inv, y_inv, mul_neg, lt_add_neg_iff_add_lt, zero_add]
refine lt_of_mul_lt_mul_left ?_ <| zero_le_one.trans hax.le
calc
a.x * (d * (a.y * a₁.y))
_ = d * a.y * (a.x * a₁.y) := by ring
_ ≤ d * a.y * (a.y * a₁.x) := by have := x_mul_y_le_y_mul_x h hax hay; have := h.d_pos; gcongr
_ = (a.x ^ 2 - 1) * a₁.x := by rw [← a.prop_y]; ring
_ < a.x * (a.x * a₁.x) := by linarith [h.1]
