English
As above, for the same hypotheses, (sModNat(2^p−1) k) equals sMod p k in integers.
Русский
Как и ранее, при тех же предпосылках (sModNat(2^p−1) k) равно sMod p k в целых.
LaTeX
$$$ (sModNat (2^p - 1) k : \mathbb{Z}) = sMod p k $$$
Lean4
theorem sModNat_eq_sMod (p k : ℕ) (hp : 2 ≤ p) : (sModNat (2 ^ p - 1) k : ℤ) = sMod p k :=
by
have h1 :=
calc
4 = 2 ^ 2 := by simp
_ ≤ 2 ^ p := Nat.pow_le_pow_right (by simp) hp
have h2 : 1 ≤ 2 ^ p := by omega
induction k with
| zero =>
rw [sModNat, sMod, Int.natCast_emod]
simp [h2]
| succ k ih =>
rw [sModNat, sMod, ← ih]
have h3 : 2 ≤ 2 ^ p - 1 := by
zify [h2]
calc
(2 : Int) ≤ 4 - 1 := by simp
_ ≤ 2 ^ p - 1 := by zify at h1; exact Int.sub_le_sub_right h1 _
zify [h2, h3]
rw [← add_sub_assoc, sub_eq_add_neg, add_assoc, add_comm _ (-2), ← add_assoc, Int.add_emod_right, ← sub_eq_add_neg]
