n : ℕ
⊢ 0 ≤ if IsPrimePow n then Real.log ↑(minFac n) else 0
n : ℕ
⊢ 0 ≤ ↑Λ n
rw [vonMangoldt_apply]
case inl
n : ℕ
h✝ : IsPrimePow n
⊢ 0 ≤ Real.log ↑(minFac n)

case inr
n : ℕ
h✝ : ¬IsPrimePow n
⊢ 0 ≤ 0
n : ℕ
⊢ 0 ≤ if IsPrimePow n then Real.log ↑(minFac n) else 0
split_ifs
no goals
case inr
n : ℕ
h✝ : ¬IsPrimePow n
⊢ 0 ≤ 0
rfl
no goals
case inl
n : ℕ
h✝ : IsPrimePow n
⊢ 0 ≤ Real.log ↑(minFac n)
exact Real.log_nonneg (one_le_cast.2 (Nat.minFac_pos n))