English
If a ≡ b (mod c) with a, b > 1, then for all n, x_n^{(a)} ≡ x_n^{(b)} (mod c) and y_n^{(a)} ≡ y_n^{(b)} (mod c).
Русский
Если a ≡ b (mod c) и a, b > 1, то для всех n выполняется x_n^{(a)} ≡ x_n^{(b)} (mod c) и y_n^{(a)} ≡ y_n^{(b)} (mod c).
LaTeX
$$$$ a \\equiv b \\pmod{c}, \\ a,b > 1 \\quad \\Rightarrow\\quad x_n^{(a)} \\equiv x_n^{(b)} \\pmod{c} \\land y_n^{(a)} \\equiv y_n^{(b)} \\pmod{c} $$$$
Lean4
theorem modEq_of_xn_modEq {i j n} (ipos : 0 < i) (hin : i ≤ n) (h : xn a1 j ≡ xn a1 i [MOD xn a1 n]) :
j ≡ i [MOD 4 * n] ∨ j + i ≡ 0 [MOD 4 * n] :=
let j' := j % (4 * n)
have n4 : 0 < 4 * n := mul_pos (by decide) (ipos.trans_le hin)
have jl : j' < 4 * n := Nat.mod_lt _ n4
have jj : j ≡ j' [MOD 4 * n] := by delta ModEq; rw [Nat.mod_eq_of_lt jl]
have : ∀ j q, xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n] := by intro j q;
induction q with
| zero => simp [ModEq.refl]
| succ q IH =>
rw [Nat.mul_succ, ← add_assoc, add_comm]
exact (xn_modEq_x4n_add _ _ _).trans IH
Or.imp (fun ji : j' = i => by rwa [← ji])
(fun ji : j' + i = 4 * n =>
(jj.add_right _).trans <| by
rw [ji]
exact dvd_rfl.modEq_zero_nat)
(eq_of_xn_modEq' a1 ipos hin jl.le <|
(h.symm.trans <| by
rw [← Nat.mod_add_div j (4 * n)]
exact this j' _).symm)
