English
If y > 0, k > 0, and y^k < a, then the integer y^k is strictly less than 2 a y − y^2 − 1.
Русский
Если y > 0, k > 0 и y^k < a, то целое y^k строго меньше 2 a y − y^2 − 1.
LaTeX
$$$$ (y^k)_{ \mathbb{Z} } < 2 a y - y^2 - 1 \qquad (y>0, k>0, y^k < a) $$$$
Lean4
theorem eq_pow_of_pell {m n k} :
n ^ k = m ↔
k = 0 ∧ m = 1 ∨
0 < k ∧
(n = 0 ∧ m = 0 ∨
0 < n ∧
∃ (w a t z : ℕ) (a1 : 1 < a),
xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
2 * a * n = t + (n * n + 1) ∧
m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1) :=
by
constructor
· rintro rfl
refine k.eq_zero_or_pos.imp (fun k0 : k = 0 => k0.symm ▸ ⟨rfl, rfl⟩) fun hk => ⟨hk, ?_⟩
refine n.eq_zero_or_pos.imp (fun n0 : n = 0 ↦ n0.symm ▸ ⟨rfl, zero_pow hk.ne'⟩) fun hn ↦ ⟨hn, ?_⟩
set w := max n k
have nw : n ≤ w := le_max_left _ _
have kw : k ≤ w := le_max_right _ _
have wpos : 0 < w := hn.trans_le nw
have w1 : 1 < w + 1 := Nat.succ_lt_succ wpos
set a := xn w1 w
have a1 : 1 < a := strictMono_x w1 wpos
have na : n ≤ a := nw.trans (n_lt_xn w1 w).le
set x := xn a1 k
set y := yn a1 k
obtain ⟨z, ze⟩ : w ∣ yn w1 w := modEq_zero_iff_dvd.1 ((yn_modEq_a_sub_one w1 w).trans dvd_rfl.modEq_zero_nat)
have nt : (↑(n ^ k) : ℤ) < 2 * a * n - n * n - 1 :=
by
refine eq_pow_of_pell_lem hn.ne' hk.ne' ?_
calc
n ^ k ≤ n ^ w := Nat.pow_le_pow_right hn kw
_ < (w + 1) ^ w := (Nat.pow_lt_pow_left (Nat.lt_succ_of_le nw) wpos.ne')
_ ≤ a := xn_ge_a_pow w1 w
lift (2 * a * n - n * n - 1 : ℤ) to ℕ using (Nat.cast_nonneg _).trans nt.le with t te
have tm : x ≡ y * (a - n) + n ^ k [MOD t] := by
apply modEq_of_dvd
rw [Int.natCast_add, Int.natCast_mul, Int.ofNat_sub na, te]
exact x_sub_y_dvd_pow a1 n k
have ta : 2 * a * n = t + (n * n + 1) := by
zify
omega
have zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1 := ze ▸ pell_eq w1 w
exact ⟨w, a, t, z, a1, tm, ta, Nat.cast_lt.1 nt, nw, kw, zp⟩
· rintro (⟨rfl, rfl⟩ | ⟨hk0, ⟨rfl, rfl⟩ | ⟨hn0, w, a, t, z, a1, tm, ta, mt, nw, kw, zp⟩⟩)
· exact _root_.pow_zero n
· exact zero_pow hk0.ne'
have hw0 : 0 < w := hn0.trans_le nw
have hw1 : 1 < w + 1 := Nat.succ_lt_succ hw0
rcases eq_pell hw1 zp with ⟨j, rfl, yj⟩
have hj0 : 0 < j := by
apply Nat.pos_of_ne_zero
rintro rfl
exact lt_irrefl 1 a1
have wj : w ≤ j :=
Nat.le_of_dvd hj0
(modEq_zero_iff_dvd.1 <| (yn_modEq_a_sub_one hw1 j).symm.trans <| modEq_zero_iff_dvd.2 ⟨z, yj.symm⟩)
have hnka : n ^ k < xn hw1 j :=
calc
n ^ k ≤ n ^ j := Nat.pow_le_pow_right hn0 (le_trans kw wj)
_ < (w + 1) ^ j := (Nat.pow_lt_pow_left (Nat.lt_succ_of_le nw) hj0.ne')
_ ≤ xn hw1 j := xn_ge_a_pow hw1 j
have nt : (↑(n ^ k) : ℤ) < 2 * xn hw1 j * n - n * n - 1 := eq_pow_of_pell_lem hn0.ne' hk0.ne' hnka
have na : n ≤ xn hw1 j := (Nat.le_self_pow hk0.ne' _).trans hnka.le
have te : (t : ℤ) = 2 * xn hw1 j * n - n * n - 1 :=
by
rw [sub_sub, eq_sub_iff_add_eq]
exact mod_cast ta.symm
have : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t] :=
by
apply modEq_of_dvd
rw [te, Nat.cast_add, Nat.cast_mul, Int.ofNat_sub na]
exact x_sub_y_dvd_pow a1 n k
have : n ^ k % t = m % t := (this.symm.trans tm).add_left_cancel' _
rw [← te] at nt
rwa [Nat.mod_eq_of_lt (Nat.cast_lt.1 nt), Nat.mod_eq_of_lt mt] at this
