harmonic_not_int — Mathlib

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'

Похожие утверждения