English
If j ≤ 2n, then xn(a1, 4n − j) ≡ xn(a1, j) (mod xn(a1, n)).
Русский
Если j ≤ 2n, то xn(a1, 4n − j) ≡ xn(a1, j) (mod xn(a1, n)).
LaTeX
$$$$ xn(a1, 4n - j) \\equiv xn(a1, j) \\pmod{ xn(a1, n) } $$$$
Lean4
theorem eq_pow_of_pell_lem {a y k : ℕ} (hy0 : y ≠ 0) (hk0 : k ≠ 0) (hyk : y ^ k < a) :
(↑(y ^ k) : ℤ) < 2 * a * y - y * y - 1 :=
have hya : y < a := (Nat.le_self_pow hk0 _).trans_lt hyk
calc
(↑(y ^ k) : ℤ) < a := Nat.cast_lt.2 hyk
_ ≤ (a : ℤ) ^ 2 - (a - 1 : ℤ) ^ 2 - 1 :=
by
rw [sub_sq, mul_one, one_pow, sub_add, sub_sub_cancel, two_mul, sub_sub, ← add_sub, le_add_iff_nonneg_right,
sub_nonneg, Int.add_one_le_iff]
norm_cast
exact lt_of_le_of_lt (Nat.succ_le_of_lt (Nat.pos_of_ne_zero hy0)) hya
_ ≤ (a : ℤ) ^ 2 - (a - y : ℤ) ^ 2 - 1 := by
have := hya.le
gcongr <;> norm_cast <;> omega
_ = 2 * a * y - y * y - 1 := by ring
