Let $p_n$ denote the $n$-th prime number. Does anyone know a proof of the following property?
$$\forall n, n', \ p_n p_{n'} \geq p_{n+n'}$$
I'm surprised I can't find anything on this while I believe it should be something people could find interesting (if it's true). The case $n=1$ (i.e. $p_n=2$) is equivalent to Bertrand's postulate.
Assume $n\leq m$ (here I use $m$ instead of $n'$). By Rosser's theorem we have that $p_np_m>n\ln n\cdot m\ln m=nm\ln n\ln m$. For $n,m>8$ we have $nm\geq\frac{n+4}{2}\cdot m=\frac{1}{2}nm+2m\geq 2n+2m$. We further have for $n>e^2$ $\ln n\ln m>2\ln m=\ln m+\ln m\geq\ln n+\ln m$, so $p_np_m>nm\ln n\ln m> 2(n+m)(\ln n+\ln m)>2(n+m)\ln nm>2(n+m)\ln(n+m)=(n+m)\ln(n+m)+(n+m)\ln(n+m)>(n+m)\ln(n+m)+(n+m)\ln\ln(n+m)>p_{n+m}$ where last equality is one mentioned here and holds for $n+m\geq 6$.
We can use a few explicit improvements over Bertrand found on Wikipedia:
[Nagura 1952] For $x\ge 25$ there is a prime between $x$ and $\frac 65 x$.
Hence if $p_{n}\ge \left(\frac 65\right)^n$ and $p_{n'}>23$ then there are $n$ primes between $p_n'$ and $p_{n}p_{n'}$. Together with finitely many checks for $p_n\le p_{n'}\le 23$ this settles all cases with one of the primes being $<100$ (or equivalently: where at least one of $n,n'$ is $\le 25$). Actually, we need only handle the case that at least one of $n,n'$ is $\le 5$ (i.e. one of $p_n,p_{n'}$ is $\le 11$), because the rest is dealt with by the following nice estimate for the $n$th prime:
Hence $$p_np_{n'}>nn'(\ln(n\ln n)-1)(\ln(n'\ln n')-1)$$ and $$p_{n+n'}<(n+n')\ln((n+n')\ln(n+n')) $$ As we may even assume $n\ge n'\ge6$, we find $$\begin{align} p_{n+n'}&<2n\ln(2n\ln(2n))\\&=2n\ln((2n+\ln2)\ln n)\\&<2n(\ln 3+\ln(n\ln n))\\&<3n\ln(n\ln n))\end{align}$$ and $$\begin{align}p_np_{n'}&>6n(\ln(n\ln n)-1)(\ln(6\ln 6)-1)\\& >13n(\ln(n\ln n)-1)\end{align} $$ So that all we need to complete the proof is $$ 10\ln(n\ln n)>13$$ which is the case because $n\ln n\ge 6\ln 6>10$
