Theorem: finsum_range_eq_sum_range (PrimeNumberTheoremAnd/Consequences.lean)

State before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
⊢ ∑ᶠ (n : ℕ) (_ : ↑n < x), f n = ∑ n ∈ range ⌈x⌉₊, f n
Tactic:
apply finsum_cond_eq_sum_of_cond_iff f
State after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
⊢ ∀ {x_1 : ℕ}, f x_1 ≠ 0 → (↑x_1 < x ↔ x_1 ∈ range ⌈x⌉₊)

State before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
⊢ ∀ {x_1 : ℕ}, f x_1 ≠ 0 → (↑x_1 < x ↔ x_1 ∈ range ⌈x⌉₊)
Tactic:
intros
State after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
x✝ : ℕ
a✝ : f x✝ ≠ 0
⊢ ↑x✝ < x ↔ x✝ ∈ range ⌈x⌉₊

State before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
x✝ : ℕ
a✝ : f x✝ ≠ 0
⊢ ↑x✝ < x ↔ x✝ ∈ range ⌈x⌉₊
Tactic:
simp only [mem_range]
State after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
x✝ : ℕ
a✝ : f x✝ ≠ 0
⊢ ↑x✝ < x ↔ x✝ < ⌈x⌉₊

State before:
R : Type u_1
inst✝ : AddCommMonoid R
f : ArithmeticFunction R
x : ℝ
x✝ : ℕ
a✝ : f x✝ ≠ 0
⊢ ↑x✝ < x ↔ x✝ < ⌈x⌉₊
Tactic:
exact Iff.symm Nat.lt_ceil
State after:
no goals