English
For primes p, n > 0, and i in Ico(1, n), p^i divides n if and only if i ∈ Ico(1, b) for some bound; equivalently, the sets of indices where divisibility holds agree up to the bound where n < p^b.
Русский
Для простого p, n > 0 и i ∈ Ico(1, n) верно p^i | n тогда и только тогда, когда i ∈ Ico(1, b) для заданного верхнего предела; равенство множеств индексов делимости совпадает до границы n < p^b.
LaTeX
$$$ \{ i \in \mathrm{Ico}(1, n) \mid p^i \mid n \} = \{ i \in \mathrm{Ico}(1, b) \mid p^i \mid n \}$$$
Lean4
theorem Ico_pow_dvd_eq_Ico_of_lt {n p b : ℕ} (pp : p.Prime) (hn : n ≠ 0) (hb : n < p ^ b) :
{i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Ico 1 b | p ^ i ∣ n} :=
by
ext i
simp only [Finset.mem_filter, mem_Ico, and_congr_left_iff, and_congr_right_iff]
refine fun h1 h2 ↦ ⟨fun h ↦ ?_, fun h ↦ lt_of_pow_dvd_right hn (Prime.one_lt pp) h1⟩
rcases p with - | p
· rw [zero_pow (by cutsat), zero_dvd_iff] at h1
exact (hn h1).elim
· rw [← Nat.pow_lt_pow_iff_right (Prime.one_lt pp)]
apply lt_of_le_of_lt (le_of_dvd (Nat.zero_lt_of_ne_zero hn) h1) hb
