English
Any nonnegative Pell solution is a nonnegative power of a fundamental solution. More precisely, if a is a solution with a.x > 0 and a.y ≥ 0, then there exists n ∈ ℕ such that a = a1^n for some fundamental a1.
Русский
Любое неотрицательное решение Пелля является неотрицательной степенью фундаментального решения: если a.x > 0 и a.y ≥ 0, то существует n ∈ ℕ such that a = a1^n для некоторого фундаментального a1.
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),\; a.x > 0 \land a.y \ge 0 \Rightarrow \exists n \in \mathbb{N},\; a = a_1^{n}.$$$
Lean4
/-- Any nonnegative solution is a power with nonnegative exponent of a fundamental solution. -/
theorem eq_pow_of_nonneg {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : 0 < a.x) (hay : 0 ≤ a.y) :
∃ n : ℕ, a = a₁ ^ n := by
lift a.x to ℕ using hax.le with ax hax'
induction ax using Nat.strong_induction_on generalizing a with
| h x ih =>
rcases hay.eq_or_lt with hy | hy
· -- case 1: `a = 1`
refine ⟨0, ?_⟩
simp only [pow_zero]
ext <;> simp only [x_one, y_one]
· have prop := a.prop
rw [← hy, sq (0 : ℤ), zero_mul, mul_zero, sub_zero, sq_eq_one_iff] at prop
refine prop.resolve_right fun hf => ?_
have := (hax.trans_eq hax').le.trans_eq hf
norm_num at this
· exact hy.symm
· -- case 2: `a ≥ a₁`
have hx₁ : 1 < a.x := by nlinarith [a.prop, h.d_pos]
have hxx₁ := h.mul_inv_x_pos hx₁ hy
have hxx₂ := h.mul_inv_x_lt_x hx₁ hy
have hyy := h.mul_inv_y_nonneg hx₁ hy
lift (a * a₁⁻¹).x to ℕ using hxx₁.le with x' hx'
obtain ⟨n, hn⟩ := ih x' (mod_cast hxx₂.trans_eq hax'.symm) hyy hx' hxx₁
exact ⟨n + 1, by rw [pow_succ', ← hn, mul_comm a, ← mul_assoc, mul_inv_cancel, one_mul]⟩
