English
For all n with n > 0, the exponent of 2 in n! is strictly less than n.
Русский
Для любого n > 0 степень 2 в факториале n! строго меньше n.
LaTeX
$$$n \neq 0 \Rightarrow \nu_2(n!) < n$$$
Lean4
theorem emultiplicity_two_factorial_lt : ∀ {n : ℕ} (_ : n ≠ 0), emultiplicity 2 n ! < n :=
by
have h2 := prime_two.prime
refine binaryRec ?_ ?_
· exact fun h => False.elim <| h rfl
· intro b n ih h
by_cases hn : n = 0
· subst hn
simp only [ne_eq, bit_eq_zero_iff, true_and, Bool.not_eq_false] at h
simp only [bit, h, cond_true, mul_zero, zero_add, factorial_one]
rw [Prime.emultiplicity_one]
· exact zero_lt_one
· decide
have : emultiplicity 2 (2 * n)! < (2 * n : ℕ) :=
by
rw [prime_two.emultiplicity_factorial_mul]
rw [two_mul]
push_cast
apply WithTop.add_lt_add_right _ (ih hn)
exact Ne.symm nofun
cases b
· simpa
· suffices emultiplicity 2 (2 * n + 1) + emultiplicity 2 (2 * n)! < ↑(2 * n) + 1 by
simpa [emultiplicity_mul, h2, prime_two, bit, factorial]
rw [emultiplicity_eq_zero.2 (two_not_dvd_two_mul_add_one n), zero_add]
refine this.trans ?_
exact mod_cast lt_succ_self _
