norm_num [Nat.pos_iff_ne_zero.mp hN]
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : (∑ i ∈ range (N + 1), ↑(μ i) / ↑i) * ↑N = 1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)
⊢ ↑N ≠ 0
no goals