no goals
p : ℕ
hp : Prime p
b : ℕ
x✝ : log p 0 < b
⊢ multiplicity p 0! = ↑(∑ i in Ico 1 b, 0 / p ^ i)
simp [Ico, hp.multiplicity_one]
no goals
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ multiplicity p (n + 1)! = multiplicity p n ! + multiplicity p (n + 1)
rw [factorial_succ, hp.multiplicity_mul, add_comm]
no goals
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ multiplicity p n ! + multiplicity p (n + 1) =
    ↑(∑ i in Ico 1 b, n / p ^ i) + ↑(card (filter (fun i => p ^ i ∣ n + 1) (Ico 1 b)))
rw [multiplicity_factorial hp ((log_mono_right <| le_succ _).trans_lt hb), ←
  multiplicity_eq_card_pow_dvd hp.ne_one (succ_pos _) hb]
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i in Ico 1 b, n / p ^ i) + ↑(card (filter (fun i => p ^ i ∣ n + 1) (Ico 1 b))) =
    ↑(∑ x in Ico 1 b, n / p ^ x + ↑(card (filter (fun x => p ^ x ∣ n + 1) (Ico 1 b))))
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i in Ico 1 b, n / p ^ i) + ↑(card (filter (fun i => p ^ i ∣ n + 1) (Ico 1 b))) =
    ↑(∑ i in Ico 1 b, (n / p ^ i + if p ^ i ∣ n + 1 then 1 else 0))
rw [sum_add_distrib, sum_boole]
no goals
p : ℕ
hp : Prime p
n b : ℕ
hb : log p (n + 1) < b
⊢ ↑(∑ i in Ico 1 b, n / p ^ i) + ↑(card (filter (fun i => p ^ i ∣ n + 1) (Ico 1 b))) =
    ↑(∑ x in Ico 1 b, n / p ^ x + ↑(card (filter (fun x => p ^ x ∣ n + 1) (Ico 1 b))))
simp