English
For a > 1, for any n and b, if certain constructive conditions hold, then there exists n with b = pellZd a1 n.
Русский
Пусть a > 1, для любых n и b выполняются определенные условия; тогда существует n such that b = pellZd a1 n.
LaTeX
$$$ \exists n\, b = pellZd(a1, n) $$$
Lean4
theorem eq_pell_lem : ∀ (n) (b : ℤ√(d a1)), 1 ≤ b → IsPell b → b ≤ pellZd a1 n → ∃ n, b = pellZd a1 n
| 0, _ => fun h1 _ hl => ⟨0, @Zsqrtd.le_antisymm _ (dnsq a1) _ _ hl h1⟩
| n + 1, b => fun h1 hp h =>
have a1p : (0 : ℤ√(d a1)) ≤ ⟨a, 1⟩ := trivial
have am1p : (0 : ℤ√(d a1)) ≤ ⟨a, -1⟩ := show (_ : Nat) ≤ _ by simp; exact Nat.pred_le _
have a1m : (⟨a, 1⟩ * ⟨a, -1⟩ : ℤ√(d a1)) = 1 := isPell_norm.1 (isPell_one a1)
if ha : (⟨↑a, 1⟩ : ℤ√(d a1)) ≤ b then
let ⟨m, e⟩ :=
eq_pell_lem n (b * ⟨a, -1⟩) (by rw [← a1m]; exact mul_le_mul_of_nonneg_right ha am1p)
(isPell_mul hp (isPell_star.1 (isPell_one a1)))
(by
have t := mul_le_mul_of_nonneg_right h am1p
rwa [pellZd_succ, mul_assoc, a1m, mul_one] at t)
⟨m + 1, by
rw [show b = b * ⟨a, -1⟩ * ⟨a, 1⟩ by rw [mul_assoc, Eq.trans (mul_comm _ _) a1m]; simp, pellZd_succ, e]⟩
else
suffices ¬1 < b from ⟨0, show b = 1 from (Or.resolve_left (lt_or_eq_of_le h1) this).symm⟩
fun h1l => by
obtain ⟨x, y⟩ := b
exact by
have bm : (_ * ⟨_, _⟩ : ℤ√d a1) = 1 := Pell.isPell_norm.1 hp
have y0l : (0 : ℤ√d a1) < ⟨x - x, y - -y⟩ :=
sub_lt_sub h1l fun hn : (1 : ℤ√d a1) ≤ ⟨x, -y⟩ =>
by
have t := mul_le_mul_of_nonneg_left hn (le_trans zero_le_one h1)
rw [bm, mul_one] at t
exact h1l t
have yl2 : (⟨_, _⟩ : ℤ√_) < ⟨_, _⟩ :=
show (⟨x, y⟩ - ⟨x, -y⟩ : ℤ√d a1) < ⟨a, 1⟩ - ⟨a, -1⟩ from
sub_lt_sub ha fun hn : (⟨x, -y⟩ : ℤ√d a1) ≤ ⟨a, -1⟩ =>
by
have t := mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hn (le_trans zero_le_one h1)) a1p
rw [bm, one_mul, mul_assoc, Eq.trans (mul_comm _ _) a1m, mul_one] at t
exact ha t
simp only [sub_self, sub_neg_eq_add] at y0l;
simp only [Zsqrtd.re_neg, add_neg_cancel, Zsqrtd.im_neg, neg_neg] at yl2
exact
match y, y0l, (yl2 : (⟨_, _⟩ : ℤ√_) < ⟨_, _⟩) with
| 0, y0l, _ => y0l (le_refl 0)
| (y + 1 : ℕ), _, yl2 =>
yl2
(Zsqrtd.le_of_le_le (by simp)
(let t := Int.ofNat_le_ofNat_of_le (Nat.succ_pos y)
add_le_add t t))
| Int.negSucc _, y0l, _ => y0l trivial
