no goals
⊢ ↑Λ 0 ≤ Real.log ↑0
simp
n : ℕ
⊢ ↑Λ (n + 1) ≤ ∑ i in divisors (n + 1), ↑Λ i
n : ℕ
⊢ ↑Λ (n + 1) ≤ Real.log ↑(n + 1)
rw [← vonMangoldt_sum]
no goals
n : ℕ
⊢ ↑Λ (n + 1) ≤ ∑ i in divisors (n + 1), ↑Λ i
exact single_le_sum (by exact fun _ _ => vonMangoldt_nonneg)
  (mem_divisors_self _ n.succ_ne_zero)
no goals
n : ℕ
⊢ ∀ (i : ℕ), i ∈ divisors (n + 1) → 0 ≤ ↑Λ i
exact fun _ _ => vonMangoldt_nonneg