English
If p is prime, n > 0, and n ≤ p^b, then the set of i in Ico(1,n) with p^i | n equals the set of i in Icc(1,b) with p^i | n.
Русский
Если p — простое, n > 0 и n ≤ p^b, тогда множества i ∈ Ico(1,n) с p^i | n совпадает с i ∈ Icc(1,b) с p^i | n.
LaTeX
$$$ {i \in \mathrm{Ico}(1, n) \mid p^i \mid n} = {i \in \mathrm{Icc}(1, b) \mid p^i \mid n} $$$
Lean4
theorem Ico_filter_pow_dvd_eq {n p b : ℕ} (pp : p.Prime) (hn : n ≠ 0) (hb : n ≤ p ^ b) :
{i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Icc 1 b | p ^ i ∣ n} :=
by
ext x
simp only [Finset.mem_filter, mem_Ico, mem_Icc, and_congr_left_iff, and_congr_right_iff]
rintro h1 -
exact
iff_of_true (lt_of_pow_dvd_right hn pp.two_le h1) <|
(Nat.pow_le_pow_iff_right pp.one_lt).1 <| (le_of_dvd hn.bot_lt h1).trans hb
