English
The set of Pell solutions with positive x-coordinate is closed under multiplication.
Русский
Набор решений Пелля с положительным x закрыт относительно умножения.
LaTeX
$$$\forall a,b\in \mathrm{Solution}_1(d),\; (0 < a_x) \land (0 < b_x) \rightarrow 0 < (a\cdot b)_x$$$
Lean4
/-- The set of solutions with `x > 0` is closed under multiplication. -/
theorem x_mul_pos {a b : Solution₁ d} (ha : 0 < a.x) (hb : 0 < b.x) : 0 < (a * b).x :=
by
simp only [x_mul]
refine neg_lt_iff_pos_add'.mp (abs_lt.mp ?_).1
rw [← abs_of_pos ha, ← abs_of_pos hb, ← abs_mul, ← sq_lt_sq, mul_pow a.x, a.prop_x, b.prop_x, ← sub_pos]
ring_nf
rcases le_or_gt 0 d with h | h
· positivity
· rw [(eq_zero_of_d_neg h a).resolve_left ha.ne', (eq_zero_of_d_neg h b).resolve_left hb.ne']
simp
