A : Type ?u.186788
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ 1 -
      (0 + ↑(Nat.choose 3 0) / (↑3 - ↑0 + 1) * bernoulli' 0 + ↑(Nat.choose 3 1) / (↑3 - ↑1 + 1) * bernoulli' 1 +
        ↑(Nat.choose 3 2) / (↑3 - ↑2 + 1) * bernoulli' 2) =
    0
A : Type ?u.186788
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ bernoulli' 3 = 0
rw [bernoulli'_def, sum_range_succ, sum_range_succ, sum_range_succ, sum_range_zero]
no goals
A : Type ?u.186788
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ 1 -
      (0 + ↑(Nat.choose 3 0) / (↑3 - ↑0 + 1) * bernoulli' 0 + ↑(Nat.choose 3 1) / (↑3 - ↑1 + 1) * bernoulli' 1 +
        ↑(Nat.choose 3 2) / (↑3 - ↑2 + 1) * bernoulli' 2) =
    0
norm_num