p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i in Ico 1 (succ (log p n)), n / p ^ i ≤ n / (p - 1)
p : ℕ
hp : Prime p
n : ℕ
⊢ multiplicity p n ! ≤ ↑(n / (p - 1))
rw [hp.multiplicity_factorial (lt_succ_self _), PartENat.coe_le_coe]
no goals
p : ℕ
hp : Prime p
n : ℕ
⊢ ∑ i in Ico 1 (succ (log p n)), n / p ^ i ≤ n / (p - 1)
exact Nat.geom_sum_Ico_le hp.two_le _ _