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