English
If a ≡ b (mod c) and a,b > 1, then the Pell sequences are congruent termwise: xn a1 n ≡ xn b1 n (mod c) and yn a1 n ≡ yn b1 n (mod c) for all n.
Русский
Если a ≡ b (mod c) и a,b > 1, то последовательности Пелля совпадают по членам: xn a1 n ≡ xn b1 n (mod c) и yn a1 n ≡ yn b1 n (mod c) для всех n.
LaTeX
$$$$ x_n^{(a)} \\equiv x_n^{(b)} \\pmod{c} \\quad \\text{и} \\quad y_n^{(a)} \\equiv y_n^{(b)} \\pmod{c} $$$$
Lean4
theorem xy_modEq_of_modEq {a b c} (a1 : 1 < a) (b1 : 1 < b) (h : a ≡ b [MOD c]) :
∀ n, xn a1 n ≡ xn b1 n [MOD c] ∧ yn a1 n ≡ yn b1 n [MOD c]
| 0 => by simp [Nat.ModEq.refl]
| 1 => by simpa [Nat.ModEq.refl]
| n + 2 =>
⟨(xy_modEq_of_modEq a1 b1 h n).left.add_right_cancel <|
by
rw [xn_succ_succ a1, xn_succ_succ b1]
exact (h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).left,
(xy_modEq_of_modEq a1 b1 h n).right.add_right_cancel <|
by
rw [yn_succ_succ a1, yn_succ_succ b1]
exact (h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).right⟩
