Description: Lemma for basel . Using vieta1 , we can calculate the sum of the roots of P as the quotient of the top two coefficients, and since the function T enumerates the roots, we are left with an equation that sums the cot ^ 2 function at the M different roots. (Contributed by Mario Carneiro, 29-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | basel.n | |
|
basel.p | |
||
basel.t | |
||
Assertion | basellem5 | |