English
For a > 1 and n, j ∈ ℕ, the Pell x_n(n) divides a certain linear combination of x_j and y_n, with a conjugation implicity encoded; precisely, xn(a, n) ∣ (d(a) y_n(a) n (y_n(a) n xn(a, j)) + xn(a, j)).
Русский
Для a > 1 и n, j ∈ ℕ, x_n(a, n) делит заданную линейную комбинацию x_j и y_n(a) с участием d(a) и сопряжения.
LaTeX
$$$\\text{xn}(a, n) \\mid \\bigl( d(a)\\, y_n(a) \\cdot (y_n(a)\\cdot x_n(a, j)) + x_n(a, j) \\bigr)$$$
Lean4
theorem xn_modEq_x2n_add_lem (n j) : xn a1 n ∣ d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j :=
by
have h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (d a1 * yn a1 n * yn a1 n + 1) * xn a1 j := by
simp [add_mul, mul_assoc]
have h2 : d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n :=
by
zify at *
apply add_eq_of_eq_sub' (Eq.symm (pell_eqz a1 n))
rw [h2] at h1; rw [h1, mul_assoc]; exact dvd_mul_right _ _
