Résolution en nombres naturels

Je ne suis pas certain que tu t'y prennes bien pour minorer $\pi(x)$. Ta première inéquation provient sans doute de $p_k \geqslant x$ et, de là, tu veux minorer $\pi(x)$, c'est-à-dire que tu fais le chemin habituel à l'envers.

Ces équations ou inéquations transcendantes sont délicates à manipuler, et il faut souvent faire des concessions. Là, tu demandes une précision assez grande, pas facile à obtenir.

Simplifions, en prenant par exemple la majoration $p_k < 2k \log k$ vraie pour tout $k \geqslant 3$ : on se ramène alors à résoudre l'inéquation $k \log k \geqslant \frac{1}{2} x$. Si $k_0(x) > 1$ est la solution de l'équation $k \log k = \frac{1}{2} x$, alors les solutions de l'inéquations sont données par $k \geqslant k_0(x)$. Or il est connu que, pour $x > 2e$
$$\frac{x}{2\log (x/2)} < k_0(x) < (1+e^{-1}) \frac{x}{2\log (x/2)}$$
donc $k \log k \geqslant \frac{1}{2} x \Longrightarrow k > \frac{x}{2\log (x/2)}$.

Une référence :

F. W. J. Olver, Asymptotics and Special Functions, Academic Press, Inc, 1974, Theorem 5.1 page 13.

Je subodore que ce genre de résolution ne consiste qu'en des implications et non pas des équivalences. Ça semble trop compliqué à résoudre pour obtenir une équivalence, mais je peux me tromper.