English
If x and y of a Pell solution are positive, then for any natural exponent n, the y-coordinate of a^n is positive.
Русский
Если x и y решения Пелля положительны, то для любого натурального показателя n y-координата a^n положительна.
LaTeX
$$$\forall a\in \mathrm{Solution}_1(d),\; a_x>0 \land a_y>0 \rightarrow \forall n\in \mathbb{N},\; (a^n)_y > 0$$$
Lean4
/-- If `(x, y)` is a solution with `x` and `y` positive, then all its powers with positive
natural exponents have positive `y`. -/
theorem y_pow_succ_pos {a : Solution₁ d} (hax : 0 < a.x) (hay : 0 < a.y) (n : ℕ) : 0 < (a ^ n.succ).y := by
induction n with
| zero => simp only [pow_one, hay]
| succ n ih => rw [pow_succ']; exact y_mul_pos hax hay (x_pow_pos hax _) ih
