case pos
A : Type ?u.635032
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hn : n ≠ 1
h0 : n = 0
⊢ bernoulli n = bernoulli' n

case neg
A : Type ?u.635032
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
⊢ bernoulli n = bernoulli' n
A : Type ?u.635032
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hn : n ≠ 1
⊢ bernoulli n = bernoulli' n
by_cases h0 : n = 0
case neg
A : Type ?u.635032
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
⊢ (-1) ^ (n % 2) * bernoulli' n = bernoulli' n
case neg
A : Type ?u.635032
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
⊢ bernoulli n = bernoulli' n
rw [bernoulli, neg_one_pow_eq_pow_mod_two]
case neg.inl
A : Type ?u.635032
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
h : n % 2 = 0
⊢ (-1) ^ (n % 2) * bernoulli' n = bernoulli' n

case neg.inr
A : Type ?u.635032
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
h : n % 2 = 1
⊢ (-1) ^ (n % 2) * bernoulli' n = bernoulli' n
case neg
A : Type ?u.635032
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
⊢ (-1) ^ (n % 2) * bernoulli' n = bernoulli' n
cases' mod_two_eq_zero_or_one n with h h
no goals
case pos
A : Type ?u.635032
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hn : n ≠ 1
h0 : n = 0
⊢ bernoulli n = bernoulli' n
simp [h0]
no goals
case neg.inl
A : Type ?u.635032
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
h : n % 2 = 0
⊢ (-1) ^ (n % 2) * bernoulli' n = bernoulli' n
simp [h]
no goals
case neg.inr
A : Type ?u.635032
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hn : n ≠ 1
h0 : ¬n = 0
h : n % 2 = 1
⊢ (-1) ^ (n % 2) * bernoulli' n = bernoulli' n
simp [bernoulli'_odd_eq_zero (odd_iff.mpr h) (one_lt_iff_ne_zero_and_ne_one.mpr ⟨h0, hn⟩)]