[GOAL]
n : ℕ
⊢ bernoulli n = ∑ i in range (n + 1), ↑(monomial i) (_root_.bernoulli (n - i) * ↑(Nat.choose n i))
[PROOFSTEP]
rw [← sum_range_reflect, add_succ_sub_one, add_zero, bernoulli]
[GOAL]
n : ℕ
⊢ ∑ i in range (n + 1), ↑(monomial (n - i)) (_root_.bernoulli i * ↑(Nat.choose n i)) =
    ∑ j in range (n + 1), ↑(monomial (n - j)) (_root_.bernoulli (n - (n - j)) * ↑(Nat.choose n (n - j)))
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range (n + 1) →
      ↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x)) =
        ↑(monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(Nat.choose n (n - x)))
[PROOFSTEP]
rintro x hx
[GOAL]
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x)) =
    ↑(monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(Nat.choose n (n - x)))
[PROOFSTEP]
rw [mem_range_succ_iff] at hx
[GOAL]
n x : ℕ
hx : x ≤ n
⊢ ↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x)) =
    ↑(monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(Nat.choose n (n - x)))
[PROOFSTEP]
rw [choose_symm hx, tsub_tsub_cancel_of_le hx]
[GOAL]
⊢ bernoulli 0 = 1
[PROOFSTEP]
simp [bernoulli]
[GOAL]
n : ℕ
⊢ eval 0 (bernoulli n) = _root_.bernoulli n
[PROOFSTEP]
rw [bernoulli, eval_finset_sum, sum_range_succ]
[GOAL]
n : ℕ
⊢ ∑ x in range n, eval 0 (↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x))) +
      eval 0 (↑(monomial (n - n)) (_root_.bernoulli n * ↑(Nat.choose n n))) =
    _root_.bernoulli n
[PROOFSTEP]
have : (∑ x : ℕ in range n, _root_.bernoulli x * n.choose x * 0 ^ (n - x)) = 0 :=
  by
  apply sum_eq_zero <| fun x hx => _
  intros x hx
  have h : x < n := (mem_range.1 hx)
  simp [h]
[GOAL]
n : ℕ
⊢ ∑ x in range n, _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
[PROOFSTEP]
apply sum_eq_zero <| fun x hx => _
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range n → _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
[PROOFSTEP]
intros x hx
[GOAL]
n x : ℕ
hx : x ∈ range n
⊢ _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
[PROOFSTEP]
have h : x < n := (mem_range.1 hx)
[GOAL]
n x : ℕ
hx : x ∈ range n
h : x < n
⊢ _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
[PROOFSTEP]
simp [h]
[GOAL]
n : ℕ
this : ∑ x in range n, _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
⊢ ∑ x in range n, eval 0 (↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x))) +
      eval 0 (↑(monomial (n - n)) (_root_.bernoulli n * ↑(Nat.choose n n))) =
    _root_.bernoulli n
[PROOFSTEP]
simp [this]
[GOAL]
n : ℕ
⊢ eval 1 (bernoulli n) = bernoulli' n
[PROOFSTEP]
simp only [bernoulli, eval_finset_sum]
[GOAL]
n : ℕ
⊢ ∑ i in range (n + 1), eval 1 (↑(monomial (n - i)) (_root_.bernoulli i * ↑(Nat.choose n i))) = bernoulli' n
[PROOFSTEP]
simp only [← succ_eq_add_one, sum_range_succ, mul_one, cast_one, choose_self, (_root_.bernoulli _).mul_comm,
  sum_bernoulli, one_pow, mul_one, eval_C, eval_monomial, one_mul]
[GOAL]
n : ℕ
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
[PROOFSTEP]
by_cases h : n = 1
[GOAL]
case pos
n : ℕ
h : n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
[PROOFSTEP]
simp [h]
[GOAL]
case pos
n : ℕ
h : n = 1
⊢ 1 + -1 / 2 = 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case neg
n : ℕ
h : ¬n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
[PROOFSTEP]
simp [h]
[GOAL]
case neg
n : ℕ
h : ¬n = 1
⊢ _root_.bernoulli n = bernoulli' n
[PROOFSTEP]
exact bernoulli_eq_bernoulli'_of_ne_one h
[GOAL]
k : ℕ
⊢ ↑derivative (bernoulli (k + 1)) = (↑k + 1) * bernoulli k
[PROOFSTEP]
simp_rw [bernoulli, derivative_sum, derivative_monomial, Nat.sub_sub, Nat.add_sub_add_right]
  -- LHS sum has an extra term, but the coefficient is zero:
[GOAL]
k : ℕ
⊢ ∑ x in range (k + 1 + 1), ↑(monomial (k - x)) (_root_.bernoulli x * ↑(Nat.choose (k + 1) x) * ↑(k + 1 - x)) =
    (↑k + 1) * ∑ x in range (k + 1), ↑(monomial (k - x)) (_root_.bernoulli x * ↑(Nat.choose k x))
[PROOFSTEP]
rw [range_add_one, sum_insert not_mem_range_self, tsub_self, cast_zero, mul_zero, map_zero, zero_add, mul_sum]
  -- the rest of the sum is termwise equal:
[GOAL]
k : ℕ
⊢ ∑ x in range (k + 1), ↑(monomial (k - x)) (_root_.bernoulli x * ↑(Nat.choose (k + 1) x) * ↑(k + 1 - x)) =
    ∑ x in range (k + 1), (↑k + 1) * ↑(monomial (k - x)) (_root_.bernoulli x * ↑(Nat.choose k x))
[PROOFSTEP]
refine' sum_congr (by rfl) fun m _ => _
[GOAL]
k : ℕ
⊢ range (k + 1) = range (k + 1)
[PROOFSTEP]
rfl
[GOAL]
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose (k + 1) m) * ↑(k + 1 - m)) =
    (↑k + 1) * ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose k m))
[PROOFSTEP]
conv_rhs => rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_nat_cast, C_mul_monomial, mul_comm]
[GOAL]
k m : ℕ
x✝ : m ∈ range (k + 1)
| (↑k + 1) * ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose k m))
[PROOFSTEP]
rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_nat_cast, C_mul_monomial, mul_comm]
[GOAL]
k m : ℕ
x✝ : m ∈ range (k + 1)
| (↑k + 1) * ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose k m))
[PROOFSTEP]
rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_nat_cast, C_mul_monomial, mul_comm]
[GOAL]
k m : ℕ
x✝ : m ∈ range (k + 1)
| (↑k + 1) * ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose k m))
[PROOFSTEP]
rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_nat_cast, C_mul_monomial, mul_comm]
[GOAL]
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose (k + 1) m) * ↑(k + 1 - m)) =
    ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose k m) * ↑(k + 1))
[PROOFSTEP]
rw [mul_assoc, mul_assoc, ← Nat.cast_mul, ← Nat.cast_mul]
[GOAL]
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose (k + 1) m * (k + 1 - m))) =
    ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose k m * (k + 1)))
[PROOFSTEP]
congr 3
[GOAL]
case h.e_6.h.e_a.e_a
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ Nat.choose (k + 1) m * (k + 1 - m) = Nat.choose k m * (k + 1)
[PROOFSTEP]
rw [(choose_mul_succ_eq k m).symm, mul_comm]
[GOAL]
k : ℕ
⊢ ↑derivative (bernoulli k) = ↑k * bernoulli (k - 1)
[PROOFSTEP]
cases k with
| zero => rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
| succ k => exact_mod_cast derivative_bernoulli_add_one k
[GOAL]
k : ℕ
⊢ ↑derivative (bernoulli k) = ↑k * bernoulli (k - 1)
[PROOFSTEP]
cases k with
| zero => rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
| succ k => exact_mod_cast derivative_bernoulli_add_one k
[GOAL]
case zero
⊢ ↑derivative (bernoulli Nat.zero) = ↑Nat.zero * bernoulli (Nat.zero - 1)
[PROOFSTEP]

| zero => rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
[GOAL]
case zero
⊢ ↑derivative (bernoulli Nat.zero) = ↑Nat.zero * bernoulli (Nat.zero - 1)
[PROOFSTEP]
rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
[GOAL]
case succ
k : ℕ
⊢ ↑derivative (bernoulli (succ k)) = ↑(succ k) * bernoulli (succ k - 1)
[PROOFSTEP]

| succ k => exact_mod_cast derivative_bernoulli_add_one k
[GOAL]
case succ
k : ℕ
⊢ ↑derivative (bernoulli (succ k)) = ↑(succ k) * bernoulli (succ k - 1)
[PROOFSTEP]
exact_mod_cast derivative_bernoulli_add_one k
[GOAL]
n : ℕ
⊢ ∑ k in range (n + 1), ↑(Nat.choose (n + 1) k) • bernoulli k = ↑(monomial n) (↑n + 1)
[PROOFSTEP]
simp_rw [bernoulli_def, Finset.smul_sum, Finset.range_eq_Ico, ← Finset.sum_Ico_Ico_comm, Finset.sum_Ico_eq_sum_range]
[GOAL]
n : ℕ
⊢ ∑ k in range (n + 1 - 0),
      ∑ k_1 in range (n + 1 - (0 + k)),
        ↑(Nat.choose (n + 1) (0 + k + k_1)) •
          ↑(monomial (0 + k)) (_root_.bernoulli (0 + k + k_1 - (0 + k)) * ↑(Nat.choose (0 + k + k_1) (0 + k))) =
    ↑(monomial n) (↑n + 1)
[PROOFSTEP]
simp only [add_tsub_cancel_left, tsub_zero, zero_add, map_add]
[GOAL]
n : ℕ
⊢ ∑ x in range (n + 1),
      ∑ x_1 in range (n + 1 - x),
        ↑(Nat.choose (n + 1) (x + x_1)) • ↑(monomial x) (_root_.bernoulli x_1 * ↑(Nat.choose (x + x_1) x)) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
[PROOFSTEP]
simp_rw [smul_monomial, mul_comm (_root_.bernoulli _) _, smul_eq_mul, ← mul_assoc]
[GOAL]
n : ℕ
⊢ ∑ x in range (n + 1),
      ∑ x_1 in range (n + 1 - x),
        ↑(monomial x) (↑(Nat.choose (n + 1) (x + x_1)) * ↑(Nat.choose (x + x_1) x) * _root_.bernoulli x_1) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
[PROOFSTEP]
conv_lhs =>
  apply_congr
  ·skip
  ·conv =>
      apply_congr
      ·skip
      ·rw [← Nat.cast_mul,
          choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption))
            (le.intro rfl),
          Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
[GOAL]
n : ℕ
| ∑ x in range (n + 1),
    ∑ x_1 in range (n + 1 - x),
      ↑(monomial x) (↑(Nat.choose (n + 1) (x + x_1)) * ↑(Nat.choose (x + x_1) x) * _root_.bernoulli x_1)
[PROOFSTEP]
  apply_congr
  ·skip
  ·conv =>
      apply_congr
      ·skip
      ·rw [← Nat.cast_mul,
          choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption))
            (le.intro rfl),
          Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
[GOAL]
n : ℕ
| ∑ x in range (n + 1),
    ∑ x_1 in range (n + 1 - x),
      ↑(monomial x) (↑(Nat.choose (n + 1) (x + x_1)) * ↑(Nat.choose (x + x_1) x) * _root_.bernoulli x_1)
[PROOFSTEP]
  apply_congr
  ·skip
  ·conv =>
      apply_congr
      ·skip
      ·rw [← Nat.cast_mul,
          choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption))
            (le.intro rfl),
          Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
[GOAL]
n : ℕ
| ∑ x in range (n + 1),
    ∑ x_1 in range (n + 1 - x),
      ↑(monomial x) (↑(Nat.choose (n + 1) (x + x_1)) * ↑(Nat.choose (x + x_1) x) * _root_.bernoulli x_1)
[PROOFSTEP]
apply_congr
[GOAL]
case h
n : ℕ
⊢ range (n + 1) = ?s₂
case a
n x✝ : ℕ
a✝ : x✝ ∈ ?s₂
⊢ ∑ x in range (n + 1 - x✝),
      ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x) =
    ?g x✝
[PROOFSTEP]
·skip
[GOAL]
case h
n : ℕ
⊢ range (n + 1) = ?s₂
[PROOFSTEP]
skip
[GOAL]
case h
n : ℕ
⊢ range (n + 1) = ?s₂
[PROOFSTEP]
skip
[GOAL]
case h
n : ℕ
⊢ range (n + 1) = ?s₂
[PROOFSTEP]
skip
[GOAL]
case a
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ ∑ x in range (n + 1 - x✝),
      ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x) =
    ?g x✝
[PROOFSTEP]
·conv =>
    apply_congr
    ·skip
    ·rw [← Nat.cast_mul,
        choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption))
          (le.intro rfl),
        Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
[GOAL]
case a
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ ∑ x in range (n + 1 - x✝),
      ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x) =
    ?g x✝
[PROOFSTEP]
conv =>
    apply_congr
    ·skip
    ·rw [← Nat.cast_mul,
        choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption))
          (le.intro rfl),
        Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
[GOAL]
case a
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ ∑ x in range (n + 1 - x✝),
      ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x) =
    ?g x✝
[PROOFSTEP]
conv =>
    apply_congr
    ·skip
    ·rw [← Nat.cast_mul,
        choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption))
          (le.intro rfl),
        Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
[GOAL]
case a
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ ∑ x in range (n + 1 - x✝),
      ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x) =
    ?g x✝
[PROOFSTEP]
conv =>
  apply_congr
  ·skip
  ·rw [← Nat.cast_mul,
      choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption)) (le.intro rfl),
      Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
[GOAL]
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
| ∑ x in range (n + 1 - x✝),
    ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x)
[PROOFSTEP]
  apply_congr
  ·skip
  ·rw [← Nat.cast_mul,
      choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption)) (le.intro rfl),
      Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
[GOAL]
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
| ∑ x in range (n + 1 - x✝),
    ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x)
[PROOFSTEP]
apply_congr
[GOAL]
case h
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ range (n + 1 - x✝) = ?s₂
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ ?s₂
⊢ ↑(monomial x✝¹) (↑(Nat.choose (n + 1) (x✝¹ + x✝)) * ↑(Nat.choose (x✝¹ + x✝) x✝¹) * _root_.bernoulli x✝) = ?g x✝
[PROOFSTEP]
·skip
[GOAL]
case h
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ range (n + 1 - x✝) = ?s₂
[PROOFSTEP]
skip
[GOAL]
case h
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ range (n + 1 - x✝) = ?s₂
[PROOFSTEP]
skip
[GOAL]
case h
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ range (n + 1 - x✝) = ?s₂
[PROOFSTEP]
skip
[GOAL]
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ ↑(monomial x✝¹) (↑(Nat.choose (n + 1) (x✝¹ + x✝)) * ↑(Nat.choose (x✝¹ + x✝) x✝¹) * _root_.bernoulli x✝) = ?g x✝
[PROOFSTEP]
·rw [← Nat.cast_mul,
    choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption)) (le.intro rfl),
    Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
[GOAL]
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ ↑(monomial x✝¹) (↑(Nat.choose (n + 1) (x✝¹ + x✝)) * ↑(Nat.choose (x✝¹ + x✝) x✝¹) * _root_.bernoulli x✝) = ?g x✝
[PROOFSTEP]
rw [← Nat.cast_mul,
    choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption)) (le.intro rfl),
    Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
[GOAL]
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ ↑(monomial x✝¹) (↑(Nat.choose (n + 1) (x✝¹ + x✝)) * ↑(Nat.choose (x✝¹ + x✝) x✝¹) * _root_.bernoulli x✝) = ?g x✝
[PROOFSTEP]
rw [← Nat.cast_mul,
    choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption)) (le.intro rfl),
    Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
[GOAL]
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ ↑(monomial x✝¹) (↑(Nat.choose (n + 1) (x✝¹ + x✝)) * ↑(Nat.choose (x✝¹ + x✝) x✝¹) * _root_.bernoulli x✝) = ?g x✝
[PROOFSTEP]
rw [← Nat.cast_mul,
  choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption)) (le.intro rfl),
  Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
[GOAL]
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ x✝¹ ∈ range (n + 1)
[PROOFSTEP]
assumption
[GOAL]
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ x✝ ∈ range (n + 1 - x✝¹)
[PROOFSTEP]
assumption
[GOAL]
n : ℕ
⊢ ∑ x in range (n + 1),
      ∑ x_1 in range (n + 1 - x),
        (↑(Nat.choose (n + 1 - x) x_1) * _root_.bernoulli x_1) • ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
[PROOFSTEP]
simp_rw [← sum_smul]
[GOAL]
n : ℕ
⊢ ∑ x in range (n + 1),
      (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
        ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
[PROOFSTEP]
rw [sum_range_succ_comm]
[GOAL]
n : ℕ
⊢ (∑ i in range (n + 1 - n), ↑(Nat.choose (n + 1 - n) i) * _root_.bernoulli i) • ↑(monomial n) ↑(Nat.choose (n + 1) n) +
      ∑ x in range n,
        (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
          ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
[PROOFSTEP]
simp only [add_right_eq_self, mul_one, cast_one, cast_add, add_tsub_cancel_left, choose_succ_self_right, one_smul,
  _root_.bernoulli_zero, sum_singleton, zero_add, map_add, range_one, bernoulli_zero, mul_one, one_mul, add_zero,
  choose_self]
[GOAL]
n : ℕ
⊢ ∑ x in range n,
      (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
        ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    0
[PROOFSTEP]
apply sum_eq_zero fun x hx => _
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range n →
      (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
          ↑(monomial x) ↑(Nat.choose (n + 1) x) =
        0
[PROOFSTEP]
have f : ∀ x ∈ range n, ¬n + 1 - x = 1 := by
  rintro x H
  rw [mem_range] at H
  rw [eq_comm]
  exact _root_.ne_of_lt (Nat.lt_of_lt_of_le one_lt_two (le_tsub_of_add_le_left (succ_le_succ H)))
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
[PROOFSTEP]
rintro x H
[GOAL]
n x : ℕ
H : x ∈ range n
⊢ ¬n + 1 - x = 1
[PROOFSTEP]
rw [mem_range] at H
[GOAL]
n x : ℕ
H : x < n
⊢ ¬n + 1 - x = 1
[PROOFSTEP]
rw [eq_comm]
[GOAL]
n x : ℕ
H : x < n
⊢ ¬1 = n + 1 - x
[PROOFSTEP]
exact _root_.ne_of_lt (Nat.lt_of_lt_of_le one_lt_two (le_tsub_of_add_le_left (succ_le_succ H)))
[GOAL]
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
⊢ ∀ (x : ℕ),
    x ∈ range n →
      (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
          ↑(monomial x) ↑(Nat.choose (n + 1) x) =
        0
[PROOFSTEP]
intro x hx
[GOAL]
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
⊢ (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) • ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    0
[PROOFSTEP]
rw [sum_bernoulli]
[GOAL]
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
⊢ (if n + 1 - x = 1 then 1 else 0) • ↑(monomial x) ↑(Nat.choose (n + 1) x) = 0
[PROOFSTEP]
have g : ite (n + 1 - x = 1) (1 : ℚ) 0 = 0 :=
  by
  simp only [ite_eq_right_iff, one_ne_zero]
  intro h₁
  exact (f x hx) h₁
[GOAL]
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
⊢ (if n + 1 - x = 1 then 1 else 0) = 0
[PROOFSTEP]
simp only [ite_eq_right_iff, one_ne_zero]
[GOAL]
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
⊢ n + 1 - x = 1 → False
[PROOFSTEP]
intro h₁
[GOAL]
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
h₁ : n + 1 - x = 1
⊢ False
[PROOFSTEP]
exact (f x hx) h₁
[GOAL]
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
g : (if n + 1 - x = 1 then 1 else 0) = 0
⊢ (if n + 1 - x = 1 then 1 else 0) • ↑(monomial x) ↑(Nat.choose (n + 1) x) = 0
[PROOFSTEP]
rw [g, zero_smul]
[GOAL]
n : ℕ
⊢ ↑(succ n) • bernoulli n = ↑(monomial n) ↑(succ n) - ∑ k in range n, ↑(Nat.choose (n + 1) k) • bernoulli k
[PROOFSTEP]
rw [Nat.cast_succ, ← sum_bernoulli n, sum_range_succ, add_sub_cancel', choose_succ_self_right, Nat.cast_succ]
[GOAL]
n p : ℕ
⊢ (↑p + 1) * ∑ k in range n, ↑k ^ p = eval (↑n) (bernoulli (succ p)) - _root_.bernoulli (succ p)
[PROOFSTEP]
rw [sum_range_pow, bernoulli_def, eval_finset_sum, ← sum_div, mul_div_cancel' _ _]
[GOAL]
n p : ℕ
⊢ ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) =
    ∑ i in range (succ p + 1), eval (↑n) (↑(monomial i) (_root_.bernoulli (succ p - i) * ↑(Nat.choose (succ p) i))) -
      _root_.bernoulli (succ p)
[PROOFSTEP]
simp_rw [eval_monomial]
[GOAL]
n p : ℕ
⊢ ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) =
    ∑ x in range (succ p + 1), _root_.bernoulli (succ p - x) * ↑(Nat.choose (succ p) x) * ↑n ^ x -
      _root_.bernoulli (succ p)
[PROOFSTEP]
symm
[GOAL]
n p : ℕ
⊢ ∑ x in range (succ p + 1), _root_.bernoulli (succ p - x) * ↑(Nat.choose (succ p) x) * ↑n ^ x -
      _root_.bernoulli (succ p) =
    ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
[PROOFSTEP]
rw [← sum_flip _, sum_range_succ]
[GOAL]
n p : ℕ
⊢ ∑ x in range (p + 1),
          _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) +
        _root_.bernoulli (succ p - (p + 1 - (p + 1))) * ↑(Nat.choose (succ p) (p + 1 - (p + 1))) *
          ↑n ^ (p + 1 - (p + 1)) -
      _root_.bernoulli (succ p) =
    ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
[PROOFSTEP]
simp only [tsub_self, tsub_zero, choose_zero_right, cast_one, mul_one, _root_.pow_zero, add_tsub_cancel_right]
[GOAL]
n p : ℕ
⊢ ∑ x in range (p + 1),
      _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) =
    ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
[PROOFSTEP]
apply sum_congr rfl fun x hx => _
[GOAL]
n p : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range (p + 1) →
      _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) =
        _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
[PROOFSTEP]
intro x hx
[GOAL]
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) =
    _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
[PROOFSTEP]
apply congr_arg₂ _ (congr_arg₂ _ _ _) rfl
[GOAL]
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (succ p - (p + 1 - x)) = _root_.bernoulli x
[PROOFSTEP]
rw [Nat.sub_sub_self (mem_range_le hx)]
[GOAL]
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ ↑(Nat.choose (succ p) (p + 1 - x)) = ↑(Nat.choose (p + 1) x)
[PROOFSTEP]
rw [← choose_symm (mem_range_le hx)]
[GOAL]
n p : ℕ
⊢ ↑p + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
n p : ℕ
⊢ ¬p + 1 = 0
[PROOFSTEP]
apply succ_ne_zero _
[GOAL]
n p : ℕ
⊢ eval (↑n) (bernoulli (succ p)) = _root_.bernoulli (succ p) + (↑p + 1) * ∑ k in range n, ↑k ^ p
[PROOFSTEP]
apply eq_add_of_sub_eq'
[GOAL]
case h
n p : ℕ
⊢ eval (↑n) (bernoulli (succ p)) - _root_.bernoulli (succ p) = (↑p + 1) * ∑ k in range n, ↑k ^ p
[PROOFSTEP]
rw [sum_range_pow_eq_bernoulli_sub]
[GOAL]
n : ℕ
x : ℚ
⊢ eval (1 + x) (bernoulli n) = eval x (bernoulli n) + ↑n * x ^ (n - 1)
[PROOFSTEP]
refine' Nat.strong_induction_on n fun d hd => _
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
⊢ eval (1 + x) (bernoulli d) = eval x (bernoulli d) + ↑d * x ^ (d - 1)
[PROOFSTEP]
have nz : ((d.succ : ℕ) : ℚ) ≠ 0 := by norm_cast
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
⊢ ↑(succ d) ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (bernoulli d) = eval x (bernoulli d) + ↑d * x ^ (d - 1)
[PROOFSTEP]
apply (mul_right_inj' nz).1
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ ↑(succ d) * eval (1 + x) (bernoulli d) = ↑(succ d) * (eval x (bernoulli d) + ↑d * x ^ (d - 1))
[PROOFSTEP]
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]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (↑(monomial d) ↑(succ d)) - ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i) =
    eval x (↑(monomial d) ↑(succ d) - ∑ k in range d, ↑(Nat.choose (d + 1) k) • bernoulli k) +
      ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
conv_lhs =>
  congr
  ·skip
  · apply_congr
    ·skip
    ·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d)) - ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
  congr
  ·skip
  · apply_congr
    ·skip
    ·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d)) - ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
  congr
  ·skip
  · apply_congr
    ·skip
    ·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d)) - ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
congr
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d))
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
·skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d))
[PROOFSTEP]
skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d))
[PROOFSTEP]
skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d))
[PROOFSTEP]
skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
· apply_congr
  ·skip
  ·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
  apply_congr
  ·skip
  ·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
  apply_congr
  ·skip
  ·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
apply_congr
[GOAL]
case a.h
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ range d = ?a.s₂
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ ?a.s₂
⊢ eval (1 + x) (↑(Nat.choose (d + 1) x✝) • bernoulli x✝) = ?a.g x✝
[PROOFSTEP]
·skip
[GOAL]
case a.h
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ range d = ?a.s₂
[PROOFSTEP]
skip
[GOAL]
case a.h
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ range d = ?a.s₂
[PROOFSTEP]
skip
[GOAL]
case a.h
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ range d = ?a.s₂
[PROOFSTEP]
skip
[GOAL]
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range d
⊢ eval (1 + x) (↑(Nat.choose (d + 1) x✝) • bernoulli x✝) = ?a.g x✝
[PROOFSTEP]
·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range d
⊢ eval (1 + x) (↑(Nat.choose (d + 1) x✝) • bernoulli x✝) = ?a.g x✝
[PROOFSTEP]
rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range d
⊢ eval (1 + x) (↑(Nat.choose (d + 1) x✝) • bernoulli x✝) = ?a.g x✝
[PROOFSTEP]
rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range d
⊢ eval (1 + x) (↑(Nat.choose (d + 1) x✝) • bernoulli x✝) = ?a.g x✝
[PROOFSTEP]
rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range d
⊢ x✝ ∈ range d
[PROOFSTEP]
assumption
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (↑(monomial d) ↑(succ d)) -
      ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (eval x (bernoulli x_1) + ↑x_1 * x ^ (x_1 - 1)) =
    eval x (↑(monomial d) ↑(succ d) - ∑ k in range d, ↑(Nat.choose (d + 1) k) • bernoulli k) +
      ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
rw [eval_sub, eval_finset_sum]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (↑(monomial d) ↑(succ d)) -
      ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (eval x (bernoulli x_1) + ↑x_1 * x ^ (x_1 - 1)) =
    eval x (↑(monomial d) ↑(succ d)) - ∑ i in range d, eval x (↑(Nat.choose (d + 1) i) • bernoulli i) +
      ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
simp_rw [eval_smul, smul_add]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (↑(monomial d) ↑(succ d)) -
      ∑ x_1 in range d,
        (↑(Nat.choose (d + 1) x_1) • eval x (bernoulli x_1) + ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1))) =
    eval x (↑(monomial d) ↑(succ d)) - ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • eval x (bernoulli x_1) +
      ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
rw [sum_add_distrib, sub_add, sub_eq_sub_iff_sub_eq_sub, _root_.add_sub_sub_cancel]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (↑(monomial d) ↑(succ d)) - eval x (↑(monomial d) ↑(succ d)) =
    ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1)) + ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
conv_rhs =>
  congr
  ·skip
  · congr
    rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1)) + ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
  congr
  ·skip
  · congr
    rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1)) + ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
  congr
  ·skip
  · congr
    rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1)) + ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
congr
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1))
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
·skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1))
[PROOFSTEP]
skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1))
[PROOFSTEP]
skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1))
[PROOFSTEP]
skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
· congr
  rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
  congr
  rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
  congr
  rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
congr
[GOAL]
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑(succ d)
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑d * x ^ (d - 1)
[PROOFSTEP]
rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (↑(monomial d) ↑(succ d)) - eval x (↑(monomial d) ↑(succ d)) =
    ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1)) + ↑(Nat.choose (d + 1) d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
rw [Nat.cast_succ, ← smul_eq_mul, ← sum_range_succ _ d, eval_monomial_one_add_sub]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) * (↑x_1 * x ^ (x_1 - 1)) =
    ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1))
[PROOFSTEP]
simp_rw [smul_eq_mul]
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
⊢ (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1) = PowerSeries.X * ↑(rescale t) (exp A)
[PROOFSTEP]
ext n
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ↑(PowerSeries.coeff A n) ((PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    ↑(PowerSeries.coeff A n) (PowerSeries.X * ↑(rescale t) (exp A))
[PROOFSTEP]
cases' n with n
[GOAL]
case h.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
⊢ ↑(PowerSeries.coeff A Nat.zero) ((PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    ↑(PowerSeries.coeff A Nat.zero) (PowerSeries.X * ↑(rescale t) (exp A))
[PROOFSTEP]
simp
  -- n ≥ 1, the coefficients is a sum to n+2, so use `sum_range_succ` to write as
    -- last term plus sum to n+1
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ↑(PowerSeries.coeff A (succ n)) ((PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    ↑(PowerSeries.coeff A (succ n)) (PowerSeries.X * ↑(rescale t) (exp A))
[PROOFSTEP]
rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, PowerSeries.coeff_mul, Nat.sum_antidiagonal_eq_sum_range_succ_mk,
  sum_range_succ]
  -- last term is zero so kill with `add_zero`
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x in range (n + 1),
        ↑(PowerSeries.coeff A (x, succ n - x).fst) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
          ↑(PowerSeries.coeff A (x, succ n - x).snd) (exp A - 1) +
      ↑(PowerSeries.coeff A (n + 1, succ n - (n + 1)).fst)
          (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
        ↑(PowerSeries.coeff A (n + 1, succ n - (n + 1)).snd) (exp A - 1) =
    t ^ n * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
simp only [RingHom.map_sub, tsub_self, constantCoeff_one, constantCoeff_exp, coeff_zero_eq_constantCoeff, mul_zero,
  sub_self, add_zero]
  -- Let's multiply both sides by (n+1)! (OK because it's a unit)
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x in range (n + 1),
      ↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
        ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1) =
    t ^ n * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
have hnp1 : IsUnit ((n + 1)! : ℚ) := IsUnit.mk0 _ (by exact_mod_cast factorial_ne_zero (n + 1))
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ↑(n + 1)! ≠ 0
[PROOFSTEP]
exact_mod_cast factorial_ne_zero (n + 1)
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ∑ x in range (n + 1),
      ↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
        ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1) =
    t ^ n * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
rw [← (hnp1.map (algebraMap ℚ A)).mul_right_inj]
  -- do trivial rearrangements to make RHS (n+1)*t^n
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ↑(algebraMap ℚ A) ↑(n + 1)! *
      ∑ x in range (n + 1),
        ↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
          ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1) =
    ↑(algebraMap ℚ A) ↑(n + 1)! * (t ^ n * ↑(algebraMap ℚ A) (1 / ↑n !))
[PROOFSTEP]
rw [mul_left_comm, ← RingHom.map_mul]
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ↑(algebraMap ℚ A) ↑(n + 1)! *
      ∑ x in range (n + 1),
        ↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
          ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1) =
    t ^ n * ↑(algebraMap ℚ A) (↑(n + 1)! * (1 / ↑n !))
[PROOFSTEP]
change _ = t ^ n * algebraMap ℚ A (((n + 1) * n ! : ℕ) * (1 / n !))
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ↑(algebraMap ℚ A) ↑(n + 1)! *
      ∑ x in range (n + 1),
        ↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
          ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1) =
    t ^ n * ↑(algebraMap ℚ A) (↑((n + 1) * n !) * (1 / ↑n !))
[PROOFSTEP]
rw [cast_mul, mul_assoc, mul_one_div_cancel (show (n ! : ℚ) ≠ 0 from cast_ne_zero.2 (factorial_ne_zero n)), mul_one,
  mul_comm (t ^ n), ← aeval_monomial, cast_add, cast_one]
  -- But this is the RHS of `Polynomial.sum_bernoulli`
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ↑(algebraMap ℚ A) ↑(n + 1)! *
      ∑ x in range (n + 1),
        ↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
          ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1) =
    ↑(aeval t) (↑(monomial n) (↑n + 1))
[PROOFSTEP]
rw [← sum_bernoulli, Finset.mul_sum, AlgHom.map_sum]
  -- and now we have to prove a sum is a sum, but all the terms are equal.
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ∑ x in range (n + 1),
      ↑(algebraMap ℚ A) ↑(n + 1)! *
        (↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
          ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1)) =
    ∑ x in range (n + 1), ↑(aeval t) (↑(Nat.choose (n + 1) x) • bernoulli x)
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ∀ (x : ℕ),
    x ∈ range (n + 1) →
      ↑(algebraMap ℚ A) ↑(n + 1)! *
          (↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
            ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1)) =
        ↑(aeval t) (↑(Nat.choose (n + 1) x) • bernoulli x)
[PROOFSTEP]
intro i hi
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
i : ℕ
hi : i ∈ range (n + 1)
⊢ ↑(algebraMap ℚ A) ↑(n + 1)! *
      (↑(PowerSeries.coeff A i) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
        ↑(PowerSeries.coeff A (succ n - i)) (exp A - 1)) =
    ↑(aeval t) (↑(Nat.choose (n + 1) i) • bernoulli i)
[PROOFSTEP]
simp only [Nat.cast_choose ℚ (mem_range_le hi), coeff_mk, if_neg (mem_range_sub_ne_zero hi), one_div, AlgHom.map_smul,
  PowerSeries.coeff_one, coeff_exp, sub_zero, LinearMap.map_sub, Algebra.smul_mul_assoc, Algebra.smul_def,
  mul_right_comm _ ((aeval t) _), ← mul_assoc, ← RingHom.map_mul, succ_eq_add_one, ← Polynomial.C_eq_algebraMap,
  Polynomial.aeval_mul, Polynomial.aeval_C]
  -- finally cancel the Bernoulli polynomial and the algebra_map
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
i : ℕ
hi : i ∈ range (n + 1)
⊢ ↑(algebraMap ℚ A) (↑(n + 1)! * (↑i !)⁻¹ * (↑(n + 1 - i)!)⁻¹) * ↑(aeval t) (bernoulli i) =
    ↑(algebraMap ℚ A) (↑(n + 1)! / (↑i ! * ↑(n + 1 - i)!)) * ↑(aeval t) (bernoulli i)
[PROOFSTEP]
field_simp


[GOAL]
z : ℂ
⊢ LSeriesSummable 0 z
[PROOFSTEP]
simp [LSeriesSummable, summable_zero]
[GOAL]
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
⊢ LSeriesSummable f ↑z
[PROOFSTEP]
by_cases h0 : m = 0
[GOAL]
case pos
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : m = 0
⊢ LSeriesSummable f ↑z
[PROOFSTEP]
subst h0
[GOAL]
case pos
f : ArithmeticFunction ℂ
z : ℝ
hz : 1 < z
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ 0
⊢ LSeriesSummable f ↑z
[PROOFSTEP]
have hf : f = 0 := ArithmeticFunction.ext fun n => Complex.abs.eq_zero.1 (le_antisymm (h n) (Complex.abs.nonneg _))
[GOAL]
case pos
f : ArithmeticFunction ℂ
z : ℝ
hz : 1 < z
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ 0
hf : f = 0
⊢ LSeriesSummable f ↑z
[PROOFSTEP]
simp [hf]
[GOAL]
case neg
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ LSeriesSummable f ↑z
[PROOFSTEP]
refine' summable_of_norm_bounded (fun n : ℕ => m / n ^ z) _ _
[GOAL]
case neg.refine'_1
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ Summable fun n => m / ↑n ^ z
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
case neg.refine'_1
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ Summable fun n => m * (↑n ^ z)⁻¹
[PROOFSTEP]
exact (summable_mul_left_iff h0).2 (Real.summable_nat_rpow_inv.2 hz)
[GOAL]
case neg.refine'_2
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
⊢ ∀ (i : ℕ), ‖↑f i / ↑i ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) i
[PROOFSTEP]
intro n
[GOAL]
case neg.refine'_2
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
n : ℕ
⊢ ‖↑f n / ↑n ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) n
[PROOFSTEP]
have hm : 0 ≤ m := le_trans (Complex.abs.nonneg _) (h 0)
[GOAL]
case neg.refine'_2
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
n : ℕ
hm : 0 ≤ m
⊢ ‖↑f n / ↑n ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) n
[PROOFSTEP]
cases' n with n
[GOAL]
case neg.refine'_2.zero
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
hm : 0 ≤ m
⊢ ‖↑f Nat.zero / ↑Nat.zero ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) Nat.zero
[PROOFSTEP]
simp [hm, Real.zero_rpow (_root_.ne_of_gt (lt_trans Real.zero_lt_one hz))]
[GOAL]
case neg.refine'_2.succ
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
hm : 0 ≤ m
n : ℕ
⊢ ‖↑f (succ n) / ↑(succ n) ^ ↑z‖ ≤ (fun n => m / ↑n ^ z) (succ n)
[PROOFSTEP]
simp only [map_div₀, Complex.norm_eq_abs]
[GOAL]
case neg.refine'_2.succ
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
hm : 0 ≤ m
n : ℕ
⊢ ↑Complex.abs (↑f (succ n)) / ↑Complex.abs (↑(succ n) ^ ↑z) ≤ m / ↑(succ n) ^ z
[PROOFSTEP]
apply div_le_div hm (h _) (Real.rpow_pos_of_pos (Nat.cast_pos.2 n.succ_pos) _) (le_of_eq _)
[GOAL]
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℝ
hz : 1 < z
h0 : ¬m = 0
hm : 0 ≤ m
n : ℕ
⊢ ↑(succ n) ^ z = ↑Complex.abs (↑(succ n) ^ ↑z)
[PROOFSTEP]
rw [Complex.abs_cpow_real, Complex.abs_cast_nat]
[GOAL]
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
⊢ LSeriesSummable f w ↔ LSeriesSummable f z
[PROOFSTEP]
suffices h : ∀ n : ℕ, Complex.abs (f n) / Complex.abs (↑n ^ w) = Complex.abs (f n) / Complex.abs (↑n ^ z)
[GOAL]
f : ArithmeticFunction ℂ
w z : ℂ
h✝ : w.re = z.re
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ w) = ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ z)
⊢ LSeriesSummable f w ↔ LSeriesSummable f z
[PROOFSTEP]
simp [LSeriesSummable, ← summable_norm_iff, h, Complex.norm_eq_abs]
[GOAL]
case h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
⊢ ∀ (n : ℕ), ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ w) = ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ z)
[PROOFSTEP]
intro n
[GOAL]
case h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ w) = ↑Complex.abs (↑f n) / ↑Complex.abs (↑n ^ z)
[PROOFSTEP]
cases' n with n
[GOAL]
case h.zero
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
⊢ ↑Complex.abs (↑f Nat.zero) / ↑Complex.abs (↑Nat.zero ^ w) = ↑Complex.abs (↑f Nat.zero) / ↑Complex.abs (↑Nat.zero ^ z)
[PROOFSTEP]
simp
[GOAL]
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑Complex.abs (↑f (succ n)) / ↑Complex.abs (↑(succ n) ^ w) = ↑Complex.abs (↑f (succ n)) / ↑Complex.abs (↑(succ n) ^ z)
[PROOFSTEP]
apply congr rfl
[GOAL]
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑Complex.abs (↑(succ n) ^ w) = ↑Complex.abs (↑(succ n) ^ z)
[PROOFSTEP]
have h0 : (n.succ : ℂ) ≠ 0 := by
  rw [Ne.def, Nat.cast_eq_zero]
  apply n.succ_ne_zero
[GOAL]
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ↑(succ n) ≠ 0
[PROOFSTEP]
rw [Ne.def, Nat.cast_eq_zero]
[GOAL]
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
⊢ ¬succ n = 0
[PROOFSTEP]
apply n.succ_ne_zero
[GOAL]
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ ↑Complex.abs (↑(succ n) ^ w) = ↑Complex.abs (↑(succ n) ^ z)
[PROOFSTEP]
rw [Complex.cpow_def, Complex.cpow_def, if_neg h0, if_neg h0, Complex.abs_exp_eq_iff_re_eq]
[GOAL]
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ (Complex.log ↑(succ n) * w).re = (Complex.log ↑(succ n) * z).re
[PROOFSTEP]
simp only [h, Complex.mul_re, mul_eq_mul_left_iff, sub_right_inj]
[GOAL]
case h.succ
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ w.im = z.im ∨ (Complex.log ↑(succ n)).im = 0
[PROOFSTEP]
right
[GOAL]
case h.succ.h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ (Complex.log ↑(succ n)).im = 0
[PROOFSTEP]
rw [Complex.log_im, ← Complex.ofReal_nat_cast]
[GOAL]
case h.succ.h
f : ArithmeticFunction ℂ
w z : ℂ
h : w.re = z.re
n : ℕ
h0 : ↑(succ n) ≠ 0
⊢ Complex.arg ↑↑(succ n) = 0
[PROOFSTEP]
exact Complex.arg_ofReal_of_nonneg (le_of_lt (cast_pos.2 n.succ_pos))
[GOAL]
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℂ
hz : 1 < z.re
⊢ LSeriesSummable f z
[PROOFSTEP]
rw [← LSeriesSummable_iff_of_re_eq_re (Complex.ofReal_re z.re)]
[GOAL]
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℂ
hz : 1 < z.re
⊢ LSeriesSummable f ↑z.re
[PROOFSTEP]
apply LSeriesSummable_of_bounded_of_one_lt_real h
[GOAL]
f : ArithmeticFunction ℂ
m : ℝ
h : ∀ (n : ℕ), ↑Complex.abs (↑f n) ≤ m
z : ℂ
hz : 1 < z.re
⊢ 1 < z.re
[PROOFSTEP]
exact hz
[GOAL]
z : ℂ
⊢ LSeriesSummable (↑ζ) z ↔ 1 < z.re
[PROOFSTEP]
rw [← LSeriesSummable_iff_of_re_eq_re (Complex.ofReal_re z.re), LSeriesSummable, ← summable_norm_iff, ←
  Real.summable_one_div_nat_rpow, iff_iff_eq]
[GOAL]
z : ℂ
⊢ (Summable fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = Summable fun n => 1 / ↑n ^ z.re
[PROOFSTEP]
by_cases h0 : z.re = 0
[GOAL]
case pos
z : ℂ
h0 : z.re = 0
⊢ (Summable fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = Summable fun n => 1 / ↑n ^ z.re
[PROOFSTEP]
rw [h0, ← summable_nat_add_iff 1]
[GOAL]
case pos
z : ℂ
h0 : z.re = 0
⊢ (Summable fun n => ‖↑↑ζ (n + 1) / ↑(n + 1) ^ ↑0‖) = Summable fun n => 1 / ↑n ^ 0
[PROOFSTEP]
apply congr rfl
[GOAL]
case pos
z : ℂ
h0 : z.re = 0
⊢ (fun n => ‖↑↑ζ (n + 1) / ↑(n + 1) ^ ↑0‖) = fun n => 1 / ↑n ^ 0
[PROOFSTEP]
ext n
[GOAL]
case pos.h
z : ℂ
h0 : z.re = 0
n : ℕ
⊢ ‖↑↑ζ (n + 1) / ↑(n + 1) ^ ↑0‖ = 1 / ↑n ^ 0
[PROOFSTEP]
simp [n.succ_ne_zero]
[GOAL]
case neg
z : ℂ
h0 : ¬z.re = 0
⊢ (Summable fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = Summable fun n => 1 / ↑n ^ z.re
[PROOFSTEP]
apply congr rfl
[GOAL]
case neg
z : ℂ
h0 : ¬z.re = 0
⊢ (fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = fun n => 1 / ↑n ^ z.re
[PROOFSTEP]
ext ⟨- | n⟩
[GOAL]
case neg.h.zero
z : ℂ
h0 : ¬z.re = 0
⊢ ‖↑↑ζ Nat.zero / ↑Nat.zero ^ ↑z.re‖ = 1 / ↑Nat.zero ^ z.re
[PROOFSTEP]
simp [h0]
[GOAL]
case neg.h.succ
z : ℂ
h0 : ¬z.re = 0
n✝ : ℕ
⊢ ‖↑↑ζ (succ n✝) / ↑(succ n✝) ^ ↑z.re‖ = 1 / ↑(succ n✝) ^ z.re
[PROOFSTEP]
simp only [cast_zero, natCoe_apply, zeta_apply, succ_ne_zero, if_false, cast_succ, one_div, Complex.norm_eq_abs,
  map_inv₀, Complex.abs_cpow_real, inv_inj, zero_add]
[GOAL]
case neg.h.succ
z : ℂ
h0 : ¬z.re = 0
n✝ : ℕ
⊢ ↑Complex.abs (↑n✝ + 1) ^ z.re = (↑n✝ + 1) ^ z.re
[PROOFSTEP]
rw [← cast_one, ← cast_add, Complex.abs_of_nat, cast_add, cast_one]
[GOAL]
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ LSeries (f + g) z = LSeries f z + LSeries g z
[PROOFSTEP]
simp only [LSeries, add_apply]
[GOAL]
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ ∑' (n : ℕ), (↑f n + ↑g n) / ↑n ^ z = ∑' (n : ℕ), ↑f n / ↑n ^ z + ∑' (n : ℕ), ↑g n / ↑n ^ z
[PROOFSTEP]
rw [← tsum_add hf hg]
[GOAL]
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ ∑' (n : ℕ), (↑f n + ↑g n) / ↑n ^ z = ∑' (b : ℕ), (↑f b / ↑b ^ z + ↑g b / ↑b ^ z)
[PROOFSTEP]
apply congr rfl (funext fun n => _)
[GOAL]
f g : ArithmeticFunction ℂ
z : ℂ
hf : LSeriesSummable f z
hg : LSeriesSummable g z
⊢ ∀ (n : ℕ), (↑f n + ↑g n) / ↑n ^ z = ↑f n / ↑n ^ z + ↑g n / ↑n ^ z
[PROOFSTEP]
simp [_root_.add_div]