Metamath Proof Explorer

Theorem basellem5

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 ⊢ 𝑁 = ( ( 2 · 𝑀 ) + 1 )
basel.p ⊢ 𝑃 = ( 𝑡 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) · ( 𝑡 ↑ 𝑗 ) ) )
basel.t ⊢ 𝑇 = ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) )
Assertion basellem5 ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) )

Proof

Step Hyp Ref Expression
1 basel.n ⊢ 𝑁 = ( ( 2 · 𝑀 ) + 1 )
2 basel.p ⊢ 𝑃 = ( 𝑡 ∈ ℂ ↦ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑁 C ( 2 · 𝑗 ) ) · ( - 1 ↑ ( 𝑀 − 𝑗 ) ) ) · ( 𝑡 ↑ 𝑗 ) ) )
3 basel.t ⊢ 𝑇 = ( 𝑛 ∈ ( 1 ... 𝑀 ) ↦ ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) )
4 eqid ⊢ ( coeff ‘ 𝑃 ) = ( coeff ‘ 𝑃 )
5 eqid ⊢ ( deg ‘ 𝑃 ) = ( deg ‘ 𝑃 )
6 eqid ⊢ ( ◡ 𝑃 “ { 0 } ) = ( ◡ 𝑃 “ { 0 } )
7 1 2 basellem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝑃 ) = 𝑀 ∧ ( coeff ‘ 𝑃 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ) )
8 7 simp1d ⊢ ( 𝑀 ∈ ℕ → 𝑃 ∈ ( Poly ‘ ℂ ) )
9 7 simp2d ⊢ ( 𝑀 ∈ ℕ → ( deg ‘ 𝑃 ) = 𝑀 )
10 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
11 hashfz1 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
12 10 11 syl ⊢ ( 𝑀 ∈ ℕ → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
13 fzfid ⊢ ( 𝑀 ∈ ℕ → ( 1 ... 𝑀 ) ∈ Fin )
14 1 2 3 basellem4 ⊢ ( 𝑀 ∈ ℕ → 𝑇 : ( 1 ... 𝑀 ) –1-1-onto→ ( ◡ 𝑃 “ { 0 } ) )
15 13 14 hasheqf1od ⊢ ( 𝑀 ∈ ℕ → ( ♯ ‘ ( 1 ... 𝑀 ) ) = ( ♯ ‘ ( ◡ 𝑃 “ { 0 } ) ) )
16 9 12 15 3eqtr2rd ⊢ ( 𝑀 ∈ ℕ → ( ♯ ‘ ( ◡ 𝑃 “ { 0 } ) ) = ( deg ‘ 𝑃 ) )
17 id ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ )
18 9 17 eqeltrd ⊢ ( 𝑀 ∈ ℕ → ( deg ‘ 𝑃 ) ∈ ℕ )
19 4 5 6 8 16 18 vieta1 ⊢ ( 𝑀 ∈ ℕ → Σ 𝑥 ∈ ( ◡ 𝑃 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑃 ) ‘ ( ( deg ‘ 𝑃 ) − 1 ) ) / ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) ) )
20 id ⊢ ( 𝑥 = ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) → 𝑥 = ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) )
21 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 · π ) = ( 𝑘 · π ) )
22 21 fvoveq1d ⊢ ( 𝑛 = 𝑘 → ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) = ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) )
23 22 oveq1d ⊢ ( 𝑛 = 𝑘 → ( ( tan ‘ ( ( 𝑛 · π ) / 𝑁 ) ) ↑ - 2 ) = ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) )
24 ovex ⊢ ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) ∈ V
25 23 3 24 fvmpt ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → ( 𝑇 ‘ 𝑘 ) = ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) )
26 25 adantl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝑇 ‘ 𝑘 ) = ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) )
27 cnvimass ⊢ ( ◡ 𝑃 “ { 0 } ) ⊆ dom 𝑃
28 plyf ⊢ ( 𝑃 ∈ ( Poly ‘ ℂ ) → 𝑃 : ℂ ⟶ ℂ )
29 fdm ⊢ ( 𝑃 : ℂ ⟶ ℂ → dom 𝑃 = ℂ )
30 8 28 29 3syl ⊢ ( 𝑀 ∈ ℕ → dom 𝑃 = ℂ )
31 27 30 sseqtrid ⊢ ( 𝑀 ∈ ℕ → ( ◡ 𝑃 “ { 0 } ) ⊆ ℂ )
32 31 sselda ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑥 ∈ ( ◡ 𝑃 “ { 0 } ) ) → 𝑥 ∈ ℂ )
33 20 13 14 26 32 fsumf1o ⊢ ( 𝑀 ∈ ℕ → Σ 𝑥 ∈ ( ◡ 𝑃 “ { 0 } ) 𝑥 = Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) )
34 7 simp3d ⊢ ( 𝑀 ∈ ℕ → ( coeff ‘ 𝑃 ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) )
35 9 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( deg ‘ 𝑃 ) − 1 ) = ( 𝑀 − 1 ) )
36 34 35 fveq12d ⊢ ( 𝑀 ∈ ℕ → ( ( coeff ‘ 𝑃 ) ‘ ( ( deg ‘ 𝑃 ) − 1 ) ) = ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ ( 𝑀 − 1 ) ) )
37 nnm1nn0 ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℕ0 )
38 oveq2 ⊢ ( 𝑛 = ( 𝑀 − 1 ) → ( 2 · 𝑛 ) = ( 2 · ( 𝑀 − 1 ) ) )
39 38 oveq2d ⊢ ( 𝑛 = ( 𝑀 − 1 ) → ( 𝑁 C ( 2 · 𝑛 ) ) = ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) )
40 oveq2 ⊢ ( 𝑛 = ( 𝑀 − 1 ) → ( 𝑀 − 𝑛 ) = ( 𝑀 − ( 𝑀 − 1 ) ) )
41 40 oveq2d ⊢ ( 𝑛 = ( 𝑀 − 1 ) → ( - 1 ↑ ( 𝑀 − 𝑛 ) ) = ( - 1 ↑ ( 𝑀 − ( 𝑀 − 1 ) ) ) )
42 39 41 oveq12d ⊢ ( 𝑛 = ( 𝑀 − 1 ) → ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) = ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( - 1 ↑ ( 𝑀 − ( 𝑀 − 1 ) ) ) ) )
43 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) )
44 ovex ⊢ ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( - 1 ↑ ( 𝑀 − ( 𝑀 − 1 ) ) ) ) ∈ V
45 42 43 44 fvmpt ⊢ ( ( 𝑀 − 1 ) ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ ( 𝑀 − 1 ) ) = ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( - 1 ↑ ( 𝑀 − ( 𝑀 − 1 ) ) ) ) )
46 37 45 syl ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ ( 𝑀 − 1 ) ) = ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( - 1 ↑ ( 𝑀 − ( 𝑀 − 1 ) ) ) ) )
47 nncn ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
48 ax-1cn ⊢ 1 ∈ ℂ
49 nncan ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑀 − ( 𝑀 − 1 ) ) = 1 )
50 47 48 49 sylancl ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − ( 𝑀 − 1 ) ) = 1 )
51 50 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( - 1 ↑ ( 𝑀 − ( 𝑀 − 1 ) ) ) = ( - 1 ↑ 1 ) )
52 neg1cn ⊢ - 1 ∈ ℂ
53 exp1 ⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 1 ) = - 1 )
54 52 53 ax-mp ⊢ ( - 1 ↑ 1 ) = - 1
55 51 54 eqtrdi ⊢ ( 𝑀 ∈ ℕ → ( - 1 ↑ ( 𝑀 − ( 𝑀 − 1 ) ) ) = - 1 )
56 55 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( - 1 ↑ ( 𝑀 − ( 𝑀 − 1 ) ) ) ) = ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · - 1 ) )
57 2nn ⊢ 2 ∈ ℕ
58 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 2 · 𝑀 ) ∈ ℕ )
59 57 58 mpan ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ℕ )
60 59 peano2nnd ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) + 1 ) ∈ ℕ )
61 1 60 eqeltrid ⊢ ( 𝑀 ∈ ℕ → 𝑁 ∈ ℕ )
62 61 nnnn0d ⊢ ( 𝑀 ∈ ℕ → 𝑁 ∈ ℕ0 )
63 2z ⊢ 2 ∈ ℤ
64 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
65 peano2zm ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
66 64 65 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℤ )
67 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ ( 𝑀 − 1 ) ∈ ℤ ) → ( 2 · ( 𝑀 − 1 ) ) ∈ ℤ )
68 63 66 67 sylancr ⊢ ( 𝑀 ∈ ℕ → ( 2 · ( 𝑀 − 1 ) ) ∈ ℤ )
69 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 2 · ( 𝑀 − 1 ) ) ∈ ℤ ) → ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ∈ ℕ0 )
70 62 68 69 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ∈ ℕ0 )
71 70 nn0cnd ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ∈ ℂ )
72 mulcom ⊢ ( ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ∈ ℂ ∧ - 1 ∈ ℂ ) → ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · - 1 ) = ( - 1 · ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ) )
73 71 52 72 sylancl ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · - 1 ) = ( - 1 · ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ) )
74 71 mulm1d ⊢ ( 𝑀 ∈ ℕ → ( - 1 · ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ) = - ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) )
75 56 73 74 3eqtrd ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( - 1 ↑ ( 𝑀 − ( 𝑀 − 1 ) ) ) ) = - ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) )
76 36 46 75 3eqtrd ⊢ ( 𝑀 ∈ ℕ → ( ( coeff ‘ 𝑃 ) ‘ ( ( deg ‘ 𝑃 ) − 1 ) ) = - ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) )
77 71 negcld ⊢ ( 𝑀 ∈ ℕ → - ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ∈ ℂ )
78 76 77 eqeltrd ⊢ ( 𝑀 ∈ ℕ → ( ( coeff ‘ 𝑃 ) ‘ ( ( deg ‘ 𝑃 ) − 1 ) ) ∈ ℂ )
79 34 9 fveq12d ⊢ ( 𝑀 ∈ ℕ → ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑀 ) )
80 oveq2 ⊢ ( 𝑛 = 𝑀 → ( 2 · 𝑛 ) = ( 2 · 𝑀 ) )
81 80 oveq2d ⊢ ( 𝑛 = 𝑀 → ( 𝑁 C ( 2 · 𝑛 ) ) = ( 𝑁 C ( 2 · 𝑀 ) ) )
82 oveq2 ⊢ ( 𝑛 = 𝑀 → ( 𝑀 − 𝑛 ) = ( 𝑀 − 𝑀 ) )
83 82 oveq2d ⊢ ( 𝑛 = 𝑀 → ( - 1 ↑ ( 𝑀 − 𝑛 ) ) = ( - 1 ↑ ( 𝑀 − 𝑀 ) ) )
84 81 83 oveq12d ⊢ ( 𝑛 = 𝑀 → ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) = ( ( 𝑁 C ( 2 · 𝑀 ) ) · ( - 1 ↑ ( 𝑀 − 𝑀 ) ) ) )
85 ovex ⊢ ( ( 𝑁 C ( 2 · 𝑀 ) ) · ( - 1 ↑ ( 𝑀 − 𝑀 ) ) ) ∈ V
86 84 43 85 fvmpt ⊢ ( 𝑀 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑀 ) = ( ( 𝑁 C ( 2 · 𝑀 ) ) · ( - 1 ↑ ( 𝑀 − 𝑀 ) ) ) )
87 10 86 syl ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑁 C ( 2 · 𝑛 ) ) · ( - 1 ↑ ( 𝑀 − 𝑛 ) ) ) ) ‘ 𝑀 ) = ( ( 𝑁 C ( 2 · 𝑀 ) ) · ( - 1 ↑ ( 𝑀 − 𝑀 ) ) ) )
88 47 subidd ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 𝑀 ) = 0 )
89 88 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( - 1 ↑ ( 𝑀 − 𝑀 ) ) = ( - 1 ↑ 0 ) )
90 exp0 ⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
91 52 90 ax-mp ⊢ ( - 1 ↑ 0 ) = 1
92 89 91 eqtrdi ⊢ ( 𝑀 ∈ ℕ → ( - 1 ↑ ( 𝑀 − 𝑀 ) ) = 1 )
93 92 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( 2 · 𝑀 ) ) · ( - 1 ↑ ( 𝑀 − 𝑀 ) ) ) = ( ( 𝑁 C ( 2 · 𝑀 ) ) · 1 ) )
94 fz1ssfz0 ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
95 59 nnred ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ℝ )
96 95 lep1d ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ≤ ( ( 2 · 𝑀 ) + 1 ) )
97 96 1 breqtrrdi ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ≤ 𝑁 )
98 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
99 59 98 eleqtrdi ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ( ℤ≥ ‘ 1 ) )
100 61 nnzd ⊢ ( 𝑀 ∈ ℕ → 𝑁 ∈ ℤ )
101 elfz5 ⊢ ( ( ( 2 · 𝑀 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ) → ( ( 2 · 𝑀 ) ∈ ( 1 ... 𝑁 ) ↔ ( 2 · 𝑀 ) ≤ 𝑁 ) )
102 99 100 101 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) ∈ ( 1 ... 𝑁 ) ↔ ( 2 · 𝑀 ) ≤ 𝑁 ) )
103 97 102 mpbird ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ( 1 ... 𝑁 ) )
104 94 103 sselid ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ( 0 ... 𝑁 ) )
105 bccl2 ⊢ ( ( 2 · 𝑀 ) ∈ ( 0 ... 𝑁 ) → ( 𝑁 C ( 2 · 𝑀 ) ) ∈ ℕ )
106 104 105 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · 𝑀 ) ) ∈ ℕ )
107 106 nncnd ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · 𝑀 ) ) ∈ ℂ )
108 107 mulid1d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( 2 · 𝑀 ) ) · 1 ) = ( 𝑁 C ( 2 · 𝑀 ) ) )
109 93 108 eqtrd ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( 2 · 𝑀 ) ) · ( - 1 ↑ ( 𝑀 − 𝑀 ) ) ) = ( 𝑁 C ( 2 · 𝑀 ) ) )
110 79 87 109 3eqtrd ⊢ ( 𝑀 ∈ ℕ → ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) = ( 𝑁 C ( 2 · 𝑀 ) ) )
111 110 107 eqeltrd ⊢ ( 𝑀 ∈ ℕ → ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) ∈ ℂ )
112 106 nnne0d ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · 𝑀 ) ) ≠ 0 )
113 110 112 eqnetrd ⊢ ( 𝑀 ∈ ℕ → ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) ≠ 0 )
114 78 111 113 divnegd ⊢ ( 𝑀 ∈ ℕ → - ( ( ( coeff ‘ 𝑃 ) ‘ ( ( deg ‘ 𝑃 ) − 1 ) ) / ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) ) = ( - ( ( coeff ‘ 𝑃 ) ‘ ( ( deg ‘ 𝑃 ) − 1 ) ) / ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) ) )
115 76 negeqd ⊢ ( 𝑀 ∈ ℕ → - ( ( coeff ‘ 𝑃 ) ‘ ( ( deg ‘ 𝑃 ) − 1 ) ) = - - ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) )
116 71 negnegd ⊢ ( 𝑀 ∈ ℕ → - - ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) = ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) )
117 115 116 eqtrd ⊢ ( 𝑀 ∈ ℕ → - ( ( coeff ‘ 𝑃 ) ‘ ( ( deg ‘ 𝑃 ) − 1 ) ) = ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) )
118 117 110 oveq12d ⊢ ( 𝑀 ∈ ℕ → ( - ( ( coeff ‘ 𝑃 ) ‘ ( ( deg ‘ 𝑃 ) − 1 ) ) / ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) ) = ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) / ( 𝑁 C ( 2 · 𝑀 ) ) ) )
119 bcm1k ⊢ ( ( 2 · 𝑀 ) ∈ ( 1 ... 𝑁 ) → ( 𝑁 C ( 2 · 𝑀 ) ) = ( ( 𝑁 C ( ( 2 · 𝑀 ) − 1 ) ) · ( ( 𝑁 − ( ( 2 · 𝑀 ) − 1 ) ) / ( 2 · 𝑀 ) ) ) )
120 103 119 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · 𝑀 ) ) = ( ( 𝑁 C ( ( 2 · 𝑀 ) − 1 ) ) · ( ( 𝑁 − ( ( 2 · 𝑀 ) − 1 ) ) / ( 2 · 𝑀 ) ) ) )
121 59 nncnd ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ∈ ℂ )
122 1cnd ⊢ ( 𝑀 ∈ ℕ → 1 ∈ ℂ )
123 121 122 122 pnncand ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) + 1 ) − ( ( 2 · 𝑀 ) − 1 ) ) = ( 1 + 1 ) )
124 1 oveq1i ⊢ ( 𝑁 − ( ( 2 · 𝑀 ) − 1 ) ) = ( ( ( 2 · 𝑀 ) + 1 ) − ( ( 2 · 𝑀 ) − 1 ) )
125 df-2 ⊢ 2 = ( 1 + 1 )
126 123 124 125 3eqtr4g ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 − ( ( 2 · 𝑀 ) − 1 ) ) = 2 )
127 2nn0 ⊢ 2 ∈ ℕ0
128 126 127 eqeltrdi ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 − ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℕ0 )
129 nnm1nn0 ⊢ ( ( 2 · 𝑀 ) ∈ ℕ → ( ( 2 · 𝑀 ) − 1 ) ∈ ℕ0 )
130 59 129 syl ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) − 1 ) ∈ ℕ0 )
131 nn0sub ⊢ ( ( ( ( 2 · 𝑀 ) − 1 ) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 2 · 𝑀 ) − 1 ) ≤ 𝑁 ↔ ( 𝑁 − ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℕ0 ) )
132 130 62 131 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) − 1 ) ≤ 𝑁 ↔ ( 𝑁 − ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℕ0 ) )
133 128 132 mpbird ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) − 1 ) ≤ 𝑁 )
134 47 2timesd ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) = ( 𝑀 + 𝑀 ) )
135 134 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) − 1 ) = ( ( 𝑀 + 𝑀 ) − 1 ) )
136 47 47 122 addsubd ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑀 + 𝑀 ) − 1 ) = ( ( 𝑀 − 1 ) + 𝑀 ) )
137 135 136 eqtrd ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) − 1 ) = ( ( 𝑀 − 1 ) + 𝑀 ) )
138 nn0nnaddcl ⊢ ( ( ( 𝑀 − 1 ) ∈ ℕ0 ∧ 𝑀 ∈ ℕ ) → ( ( 𝑀 − 1 ) + 𝑀 ) ∈ ℕ )
139 37 138 mpancom ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑀 − 1 ) + 𝑀 ) ∈ ℕ )
140 137 139 eqeltrd ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) − 1 ) ∈ ℕ )
141 140 98 eleqtrdi ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
142 elfz5 ⊢ ( ( ( ( 2 · 𝑀 ) − 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 2 · 𝑀 ) − 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 2 · 𝑀 ) − 1 ) ≤ 𝑁 ) )
143 141 100 142 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) − 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 2 · 𝑀 ) − 1 ) ≤ 𝑁 ) )
144 133 143 mpbird ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) − 1 ) ∈ ( 1 ... 𝑁 ) )
145 bcm1k ⊢ ( ( ( 2 · 𝑀 ) − 1 ) ∈ ( 1 ... 𝑁 ) → ( 𝑁 C ( ( 2 · 𝑀 ) − 1 ) ) = ( ( 𝑁 C ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) ) · ( ( 𝑁 − ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) ) / ( ( 2 · 𝑀 ) − 1 ) ) ) )
146 144 145 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( ( 2 · 𝑀 ) − 1 ) ) = ( ( 𝑁 C ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) ) · ( ( 𝑁 − ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) ) / ( ( 2 · 𝑀 ) − 1 ) ) ) )
147 48 2timesi ⊢ ( 2 · 1 ) = ( 1 + 1 )
148 147 eqcomi ⊢ ( 1 + 1 ) = ( 2 · 1 )
149 148 oveq2i ⊢ ( ( 2 · 𝑀 ) − ( 1 + 1 ) ) = ( ( 2 · 𝑀 ) − ( 2 · 1 ) )
150 121 122 122 subsub4d ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) = ( ( 2 · 𝑀 ) − ( 1 + 1 ) ) )
151 2cnd ⊢ ( 𝑀 ∈ ℕ → 2 ∈ ℂ )
152 151 47 122 subdid ⊢ ( 𝑀 ∈ ℕ → ( 2 · ( 𝑀 − 1 ) ) = ( ( 2 · 𝑀 ) − ( 2 · 1 ) ) )
153 149 150 152 3eqtr4a ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) = ( 2 · ( 𝑀 − 1 ) ) )
154 153 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) ) = ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) )
155 61 nncnd ⊢ ( 𝑀 ∈ ℕ → 𝑁 ∈ ℂ )
156 140 nncnd ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) − 1 ) ∈ ℂ )
157 155 156 122 subsubd ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 − ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) ) = ( ( 𝑁 − ( ( 2 · 𝑀 ) − 1 ) ) + 1 ) )
158 126 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 − ( ( 2 · 𝑀 ) − 1 ) ) + 1 ) = ( 2 + 1 ) )
159 df-3 ⊢ 3 = ( 2 + 1 )
160 158 159 eqtr4di ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 − ( ( 2 · 𝑀 ) − 1 ) ) + 1 ) = 3 )
161 157 160 eqtrd ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 − ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) ) = 3 )
162 161 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 − ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) ) / ( ( 2 · 𝑀 ) − 1 ) ) = ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) )
163 154 162 oveq12d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) ) · ( ( 𝑁 − ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) ) / ( ( 2 · 𝑀 ) − 1 ) ) ) = ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) ) )
164 146 163 eqtrd ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( ( 2 · 𝑀 ) − 1 ) ) = ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) ) )
165 126 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 − ( ( 2 · 𝑀 ) − 1 ) ) / ( 2 · 𝑀 ) ) = ( 2 / ( 2 · 𝑀 ) ) )
166 164 165 oveq12d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( ( 2 · 𝑀 ) − 1 ) ) · ( ( 𝑁 − ( ( 2 · 𝑀 ) − 1 ) ) / ( 2 · 𝑀 ) ) ) = ( ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) ) · ( 2 / ( 2 · 𝑀 ) ) ) )
167 3re ⊢ 3 ∈ ℝ
168 nndivre ⊢ ( ( 3 ∈ ℝ ∧ ( ( 2 · 𝑀 ) − 1 ) ∈ ℕ ) → ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℝ )
169 167 140 168 sylancr ⊢ ( 𝑀 ∈ ℕ → ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℝ )
170 169 recnd ⊢ ( 𝑀 ∈ ℕ → ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℂ )
171 2re ⊢ 2 ∈ ℝ
172 nndivre ⊢ ( ( 2 ∈ ℝ ∧ ( 2 · 𝑀 ) ∈ ℕ ) → ( 2 / ( 2 · 𝑀 ) ) ∈ ℝ )
173 171 59 172 sylancr ⊢ ( 𝑀 ∈ ℕ → ( 2 / ( 2 · 𝑀 ) ) ∈ ℝ )
174 173 recnd ⊢ ( 𝑀 ∈ ℕ → ( 2 / ( 2 · 𝑀 ) ) ∈ ℂ )
175 71 170 174 mulassd ⊢ ( 𝑀 ∈ ℕ → ( ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) ) · ( 2 / ( 2 · 𝑀 ) ) ) = ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) · ( 2 / ( 2 · 𝑀 ) ) ) ) )
176 120 166 175 3eqtrd ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · 𝑀 ) ) = ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) · ( 2 / ( 2 · 𝑀 ) ) ) ) )
177 3cn ⊢ 3 ∈ ℂ
178 177 a1i ⊢ ( 𝑀 ∈ ℕ → 3 ∈ ℂ )
179 140 nnne0d ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) − 1 ) ≠ 0 )
180 59 nnne0d ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) ≠ 0 )
181 178 156 151 121 179 180 divmuldivd ⊢ ( 𝑀 ∈ ℕ → ( ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) · ( 2 / ( 2 · 𝑀 ) ) ) = ( ( 3 · 2 ) / ( ( ( 2 · 𝑀 ) − 1 ) · ( 2 · 𝑀 ) ) ) )
182 3t2e6 ⊢ ( 3 · 2 ) = 6
183 182 a1i ⊢ ( 𝑀 ∈ ℕ → ( 3 · 2 ) = 6 )
184 156 121 mulcomd ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) − 1 ) · ( 2 · 𝑀 ) ) = ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) )
185 183 184 oveq12d ⊢ ( 𝑀 ∈ ℕ → ( ( 3 · 2 ) / ( ( ( 2 · 𝑀 ) − 1 ) · ( 2 · 𝑀 ) ) ) = ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) )
186 181 185 eqtrd ⊢ ( 𝑀 ∈ ℕ → ( ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) · ( 2 / ( 2 · 𝑀 ) ) ) = ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) )
187 186 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( ( 3 / ( ( 2 · 𝑀 ) − 1 ) ) · ( 2 / ( 2 · 𝑀 ) ) ) ) = ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) ) )
188 176 187 eqtrd ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · 𝑀 ) ) = ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) ) )
189 188 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( 2 · 𝑀 ) ) / ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ) = ( ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) ) / ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ) )
190 6re ⊢ 6 ∈ ℝ
191 59 140 nnmulcld ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℕ )
192 nndivre ⊢ ( ( 6 ∈ ℝ ∧ ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℕ ) → ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) ∈ ℝ )
193 190 191 192 sylancr ⊢ ( 𝑀 ∈ ℕ → ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) ∈ ℝ )
194 193 recnd ⊢ ( 𝑀 ∈ ℕ → ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) ∈ ℂ )
195 nnm1nn0 ⊢ ( ( ( 2 · 𝑀 ) − 1 ) ∈ ℕ → ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) ∈ ℕ0 )
196 140 195 syl ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) ∈ ℕ0 )
197 153 196 eqeltrrd ⊢ ( 𝑀 ∈ ℕ → ( 2 · ( 𝑀 − 1 ) ) ∈ ℕ0 )
198 197 nn0red ⊢ ( 𝑀 ∈ ℕ → ( 2 · ( 𝑀 − 1 ) ) ∈ ℝ )
199 140 nnred ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) − 1 ) ∈ ℝ )
200 61 nnred ⊢ ( 𝑀 ∈ ℕ → 𝑁 ∈ ℝ )
201 199 ltm1d ⊢ ( 𝑀 ∈ ℕ → ( ( ( 2 · 𝑀 ) − 1 ) − 1 ) < ( ( 2 · 𝑀 ) − 1 ) )
202 153 201 eqbrtrrd ⊢ ( 𝑀 ∈ ℕ → ( 2 · ( 𝑀 − 1 ) ) < ( ( 2 · 𝑀 ) − 1 ) )
203 198 199 202 ltled ⊢ ( 𝑀 ∈ ℕ → ( 2 · ( 𝑀 − 1 ) ) ≤ ( ( 2 · 𝑀 ) − 1 ) )
204 198 199 200 203 133 letrd ⊢ ( 𝑀 ∈ ℕ → ( 2 · ( 𝑀 − 1 ) ) ≤ 𝑁 )
205 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
206 197 205 eleqtrdi ⊢ ( 𝑀 ∈ ℕ → ( 2 · ( 𝑀 − 1 ) ) ∈ ( ℤ≥ ‘ 0 ) )
207 elfz5 ⊢ ( ( ( 2 · ( 𝑀 − 1 ) ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( 2 · ( 𝑀 − 1 ) ) ∈ ( 0 ... 𝑁 ) ↔ ( 2 · ( 𝑀 − 1 ) ) ≤ 𝑁 ) )
208 206 100 207 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · ( 𝑀 − 1 ) ) ∈ ( 0 ... 𝑁 ) ↔ ( 2 · ( 𝑀 − 1 ) ) ≤ 𝑁 ) )
209 204 208 mpbird ⊢ ( 𝑀 ∈ ℕ → ( 2 · ( 𝑀 − 1 ) ) ∈ ( 0 ... 𝑁 ) )
210 bccl2 ⊢ ( ( 2 · ( 𝑀 − 1 ) ) ∈ ( 0 ... 𝑁 ) → ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ∈ ℕ )
211 209 210 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ∈ ℕ )
212 211 nnne0d ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ≠ 0 )
213 194 71 212 divcan3d ⊢ ( 𝑀 ∈ ℕ → ( ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) · ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) ) / ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ) = ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) )
214 189 213 eqtrd ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( 2 · 𝑀 ) ) / ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ) = ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) )
215 214 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( 1 / ( ( 𝑁 C ( 2 · 𝑀 ) ) / ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ) ) = ( 1 / ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) ) )
216 107 71 112 212 recdivd ⊢ ( 𝑀 ∈ ℕ → ( 1 / ( ( 𝑁 C ( 2 · 𝑀 ) ) / ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) ) ) = ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) / ( 𝑁 C ( 2 · 𝑀 ) ) ) )
217 191 nncnd ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℂ )
218 191 nnne0d ⊢ ( 𝑀 ∈ ℕ → ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ≠ 0 )
219 6cn ⊢ 6 ∈ ℂ
220 6nn ⊢ 6 ∈ ℕ
221 220 nnne0i ⊢ 6 ≠ 0
222 recdiv ⊢ ( ( ( 6 ∈ ℂ ∧ 6 ≠ 0 ) ∧ ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℂ ∧ ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ≠ 0 ) ) → ( 1 / ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) )
223 219 221 222 mpanl12 ⊢ ( ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ∈ ℂ ∧ ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ≠ 0 ) → ( 1 / ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) )
224 217 218 223 syl2anc ⊢ ( 𝑀 ∈ ℕ → ( 1 / ( 6 / ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) ) ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) )
225 215 216 224 3eqtr3d ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 C ( 2 · ( 𝑀 − 1 ) ) ) / ( 𝑁 C ( 2 · 𝑀 ) ) ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) )
226 114 118 225 3eqtrd ⊢ ( 𝑀 ∈ ℕ → - ( ( ( coeff ‘ 𝑃 ) ‘ ( ( deg ‘ 𝑃 ) − 1 ) ) / ( ( coeff ‘ 𝑃 ) ‘ ( deg ‘ 𝑃 ) ) ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) )
227 19 33 226 3eqtr3d ⊢ ( 𝑀 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( tan ‘ ( ( 𝑘 · π ) / 𝑁 ) ) ↑ - 2 ) = ( ( ( 2 · 𝑀 ) · ( ( 2 · 𝑀 ) − 1 ) ) / 6 ) )