Suppose I already know that Mertens' third theorem holds in the form $$\prod_{p\leq x} \left(1 - \frac{1}{p}\right) = \frac{C}{\ln x} + O\left(\frac{1}{\ln^2 x}\right)$$ for some constant $C$. I wonder what the easiest way is to show that $C = e^{-\gamma}$.
I do have access to the various equivalent forms of the Prime Number Theorem, basic facts about Dirichlet series, to the fact that $\lim_{s\to 1} \zeta(s) - \frac{1}{s-1} = \gamma$, and to the $\Gamma$ function (including its derivatives and the relation to $\gamma$). Perhaps that helps? (by the heuristic that ‘it has $\gamma$ in it as well’)
The background to this perhaps rather odd question is that I am trying to formalise these things in a proof assistant.