## Return to Answer

2 fix minor error

You can apply WZ theory to such identities. In particular, both sides satisfy $$x*z''(x) + (x+1)z'(x)$$ Picking $x=1$ as the initial condition (since the DE is regular there, that helps), we see that both sides evaluate to $Ei(1,1)$ and their derivatives both evaluate to $\frac{e^{-x}}{x}$, -1/e$, so they are equal. I got that differential equation using Maple's PDEtools[dpolyform] function, which uses Groebner bases over differential polynomials to 'solve' this problem. All the rest is classical analysis (as in A course of modern analysis by Whittaker and Watson, 1926 - which is unfortunately not material that is taught very much anymore, I certainly had to learn a lot of that 'on my own'). [Edit: fixed an error in the evaluation of the derivative, I pasted in the wrong line] 1 You can apply WZ theory to such identities. In particular, both sides satisfy $$x*z''(x) + (x+1)z'(x)$$ Picking$x=1$as the initial condition (since the DE is regular there, that helps), we see that both sides evaluate to$Ei(1,1)$and their derivatives both evaluate to$\frac{e^{-x}}{x}\$, so they are equal.

I got that differential equation using Maple's PDEtools[dpolyform] function, which uses Groebner bases over differential polynomials to 'solve' this problem. All the rest is classical analysis (as in A course of modern analysis by Whittaker and Watson, 1926 - which is unfortunately not material that is taught very much anymore, I certainly had to learn a lot of that 'on my own').