English
For a > 1 and n, k, Pell sequences satisfy two simultaneous modular relations relating xn and yn modulo powers of yn.
Русский
Для a > 1 и n, k последовательности x_n и y_n удовлетворяют два одновременных модульных соотношения, связывающих x и y при модульности по степеням y.
LaTeX
$$$\\text{xy\\_modEq\\_yn}(a_n, n, k):\\; xn(a,n)^{ } \\equiv \\cdots \\pmod{yn(a,n)^2},\\; yn(a,n)^{ } \\equiv \\cdots \\pmod{yn(a,n)^3}$$$
Lean4
theorem xy_modEq_yn (n) :
∀ k,
xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2] ∧ yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
| 0 => by simp [Nat.ModEq.refl]
| k + 1 => by
let ⟨hx, hy⟩ := xy_modEq_yn n k
have L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2] :=
by
gcongr
rw [modEq_zero_iff_dvd, sq]
gcongr
apply dvd_mul_of_dvd_right
rw [← modEq_zero_iff_dvd]
refine (hy.of_dvd <| dvd_pow_self _ <| by decide).trans ?_
simp [modEq_zero_iff_dvd]
have R :
xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
yn a1 n ^ 3] :=
by
gcongr ?_ + ?_
· rw [_root_.pow_succ]
exact hx.mul_right' _
· have : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n := by
rcases k with - | k <;> simp [_root_.pow_succ]; ring_nf
rw [← this]
gcongr
rw [add_tsub_cancel_right, Nat.mul_succ, xn_add, yn_add, pow_succ (xn _ n), Nat.succ_mul,
add_comm (k * xn _ n ^ k) (xn _ n ^ k), right_distrib]
exact ⟨L, R⟩
