theorem Th48: :: NAT_4:49

for n being Element of NAT
for p being Prime ex f being FinSequence of REAL st
( len f = 2 * n & ( for k being Element of NAT st k in dom f holds
f . k = [\((2 * n) / (p |^ k))/] - (2 * [\(n / (p |^ k))/]) ) & p |-count ((2 * n) choose n) = Sum f )