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