rw [mem_Ioc] at hx
N : ℕ
hN : 1 ≤ N
this : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
x : ℕ
hx : x ∈ Ioc 1 N
⊢ ∑ d ∈ x.divisors, μ d = 0
N : ℕ
hN : 1 ≤ N
this : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
x : ℕ
hx : 1 < x ∧ x ≤ N
⊢ ∑ d ∈ x.divisors, μ d = 0