English
Translation formula: B_n(1+x) = B_n(x) + n x^{n-1}.
Русский
Формула переноса: B_n(1+x) = B_n(x) + n x^{n-1}.
LaTeX
$$$B_n(1+x) = B_n(x) + n \; x^{n-1}$$$
Lean4
theorem bernoulli_eval_one_add (n : ℕ) (x : ℚ) : (bernoulli n).eval (1 + x) = (bernoulli n).eval x + n * x ^ (n - 1) :=
by
refine Nat.strong_induction_on n fun d hd => ?_
have nz : ((d.succ : ℕ) : ℚ) ≠ 0 := by norm_cast
apply (mul_right_inj' nz).1
rw [← smul_eq_mul, ← eval_smul, bernoulli_eq_sub_sum, mul_add, ← smul_eq_mul, ← eval_smul, bernoulli_eq_sub_sum,
eval_sub, eval_finset_sum]
conv_lhs =>
congr
· skip
· apply_congr
· skip
· rw [eval_smul, hd _ (mem_range.1 (by assumption))]
rw [eval_sub, eval_finset_sum]
simp_rw [eval_smul, smul_add]
rw [sum_add_distrib, sub_add, sub_eq_sub_iff_sub_eq_sub, _root_.add_sub_sub_cancel]
conv_rhs =>
congr
· skip
· congr
rw [succ_eq_add_one, ← choose_succ_self_right d]
rw [Nat.cast_succ, ← smul_eq_mul, ← sum_range_succ _ d, eval_monomial_one_add_sub]
simp_rw [smul_eq_mul]
