simp [mem_Ico_iff_div hx]
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
⊢ ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
⊢ ∀ (n : ℕ), (a ≤ ↑n / x → b ≤ ↑n / x) → f n = 0 ∨ (a ≤ ↑n / x → b ≤ ↑n / x)