Thank you. I recognize the relation of my problem to the Binomial Expansion:
In[18]:= FullSimplify[
Binomial[n, k] FactorialPower[1/2, k] FactorialPower[1/2, n - k] ==
n!*Binomial[1/2, k]*Binomial[1/2, n - k]]
Out[18]= True
and that equation I can prove easily.
Curiously---but not essentially to my line of inquiry---Mathematica doesn't solve the sum when I express it more like the Binomial Expansion:
In[13]:= FullSimplify[n!*Binomial[1/2, k]*Binomial[1/2, n - k]]
Out[13]= Binomial[1/2, k] Binomial[1/2, -k + n] n!
or more simply:
In[13]:= FullSimplify[Binomial[1/2, k]*Binomial[1/2, n - k]]
Out[13]= Binomial[1/2, k] Binomial[1/2, -k + n] n!
I could solve my problem (finding a proof as described in my initial post) by working through an analysis textbook; but what I'm really after is a proof that doesn't rely on derivatives. A proof modeled after (e.g.) Rudin would make heavy use of derivatives and Taylor's Theorem, which I'm trying to avoid.
I was hoping Mathematica could help me find such a proof, but my hope is a long shot, as Mathematica seems to excel at calculating true answers, but less so at providing proofs.