How to reproduce this result from Wolfram Functions site?

Question

Reading this Wolfram Functions page for hypergeometric $_2F_1$ function, I'm trying to reproduce this result with Mathematica. But not only doesn't it expand the function when appropriate assumptions are given, it doesn't even evaluate the statement to true (I took it from Input Form on the above linked page and replaced /; with ,):

FullSimplify[Hypergeometric2F1[1/2, n, 1 + n, z] == 
  n!/(z^n Pochhammer[1/2, n])-((2 n Sqrt[1-z])/z) Sum[(Pochhammer[1-n, k] (1-1/z)^k)/
      Pochhammer[3/2, k], {k, 0, n - 1}], Element[n, Integers] && n >= 0]

Hypergeometric2F1[1/2, n, 1 + n, z] + ( 2 n Sqrt[1 - z] Hypergeometric2F1[1, 1 - n, 3/2, (-1 + z)/z])/z == ( z^-n n!)/Pochhammer[1/2, n]

At the same time, making a table of these FullSimplify statements with n varying from e.g. 0 to 10 I do get a list of Trues.

This looks a bit strange, since I'd suppose all the knowledge base of Wolfram Functions should be built-in into Mathematica.

So, how to convince Mathematica that the statement is true in general? And ultimately, how to make it output such expansions directly (so that I could learn from it, not just check something I already know)?

Answer 1

A common trick is to use DifferenceRootReduce[] on the difference of the left and right-hand sides:

iden = Hypergeometric2F1[1/2, n, 1 + n, z] == n!/(z^n Pochhammer[1/2, n]) -
(2 n Sqrt[1 - z]/z) Sum[Pochhammer[1 - n, k] (1 - 1/z)^k/Pochhammer[3/2, k],
                        {k, 0, n - 1}];

DifferenceRootReduce[Subtract @@ iden, n]
   0

---

This looks a bit strange, since I'd suppose all the knowledge base of MathWorld should be built-in into Mathematica.

— in Alpha, I would think so; Mathematica, not so much. MathematicalFunctionData[] gives a nice pile, but I've noticed that a fair number of the relations it has are not necessarily easily recognized by Mathematica to be true.