English
All odd Bernoulli' numbers greater than 1 are zero: B'(2m+1) = 0 for m ≥ 1.
Русский
Все нечетные числа Бернулли', большие единицы, равны нулю.
LaTeX
$$$\forall n>1\text{ odd},\; \bernoulli'(n) = 0$$$
Lean4
/-- Odd Bernoulli numbers (greater than 1) are zero. -/
theorem bernoulli'_odd_eq_zero {n : ℕ} (h_odd : Odd n) (hlt : 1 < n) : bernoulli' n = 0 :=
by
let B := mk fun n => bernoulli' n / (n ! : ℚ)
suffices (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
by
rcases mul_eq_mul_right_iff.mp this with h | h <;> simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h
· apply eq_zero_of_neg_eq
specialize h n
split_ifs at h <;> simp_all [B, h_odd.neg_one_pow, factorial_ne_zero]
· simpa +decide [Nat.factorial] using h 1
have h : B * (exp ℚ - 1) = X * exp ℚ := by simpa [bernoulli'PowerSeries] using bernoulli'PowerSeries_mul_exp_sub_one ℚ
rw [sub_mul, h, mul_sub X, sub_right_inj, ← neg_sub, mul_neg, neg_eq_iff_eq_neg]
suffices evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ by
simpa [mul_assoc, sub_mul, mul_comm (evalNegHom (exp ℚ)), exp_mul_exp_neg_eq_one]
congr
