English
For every n ≥ 2, the harmonic number Hn is not an integer.
Русский
Для каждого n ≥ 2 гармоническое число Hn не целое.
LaTeX
$$$H_n \\notin \\mathbb{Z} \\\\text{ for } n \\ge 2$$$
Lean4
/-- The n-th harmonic number is not an integer for n ≥ 2. -/
theorem harmonic_not_int {n : ℕ} (h : 2 ≤ n) : ¬(harmonic n).isInt :=
by
apply padicNorm.not_int_of_not_padic_int 2
rw [padicNorm.eq_zpow_of_nonzero (harmonic_pos (ne_zero_of_lt h)).ne', padicValRat_two_harmonic, neg_neg,
zpow_natCast]
exact one_lt_pow₀ one_lt_two (Nat.log_pos one_lt_two h).ne'