| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . 3
⊢
(coeff‘𝑃) =
(coeff‘𝑃) | 
| 2 |  | eqid 2736 | . . 3
⊢
(deg‘𝑃) =
(deg‘𝑃) | 
| 3 |  | eqid 2736 | . . 3
⊢ (◡𝑃 “ {0}) = (◡𝑃 “ {0}) | 
| 4 |  | basel.n | . . . . 5
⊢ 𝑁 = ((2 · 𝑀) + 1) | 
| 5 |  | basel.p | . . . . 5
⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗))) | 
| 6 | 4, 5 | basellem2 27126 | . . . 4
⊢ (𝑀 ∈ ℕ → (𝑃 ∈ (Poly‘ℂ)
∧ (deg‘𝑃) = 𝑀 ∧ (coeff‘𝑃) = (𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛)))))) | 
| 7 | 6 | simp1d 1142 | . . 3
⊢ (𝑀 ∈ ℕ → 𝑃 ∈
(Poly‘ℂ)) | 
| 8 | 6 | simp2d 1143 | . . . 4
⊢ (𝑀 ∈ ℕ →
(deg‘𝑃) = 𝑀) | 
| 9 |  | nnnn0 12535 | . . . . 5
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) | 
| 10 |  | hashfz1 14386 | . . . . 5
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) | 
| 11 | 9, 10 | syl 17 | . . . 4
⊢ (𝑀 ∈ ℕ →
(♯‘(1...𝑀)) =
𝑀) | 
| 12 |  | fzfid 14015 | . . . . 5
⊢ (𝑀 ∈ ℕ →
(1...𝑀) ∈
Fin) | 
| 13 |  | basel.t | . . . . . 6
⊢ 𝑇 = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) | 
| 14 | 4, 5, 13 | basellem4 27128 | . . . . 5
⊢ (𝑀 ∈ ℕ → 𝑇:(1...𝑀)–1-1-onto→(◡𝑃 “ {0})) | 
| 15 | 12, 14 | hasheqf1od 14393 | . . . 4
⊢ (𝑀 ∈ ℕ →
(♯‘(1...𝑀)) =
(♯‘(◡𝑃 “ {0}))) | 
| 16 | 8, 11, 15 | 3eqtr2rd 2783 | . . 3
⊢ (𝑀 ∈ ℕ →
(♯‘(◡𝑃 “ {0})) = (deg‘𝑃)) | 
| 17 |  | id 22 | . . . 4
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ) | 
| 18 | 8, 17 | eqeltrd 2840 | . . 3
⊢ (𝑀 ∈ ℕ →
(deg‘𝑃) ∈
ℕ) | 
| 19 | 1, 2, 3, 7, 16, 18 | vieta1 26355 | . 2
⊢ (𝑀 ∈ ℕ →
Σ𝑥 ∈ (◡𝑃 “ {0})𝑥 = -(((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃)))) | 
| 20 |  | id 22 | . . 3
⊢ (𝑥 = ((tan‘((𝑘 · π) / 𝑁))↑-2) → 𝑥 = ((tan‘((𝑘 · π) / 𝑁))↑-2)) | 
| 21 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛 · π) = (𝑘 · π)) | 
| 22 | 21 | fvoveq1d 7454 | . . . . . 6
⊢ (𝑛 = 𝑘 → (tan‘((𝑛 · π) / 𝑁)) = (tan‘((𝑘 · π) / 𝑁))) | 
| 23 | 22 | oveq1d 7447 | . . . . 5
⊢ (𝑛 = 𝑘 → ((tan‘((𝑛 · π) / 𝑁))↑-2) = ((tan‘((𝑘 · π) / 𝑁))↑-2)) | 
| 24 |  | ovex 7465 | . . . . 5
⊢
((tan‘((𝑘
· π) / 𝑁))↑-2) ∈ V | 
| 25 | 23, 13, 24 | fvmpt 7015 | . . . 4
⊢ (𝑘 ∈ (1...𝑀) → (𝑇‘𝑘) = ((tan‘((𝑘 · π) / 𝑁))↑-2)) | 
| 26 | 25 | adantl 481 | . . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑇‘𝑘) = ((tan‘((𝑘 · π) / 𝑁))↑-2)) | 
| 27 |  | cnvimass 6099 | . . . . 5
⊢ (◡𝑃 “ {0}) ⊆ dom 𝑃 | 
| 28 |  | plyf 26238 | . . . . . 6
⊢ (𝑃 ∈ (Poly‘ℂ)
→ 𝑃:ℂ⟶ℂ) | 
| 29 |  | fdm 6744 | . . . . . 6
⊢ (𝑃:ℂ⟶ℂ →
dom 𝑃 =
ℂ) | 
| 30 | 7, 28, 29 | 3syl 18 | . . . . 5
⊢ (𝑀 ∈ ℕ → dom 𝑃 = ℂ) | 
| 31 | 27, 30 | sseqtrid 4025 | . . . 4
⊢ (𝑀 ∈ ℕ → (◡𝑃 “ {0}) ⊆
ℂ) | 
| 32 | 31 | sselda 3982 | . . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑥 ∈ (◡𝑃 “ {0})) → 𝑥 ∈ ℂ) | 
| 33 | 20, 12, 14, 26, 32 | fsumf1o 15760 | . 2
⊢ (𝑀 ∈ ℕ →
Σ𝑥 ∈ (◡𝑃 “ {0})𝑥 = Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) | 
| 34 | 6 | simp3d 1144 | . . . . . . 7
⊢ (𝑀 ∈ ℕ →
(coeff‘𝑃) = (𝑛 ∈ ℕ0
↦ ((𝑁C(2 ·
𝑛)) ·
(-1↑(𝑀 − 𝑛))))) | 
| 35 | 8 | oveq1d 7447 | . . . . . . 7
⊢ (𝑀 ∈ ℕ →
((deg‘𝑃) − 1) =
(𝑀 −
1)) | 
| 36 | 34, 35 | fveq12d 6912 | . . . . . 6
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘((deg‘𝑃) − 1)) = ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘(𝑀 − 1))) | 
| 37 |  | nnm1nn0 12569 | . . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℕ0) | 
| 38 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑛 = (𝑀 − 1) → (2 · 𝑛) = (2 · (𝑀 − 1))) | 
| 39 | 38 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑛 = (𝑀 − 1) → (𝑁C(2 · 𝑛)) = (𝑁C(2 · (𝑀 − 1)))) | 
| 40 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑛 = (𝑀 − 1) → (𝑀 − 𝑛) = (𝑀 − (𝑀 − 1))) | 
| 41 | 40 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑛 = (𝑀 − 1) → (-1↑(𝑀 − 𝑛)) = (-1↑(𝑀 − (𝑀 − 1)))) | 
| 42 | 39, 41 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑛 = (𝑀 − 1) → ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))) = ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1))))) | 
| 43 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ ((𝑁C(2 ·
𝑛)) ·
(-1↑(𝑀 − 𝑛)))) = (𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛)))) | 
| 44 |  | ovex 7465 | . . . . . . . 8
⊢ ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))) ∈ V | 
| 45 | 42, 43, 44 | fvmpt 7015 | . . . . . . 7
⊢ ((𝑀 − 1) ∈
ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘(𝑀 − 1)) = ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1))))) | 
| 46 | 37, 45 | syl 17 | . . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑛 ∈ ℕ0
↦ ((𝑁C(2 ·
𝑛)) ·
(-1↑(𝑀 − 𝑛))))‘(𝑀 − 1)) = ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1))))) | 
| 47 |  | nncn 12275 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) | 
| 48 |  | ax-1cn 11214 | . . . . . . . . . . 11
⊢ 1 ∈
ℂ | 
| 49 |  | nncan 11539 | . . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑀 −
(𝑀 − 1)) =
1) | 
| 50 | 47, 48, 49 | sylancl 586 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑀 − (𝑀 − 1)) = 1) | 
| 51 | 50 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(-1↑(𝑀 − (𝑀 − 1))) =
(-1↑1)) | 
| 52 |  | neg1cn 12381 | . . . . . . . . . 10
⊢ -1 ∈
ℂ | 
| 53 |  | exp1 14109 | . . . . . . . . . 10
⊢ (-1
∈ ℂ → (-1↑1) = -1) | 
| 54 | 52, 53 | ax-mp 5 | . . . . . . . . 9
⊢
(-1↑1) = -1 | 
| 55 | 51, 54 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(-1↑(𝑀 − (𝑀 − 1))) =
-1) | 
| 56 | 55 | oveq2d 7448 | . . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))) = ((𝑁C(2 · (𝑀 − 1))) · -1)) | 
| 57 |  | 2nn 12340 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ | 
| 58 |  | nnmulcl 12291 | . . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ ∧ 𝑀
∈ ℕ) → (2 · 𝑀) ∈ ℕ) | 
| 59 | 57, 58 | mpan 690 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℕ) | 
| 60 | 59 | peano2nnd 12284 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) + 1) ∈
ℕ) | 
| 61 | 4, 60 | eqeltrid 2844 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℕ) | 
| 62 | 61 | nnnn0d 12589 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 63 |  | 2z 12651 | . . . . . . . . . . 11
⊢ 2 ∈
ℤ | 
| 64 |  | nnz 12636 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) | 
| 65 |  | peano2zm 12662 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) | 
| 66 | 64, 65 | syl 17 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℤ) | 
| 67 |  | zmulcl 12668 | . . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ (𝑀
− 1) ∈ ℤ) → (2 · (𝑀 − 1)) ∈
ℤ) | 
| 68 | 63, 66, 67 | sylancr 587 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ ℤ) | 
| 69 |  | bccl 14362 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (2 · (𝑀
− 1)) ∈ ℤ) → (𝑁C(2 · (𝑀 − 1))) ∈
ℕ0) | 
| 70 | 62, 68, 69 | syl2anc 584 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈
ℕ0) | 
| 71 | 70 | nn0cnd 12591 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈
ℂ) | 
| 72 |  | mulcom 11242 | . . . . . . . 8
⊢ (((𝑁C(2 · (𝑀 − 1))) ∈ ℂ ∧ -1 ∈
ℂ) → ((𝑁C(2
· (𝑀 − 1)))
· -1) = (-1 · (𝑁C(2 · (𝑀 − 1))))) | 
| 73 | 71, 52, 72 | sylancl 586 | . . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · -1) = (-1 ·
(𝑁C(2 · (𝑀 − 1))))) | 
| 74 | 71 | mulm1d 11716 | . . . . . . 7
⊢ (𝑀 ∈ ℕ → (-1
· (𝑁C(2 ·
(𝑀 − 1)))) = -(𝑁C(2 · (𝑀 − 1)))) | 
| 75 | 56, 73, 74 | 3eqtrd 2780 | . . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))) = -(𝑁C(2 · (𝑀 − 1)))) | 
| 76 | 36, 46, 75 | 3eqtrd 2780 | . . . . 5
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘((deg‘𝑃) − 1)) = -(𝑁C(2 · (𝑀 − 1)))) | 
| 77 | 71 | negcld 11608 | . . . . 5
⊢ (𝑀 ∈ ℕ → -(𝑁C(2 · (𝑀 − 1))) ∈
ℂ) | 
| 78 | 76, 77 | eqeltrd 2840 | . . . 4
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘((deg‘𝑃) − 1)) ∈
ℂ) | 
| 79 | 34, 8 | fveq12d 6912 | . . . . . 6
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘(deg‘𝑃)) = ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘𝑀)) | 
| 80 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (2 · 𝑛) = (2 · 𝑀)) | 
| 81 | 80 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑛 = 𝑀 → (𝑁C(2 · 𝑛)) = (𝑁C(2 · 𝑀))) | 
| 82 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (𝑀 − 𝑛) = (𝑀 − 𝑀)) | 
| 83 | 82 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑛 = 𝑀 → (-1↑(𝑀 − 𝑛)) = (-1↑(𝑀 − 𝑀))) | 
| 84 | 81, 83 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑛 = 𝑀 → ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))) = ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀)))) | 
| 85 |  | ovex 7465 | . . . . . . . 8
⊢ ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀))) ∈ V | 
| 86 | 84, 43, 85 | fvmpt 7015 | . . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘𝑀) = ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀)))) | 
| 87 | 9, 86 | syl 17 | . . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑛 ∈ ℕ0
↦ ((𝑁C(2 ·
𝑛)) ·
(-1↑(𝑀 − 𝑛))))‘𝑀) = ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀)))) | 
| 88 | 47 | subidd 11609 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑀 − 𝑀) = 0) | 
| 89 | 88 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(-1↑(𝑀 − 𝑀)) =
(-1↑0)) | 
| 90 |  | exp0 14107 | . . . . . . . . . 10
⊢ (-1
∈ ℂ → (-1↑0) = 1) | 
| 91 | 52, 90 | ax-mp 5 | . . . . . . . . 9
⊢
(-1↑0) = 1 | 
| 92 | 89, 91 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(-1↑(𝑀 − 𝑀)) = 1) | 
| 93 | 92 | oveq2d 7448 | . . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀))) = ((𝑁C(2 · 𝑀)) · 1)) | 
| 94 |  | fz1ssfz0 13664 | . . . . . . . . . . 11
⊢
(1...𝑁) ⊆
(0...𝑁) | 
| 95 | 59 | nnred 12282 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℝ) | 
| 96 | 95 | lep1d 12200 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ≤ ((2
· 𝑀) +
1)) | 
| 97 | 96, 4 | breqtrrdi 5184 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ≤ 𝑁) | 
| 98 |  | nnuz 12922 | . . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) | 
| 99 | 59, 98 | eleqtrdi 2850 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
(ℤ≥‘1)) | 
| 100 | 61 | nnzd 12642 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℤ) | 
| 101 |  | elfz5 13557 | . . . . . . . . . . . . 13
⊢ (((2
· 𝑀) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑀) ∈ (1...𝑁) ↔ (2 · 𝑀) ≤ 𝑁)) | 
| 102 | 99, 100, 101 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) ∈
(1...𝑁) ↔ (2 ·
𝑀) ≤ 𝑁)) | 
| 103 | 97, 102 | mpbird 257 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
(1...𝑁)) | 
| 104 | 94, 103 | sselid 3980 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
(0...𝑁)) | 
| 105 |  | bccl2 14363 | . . . . . . . . . 10
⊢ ((2
· 𝑀) ∈
(0...𝑁) → (𝑁C(2 · 𝑀)) ∈ ℕ) | 
| 106 | 104, 105 | syl 17 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) ∈ ℕ) | 
| 107 | 106 | nncnd 12283 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) ∈ ℂ) | 
| 108 | 107 | mulridd 11279 | . . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) · 1) = (𝑁C(2 · 𝑀))) | 
| 109 | 93, 108 | eqtrd 2776 | . . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀))) = (𝑁C(2 · 𝑀))) | 
| 110 | 79, 87, 109 | 3eqtrd 2780 | . . . . 5
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘(deg‘𝑃)) = (𝑁C(2 · 𝑀))) | 
| 111 | 110, 107 | eqeltrd 2840 | . . . 4
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘(deg‘𝑃)) ∈ ℂ) | 
| 112 | 106 | nnne0d 12317 | . . . . 5
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) ≠ 0) | 
| 113 | 110, 112 | eqnetrd 3007 | . . . 4
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘(deg‘𝑃)) ≠ 0) | 
| 114 | 78, 111, 113 | divnegd 12057 | . . 3
⊢ (𝑀 ∈ ℕ →
-(((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))) = (-((coeff‘𝑃)‘((deg‘𝑃) − 1)) /
((coeff‘𝑃)‘(deg‘𝑃)))) | 
| 115 | 76 | negeqd 11503 | . . . . 5
⊢ (𝑀 ∈ ℕ →
-((coeff‘𝑃)‘((deg‘𝑃) − 1)) = --(𝑁C(2 · (𝑀 − 1)))) | 
| 116 | 71 | negnegd 11612 | . . . . 5
⊢ (𝑀 ∈ ℕ → --(𝑁C(2 · (𝑀 − 1))) = (𝑁C(2 · (𝑀 − 1)))) | 
| 117 | 115, 116 | eqtrd 2776 | . . . 4
⊢ (𝑀 ∈ ℕ →
-((coeff‘𝑃)‘((deg‘𝑃) − 1)) = (𝑁C(2 · (𝑀 − 1)))) | 
| 118 | 117, 110 | oveq12d 7450 | . . 3
⊢ (𝑀 ∈ ℕ →
(-((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))) = ((𝑁C(2 · (𝑀 − 1))) / (𝑁C(2 · 𝑀)))) | 
| 119 |  | bcm1k 14355 | . . . . . . . . . 10
⊢ ((2
· 𝑀) ∈
(1...𝑁) → (𝑁C(2 · 𝑀)) = ((𝑁C((2 · 𝑀) − 1)) · ((𝑁 − ((2 · 𝑀) − 1)) / (2 · 𝑀)))) | 
| 120 | 103, 119 | syl 17 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) = ((𝑁C((2 · 𝑀) − 1)) · ((𝑁 − ((2 · 𝑀) − 1)) / (2 · 𝑀)))) | 
| 121 | 59 | nncnd 12283 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℂ) | 
| 122 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → 1 ∈
ℂ) | 
| 123 | 121, 122,
122 | pnncand 11660 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) + 1) −
((2 · 𝑀) − 1))
= (1 + 1)) | 
| 124 | 4 | oveq1i 7442 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 − ((2 · 𝑀) − 1)) = (((2 ·
𝑀) + 1) − ((2
· 𝑀) −
1)) | 
| 125 |  | df-2 12330 | . . . . . . . . . . . . . . . 16
⊢ 2 = (1 +
1) | 
| 126 | 123, 124,
125 | 3eqtr4g 2801 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → (𝑁 − ((2 · 𝑀) − 1)) =
2) | 
| 127 |  | 2nn0 12545 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ0 | 
| 128 | 126, 127 | eqeltrdi 2848 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (𝑁 − ((2 · 𝑀) − 1)) ∈
ℕ0) | 
| 129 |  | nnm1nn0 12569 | . . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑀) ∈ ℕ
→ ((2 · 𝑀)
− 1) ∈ ℕ0) | 
| 130 | 59, 129 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℕ0) | 
| 131 |  | nn0sub 12578 | . . . . . . . . . . . . . . 15
⊢ ((((2
· 𝑀) − 1)
∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (((2
· 𝑀) − 1) ≤
𝑁 ↔ (𝑁 − ((2 · 𝑀) − 1)) ∈
ℕ0)) | 
| 132 | 130, 62, 131 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1) ≤
𝑁 ↔ (𝑁 − ((2 · 𝑀) − 1)) ∈
ℕ0)) | 
| 133 | 128, 132 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1) ≤
𝑁) | 
| 134 | 47 | 2timesd 12511 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) = (𝑀 + 𝑀)) | 
| 135 | 134 | oveq1d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1) =
((𝑀 + 𝑀) − 1)) | 
| 136 | 47, 47, 122 | addsubd 11642 | . . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → ((𝑀 + 𝑀) − 1) = ((𝑀 − 1) + 𝑀)) | 
| 137 | 135, 136 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1) =
((𝑀 − 1) + 𝑀)) | 
| 138 |  | nn0nnaddcl 12559 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑀 − 1) ∈
ℕ0 ∧ 𝑀
∈ ℕ) → ((𝑀
− 1) + 𝑀) ∈
ℕ) | 
| 139 | 37, 138 | mpancom 688 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → ((𝑀 − 1) + 𝑀) ∈ ℕ) | 
| 140 | 137, 139 | eqeltrd 2840 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℕ) | 
| 141 | 140, 98 | eleqtrdi 2850 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ (ℤ≥‘1)) | 
| 142 |  | elfz5 13557 | . . . . . . . . . . . . . 14
⊢ ((((2
· 𝑀) − 1)
∈ (ℤ≥‘1) ∧ 𝑁 ∈ ℤ) → (((2 · 𝑀) − 1) ∈ (1...𝑁) ↔ ((2 · 𝑀) − 1) ≤ 𝑁)) | 
| 143 | 141, 100,
142 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
∈ (1...𝑁) ↔ ((2
· 𝑀) − 1) ≤
𝑁)) | 
| 144 | 133, 143 | mpbird 257 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ (1...𝑁)) | 
| 145 |  | bcm1k 14355 | . . . . . . . . . . . 12
⊢ (((2
· 𝑀) − 1)
∈ (1...𝑁) →
(𝑁C((2 · 𝑀) − 1)) = ((𝑁C(((2 · 𝑀) − 1) − 1)) · ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2
· 𝑀) −
1)))) | 
| 146 | 144, 145 | syl 17 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑁C((2 · 𝑀) − 1)) = ((𝑁C(((2 · 𝑀) − 1) − 1)) · ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2
· 𝑀) −
1)))) | 
| 147 | 48 | 2timesi 12405 | . . . . . . . . . . . . . . . 16
⊢ (2
· 1) = (1 + 1) | 
| 148 | 147 | eqcomi 2745 | . . . . . . . . . . . . . . 15
⊢ (1 + 1) =
(2 · 1) | 
| 149 | 148 | oveq2i 7443 | . . . . . . . . . . . . . 14
⊢ ((2
· 𝑀) − (1 +
1)) = ((2 · 𝑀)
− (2 · 1)) | 
| 150 | 121, 122,
122 | subsub4d 11652 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
− 1) = ((2 · 𝑀) − (1 + 1))) | 
| 151 |  | 2cnd 12345 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 2 ∈
ℂ) | 
| 152 | 151, 47, 122 | subdid 11720 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1)) =
((2 · 𝑀) − (2
· 1))) | 
| 153 | 149, 150,
152 | 3eqtr4a 2802 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
− 1) = (2 · (𝑀
− 1))) | 
| 154 | 153 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (𝑁C(((2 · 𝑀) − 1) − 1)) = (𝑁C(2 · (𝑀 − 1)))) | 
| 155 | 61 | nncnd 12283 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 156 | 140 | nncnd 12283 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℂ) | 
| 157 | 155, 156,
122 | subsubd 11649 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (𝑁 − (((2 · 𝑀) − 1) − 1)) =
((𝑁 − ((2 ·
𝑀) − 1)) +
1)) | 
| 158 | 126 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → ((𝑁 − ((2 · 𝑀) − 1)) + 1) = (2 +
1)) | 
| 159 |  | df-3 12331 | . . . . . . . . . . . . . . 15
⊢ 3 = (2 +
1) | 
| 160 | 158, 159 | eqtr4di 2794 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → ((𝑁 − ((2 · 𝑀) − 1)) + 1) =
3) | 
| 161 | 157, 160 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (𝑁 − (((2 · 𝑀) − 1) − 1)) =
3) | 
| 162 | 161 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2
· 𝑀) − 1)) =
(3 / ((2 · 𝑀)
− 1))) | 
| 163 | 154, 162 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((𝑁C(((2 · 𝑀) − 1) − 1)) · ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2
· 𝑀) − 1))) =
((𝑁C(2 · (𝑀 − 1))) · (3 / ((2
· 𝑀) −
1)))) | 
| 164 | 146, 163 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁C((2 · 𝑀) − 1)) = ((𝑁C(2 · (𝑀 − 1))) · (3 / ((2 ·
𝑀) −
1)))) | 
| 165 | 126 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((𝑁 − ((2 · 𝑀) − 1)) / (2 ·
𝑀)) = (2 / (2 ·
𝑀))) | 
| 166 | 164, 165 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁C((2 · 𝑀) − 1)) · ((𝑁 − ((2 · 𝑀) − 1)) / (2 · 𝑀))) = (((𝑁C(2 · (𝑀 − 1))) · (3 / ((2 ·
𝑀) − 1))) · (2
/ (2 · 𝑀)))) | 
| 167 |  | 3re 12347 | . . . . . . . . . . . 12
⊢ 3 ∈
ℝ | 
| 168 |  | nndivre 12308 | . . . . . . . . . . . 12
⊢ ((3
∈ ℝ ∧ ((2 · 𝑀) − 1) ∈ ℕ) → (3 / ((2
· 𝑀) − 1))
∈ ℝ) | 
| 169 | 167, 140,
168 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (3 / ((2
· 𝑀) − 1))
∈ ℝ) | 
| 170 | 169 | recnd 11290 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (3 / ((2
· 𝑀) − 1))
∈ ℂ) | 
| 171 |  | 2re 12341 | . . . . . . . . . . . 12
⊢ 2 ∈
ℝ | 
| 172 |  | nndivre 12308 | . . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ (2 · 𝑀) ∈ ℕ) → (2 / (2 ·
𝑀)) ∈
ℝ) | 
| 173 | 171, 59, 172 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2 / (2
· 𝑀)) ∈
ℝ) | 
| 174 | 173 | recnd 11290 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2 / (2
· 𝑀)) ∈
ℂ) | 
| 175 | 71, 170, 174 | mulassd 11285 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (((𝑁C(2 · (𝑀 − 1))) · (3 / ((2 ·
𝑀) − 1))) · (2
/ (2 · 𝑀))) =
((𝑁C(2 · (𝑀 − 1))) · ((3 / ((2
· 𝑀) − 1))
· (2 / (2 · 𝑀))))) | 
| 176 | 120, 166,
175 | 3eqtrd 2780 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) = ((𝑁C(2 · (𝑀 − 1))) · ((3 / ((2 ·
𝑀) − 1)) · (2
/ (2 · 𝑀))))) | 
| 177 |  | 3cn 12348 | . . . . . . . . . . . 12
⊢ 3 ∈
ℂ | 
| 178 | 177 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 3 ∈
ℂ) | 
| 179 | 140 | nnne0d 12317 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1) ≠
0) | 
| 180 | 59 | nnne0d 12317 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ≠
0) | 
| 181 | 178, 156,
151, 121, 179, 180 | divmuldivd 12085 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((3 / ((2
· 𝑀) − 1))
· (2 / (2 · 𝑀))) = ((3 · 2) / (((2 · 𝑀) − 1) · (2
· 𝑀)))) | 
| 182 |  | 3t2e6 12433 | . . . . . . . . . . . 12
⊢ (3
· 2) = 6 | 
| 183 | 182 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (3
· 2) = 6) | 
| 184 | 156, 121 | mulcomd 11283 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
· (2 · 𝑀)) =
((2 · 𝑀) ·
((2 · 𝑀) −
1))) | 
| 185 | 183, 184 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((3
· 2) / (((2 · 𝑀) − 1) · (2 · 𝑀))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) | 
| 186 | 181, 185 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((3 / ((2
· 𝑀) − 1))
· (2 / (2 · 𝑀))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) | 
| 187 | 186 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · ((3 / ((2 ·
𝑀) − 1)) · (2
/ (2 · 𝑀)))) =
((𝑁C(2 · (𝑀 − 1))) · (6 / ((2
· 𝑀) · ((2
· 𝑀) −
1))))) | 
| 188 | 176, 187 | eqtrd 2776 | . . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) = ((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 ·
𝑀) · ((2 ·
𝑀) −
1))))) | 
| 189 | 188 | oveq1d 7447 | . . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1)))) = (((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 ·
𝑀) · ((2 ·
𝑀) − 1)))) / (𝑁C(2 · (𝑀 − 1))))) | 
| 190 |  | 6re 12357 | . . . . . . . . 9
⊢ 6 ∈
ℝ | 
| 191 | 59, 140 | nnmulcld 12320 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · ((2
· 𝑀) − 1))
∈ ℕ) | 
| 192 |  | nndivre 12308 | . . . . . . . . 9
⊢ ((6
∈ ℝ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℕ) → (6 /
((2 · 𝑀) ·
((2 · 𝑀) −
1))) ∈ ℝ) | 
| 193 | 190, 191,
192 | sylancr 587 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ → (6 / ((2
· 𝑀) · ((2
· 𝑀) − 1)))
∈ ℝ) | 
| 194 | 193 | recnd 11290 | . . . . . . 7
⊢ (𝑀 ∈ ℕ → (6 / ((2
· 𝑀) · ((2
· 𝑀) − 1)))
∈ ℂ) | 
| 195 |  | nnm1nn0 12569 | . . . . . . . . . . . . . 14
⊢ (((2
· 𝑀) − 1)
∈ ℕ → (((2 · 𝑀) − 1) − 1) ∈
ℕ0) | 
| 196 | 140, 195 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
− 1) ∈ ℕ0) | 
| 197 | 153, 196 | eqeltrrd 2841 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ ℕ0) | 
| 198 | 197 | nn0red 12590 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ ℝ) | 
| 199 | 140 | nnred 12282 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℝ) | 
| 200 | 61 | nnred 12282 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 201 | 199 | ltm1d 12201 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
− 1) < ((2 · 𝑀) − 1)) | 
| 202 | 153, 201 | eqbrtrrd 5166 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
< ((2 · 𝑀)
− 1)) | 
| 203 | 198, 199,
202 | ltled 11410 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
≤ ((2 · 𝑀)
− 1)) | 
| 204 | 198, 199,
200, 203, 133 | letrd 11419 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
≤ 𝑁) | 
| 205 |  | nn0uz 12921 | . . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) | 
| 206 | 197, 205 | eleqtrdi 2850 | . . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ (ℤ≥‘0)) | 
| 207 |  | elfz5 13557 | . . . . . . . . . . 11
⊢ (((2
· (𝑀 − 1))
∈ (ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → ((2 · (𝑀 − 1)) ∈ (0...𝑁) ↔ (2 · (𝑀 − 1)) ≤ 𝑁)) | 
| 208 | 206, 100,
207 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((2
· (𝑀 − 1))
∈ (0...𝑁) ↔ (2
· (𝑀 − 1))
≤ 𝑁)) | 
| 209 | 204, 208 | mpbird 257 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ (0...𝑁)) | 
| 210 |  | bccl2 14363 | . . . . . . . . 9
⊢ ((2
· (𝑀 − 1))
∈ (0...𝑁) →
(𝑁C(2 · (𝑀 − 1))) ∈
ℕ) | 
| 211 | 209, 210 | syl 17 | . . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈
ℕ) | 
| 212 | 211 | nnne0d 12317 | . . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ≠ 0) | 
| 213 | 194, 71, 212 | divcan3d 12049 | . . . . . 6
⊢ (𝑀 ∈ ℕ → (((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 ·
𝑀) · ((2 ·
𝑀) − 1)))) / (𝑁C(2 · (𝑀 − 1)))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) | 
| 214 | 189, 213 | eqtrd 2776 | . . . . 5
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1)))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) | 
| 215 | 214 | oveq2d 7448 | . . . 4
⊢ (𝑀 ∈ ℕ → (1 /
((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1))))) = (1 / (6 / ((2 ·
𝑀) · ((2 ·
𝑀) −
1))))) | 
| 216 | 107, 71, 112, 212 | recdivd 12061 | . . . 4
⊢ (𝑀 ∈ ℕ → (1 /
((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1))))) = ((𝑁C(2 · (𝑀 − 1))) / (𝑁C(2 · 𝑀)))) | 
| 217 | 191 | nncnd 12283 | . . . . 5
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · ((2
· 𝑀) − 1))
∈ ℂ) | 
| 218 | 191 | nnne0d 12317 | . . . . 5
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · ((2
· 𝑀) − 1))
≠ 0) | 
| 219 |  | 6cn 12358 | . . . . . 6
⊢ 6 ∈
ℂ | 
| 220 |  | 6nn 12356 | . . . . . . 7
⊢ 6 ∈
ℕ | 
| 221 | 220 | nnne0i 12307 | . . . . . 6
⊢ 6 ≠
0 | 
| 222 |  | recdiv 11974 | . . . . . 6
⊢ (((6
∈ ℂ ∧ 6 ≠ 0) ∧ (((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ ∧ ((2
· 𝑀) · ((2
· 𝑀) − 1))
≠ 0)) → (1 / (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) /
6)) | 
| 223 | 219, 221,
222 | mpanl12 702 | . . . . 5
⊢ ((((2
· 𝑀) · ((2
· 𝑀) − 1))
∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ≠ 0) → (1 / (6 / ((2
· 𝑀) · ((2
· 𝑀) − 1)))) =
(((2 · 𝑀) ·
((2 · 𝑀) − 1))
/ 6)) | 
| 224 | 217, 218,
223 | syl2anc 584 | . . . 4
⊢ (𝑀 ∈ ℕ → (1 / (6 /
((2 · 𝑀) ·
((2 · 𝑀) −
1)))) = (((2 · 𝑀)
· ((2 · 𝑀)
− 1)) / 6)) | 
| 225 | 215, 216,
224 | 3eqtr3d 2784 | . . 3
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) / (𝑁C(2 · 𝑀))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) | 
| 226 | 114, 118,
225 | 3eqtrd 2780 | . 2
⊢ (𝑀 ∈ ℕ →
-(((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) /
6)) | 
| 227 | 19, 33, 226 | 3eqtr3d 2784 | 1
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) = (((2 ·
𝑀) · ((2 ·
𝑀) − 1)) /
6)) |