p : ℕ
w : 0 < p
i : ℕ
⊢ sMod p i % (2 ^ p - 1) < 2 ^ p - 1
p : ℕ
w : 0 < p
i : ℕ
⊢ sMod p i < 2 ^ p - 1
rw [← sMod_mod]
p : ℕ
w : 0 < p
i : ℕ
⊢ abs (2 ^ p - 1) = 2 ^ p - 1
p : ℕ
w : 0 < p
i : ℕ
⊢ sMod p i % (2 ^ p - 1) < 2 ^ p - 1
refine (Int.emod_lt _ (mersenne_int_ne_zero p w)).trans_eq ?_
no goals
p : ℕ
w : 0 < p
i : ℕ
⊢ abs (2 ^ p - 1) = 2 ^ p - 1
exact abs_of_nonneg (mersenne_int_pos w).le