show/hide this revision's text 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]
show/hide this revision's text 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').