English
As before, the y-coordinate remains positive under multiplication for positively valued components.
Русский
Как и ранее, y-координата остается положительной при умножении для положительных компонентов.
LaTeX
$$$\forall a,b\in \mathrm{Solution}_1(d),\; a_x>0 \land a_y>0 \land b_x>0 \land b_y>0 \rightarrow (a\cdot b)_y > 0$$$
Lean4
/-- If `d` is a positive integer that is not a square, then there exists a solution
to the Pell equation `x^2 - d*y^2 = 1` with `x > 1` and `y > 0`. -/
theorem exists_pos_of_not_isSquare (h₀ : 0 < d) (hd : ¬IsSquare d) : ∃ a : Solution₁ d, 1 < a.x ∧ 0 < a.y :=
by
obtain ⟨x, y, h, hy⟩ := exists_of_not_isSquare h₀ hd
refine ⟨mk |x| |y| (by rwa [sq_abs, sq_abs]), ?_, abs_pos.mpr hy⟩
rw [x_mk, ← one_lt_sq_iff_one_lt_abs, eq_add_of_sub_eq h, lt_add_iff_pos_right]
exact mul_pos h₀ (sq_pos_of_ne_zero hy)
