3.1 Extending Legendre sums

Lemma 3.1 Vanishing of large floor divisions

✓

For \(p \geq 2\) and \(i {\gt} \texttt{trunc\_ log}(p, n)\),

\[ \left\lfloor \frac{n}{p^i} \right\rfloor = 0. \]

Proof. By trunc_log_ltn, \(n {\lt} p^{\texttt{trunc\_ log}(p,n)+1} \leq p^i\). Apply divn_small.

Lemma 3.2 Legendre with extended bound

✓

For prime \(p\) and \(b {\gt} \texttt{trunc\_ log}(p, n)\),

\[ v_p(n!) = \sum _{i=1}^{b} \left\lfloor \frac{n}{p^i} \right\rfloor . \]

Proof. By Lemma 1.9, \(v_p(n!) = \sum _{i=1}^{n} \lfloor n/p^i \rfloor \). The extra terms for \(i {\gt} \texttt{trunc\_ log}(p,n)\) vanish by Lemma 3.1.