I am currently formalising some results from complexity theory with a theorem prover. For that, I have to prove the following statement:


Let $p, b, \varepsilon \in \mathbb R$ with $\varepsilon>0$ and $b \in (0,1)$. Then there exists some $x\_0\in\mathbb R$ such that for all $x \geq x\_0$:


$$\left(1-\frac{1}{b \ln^{1+\varepsilon} x}\right)^p\left(1+\frac{1}{\ln^{\varepsilon/2}\left(bx + \frac{x}{\ln^{1+\varepsilon} x}\right)}\right) \geq 1 + \frac{1}{\ln^{\varepsilon/2} x}$$


The paper from which I have this statement says that this can be shown by Taylor series expansions and asymptotic analysis, but gives no further details.


I have given this a lot of thought, but don't see how I could employ Taylor series or anything else to prove this.



Proving a complicated inequality with powers of logarithms
When $x\to \infty$ we have
$$\left(1-\frac1{b\ln^{1+\epsilon}x}\right)^p = 1 -\frac p{b\ln^{1+\epsilon}x} + o\left(\frac1{\ln^{1+\epsilon}x}\right),$$
and 
$$\frac1{\ln^{\epsilon/2}\left(bx + \frac x{\ln^{1+\epsilon}x}\right)}= (\ln bx)^{-\epsilon/2} \left(\frac1{1+ \frac1{\ln bx} \ln\left(1 + \frac1{b\ln^{1+\epsilon}x}\right)}\right)^{\epsilon/2}= (\ln bx)^{-\epsilon/2} + o\left(\frac1{\ln^{1+\epsilon/2}x}\right).$$
Hence
$$\left(1-\frac1{b\ln^{1+\epsilon}x}\right)^p\left(1+ \frac1{\ln^{\epsilon/2}\left(bx + \frac x{\ln^{1+\epsilon}x}\right)}\right) = 1 + \frac1{(\ln bx)^{\epsilon/2}} + o\left(\frac1{\ln^{1+\epsilon/2}x}\right).$$
The existence of $x\_0$ now follows from the assumption $b\in (0,1)$.


