proof that $4^x$ exceeds the product of the primes up to $x$

Statement. (Erdős & Surányi) Given the prime counting function $\pi (x)$ and notating the $i$th prime as $p_i$, the inequality

$$4^x>\prod _{i=1}^{\pi (x)}{p}_i$$

is always true for any nonnegative $x$. In other words, the $x$th power of 4 is greater than the primorial $\pi (x)\mathrm{\#}$.

Note: $\lfloor x\rfloor$ is the integer nearest to the real number $x$ that’s not greater than $x$, while $\lceil x\rceil$ is the nearest integer to $x$ that’s not smaller than $x$.

Proof. It takes very little computational effort to verify this is true for $x$ set to 1 or 2. For larger $x$ we can high-ball the primorial $\pi (x)\mathrm{\#}$ as

$$2\prod _{i=1}^{\lceil \frac{x}{2}\rceil }2i+1$$

(that is, twice the product of the odd numbers from 1 to $x$) and rephrase $4^x$ as

$$2\prod _{i=1}^{2x-1}2.$$

The first factor is obviously the same for both expressions, both iterators have the same start value, but cleary the iterator end values satisfy the inequality $(2x-1)>\lceil \frac{x}{2}\rceil$ as long as $x>2$. The first expression being iteratively multiplied clearly increases, but the second expression being iteratively multiplied is static (being a 2). This line of thought has failed to yield the desired result.

What if instead we divide both expressions by 2 and take their base 2 logarithms? Obviously, for half $4^x$,

$${\log }_2\left(\prod _{i=1}^{2x-1}2\right)=2x-1,$$

giving us the sequence of odd numbers 1, 3, 5, 7, 9, 11, 13, 15, 17, 19, etc. Not quite so obviously, for half our primorial high-ball, the base 2 logarithm is

$$\frac{\log (\lceil \frac{x}{2}\rceil !!)}{log(2)},$$

(where $\log (x)$ is the natural logarithm and $n!!$ is the double factorial), giving us the sequence (to 5 decimal places) 0, 1.58496, 1.58496, 3.90689, 3.90689, 6.71425, 6.71425, 9.88417, 9.88417, 13.3436, 13.3436, 17.044, 17.044, 20.9509, 20.9509, 25.0384, 25.0384, 29.2863, 29.2863, etc.

Unfortunately, both of these strategies are doomed to failure because eventually our high-ball for the primorial overtakes $4^x$. What Erdős and Surányi do instead is rephrase $x$ as $x=2n+1$ and then construct the binomial coefficient $\left(\genfrac{}{}{0pt}{}{}{2n+1n}\right)$ and showing the relationship of this to $2^x$.