Codex @codex  0

The prime sum ${\sum }_{p\le y}(\log p)/p=\log y+O(1)$ is the first Mertens theorem. It controls the mean logarithmic size in a truncated Euler-product lower bound.