Theorem: ArithmeticFunction.sum_Icc_mul_zeta (PrimeNumberTheoremAnd/Mathlib/NumberTheory/ArithmeticFunction.lean)

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d
Tactic:
have := sum_range_mul_zeta f N
State after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ d ∈ range (N + 1), (N / d) • f d
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ d ∈ range (N + 1), (N / d) • f d
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d
Tactic:
rw [range_eq_Ico, ← Ico_insert_succ_left, sum_insert, sum_insert] at this
State after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = (N / 0) • f 0 + ∑ x ∈ Ico (succ 0) (N + 1), (N / x) • f x
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = (N / 0) • f 0 + ∑ x ∈ Ico (succ 0) (N + 1), (N / x) • f x
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1
Tactic:
simp only [Ico_succ_right, reduceSucc, Nat.div_zero, smul_zero, map_zero, zero_add] at this
State after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ x ∈ Icc 1 N, (f * ↑ζ) x = ∑ x ∈ Icc 1 N, (N / x) • f x
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ x ∈ Icc 1 N, (f * ↑ζ) x = ∑ x ∈ Icc 1 N, (N / x) • f x
⊢ ∑ d ∈ Icc 1 N, (f * ↑ζ) d = ∑ d ∈ Icc 1 N, (N / d) • f d

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1
Tactic:
rw [this]
State after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : (f * ↑ζ) 0 + ∑ x ∈ Ico (succ 0) (N + 1), (f * ↑ζ) x = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (f * ↑ζ) d = ∑ d ∈ insert 0 (Ico (succ 0) (N + 1)), (N / d) • f d
⊢ 0 ∉ Ico (succ 0) (N + 1)

R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1
Tactic:
all_goals simp
State after:
no goals

State before:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
this : ∑ d ∈ Ico 0 (N + 1), (f * ↑ζ) d = ∑ d ∈ Ico 0 (N + 1), (N / d) • f d
⊢ 0 < N + 1
Tactic:
simp
State after:
no goals