Step | Hyp | Ref
| Expression |
1 | | eqid 2760 |
. . 3
⊢
(coeff‘𝑃) =
(coeff‘𝑃) |
2 | | eqid 2760 |
. . 3
⊢
(deg‘𝑃) =
(deg‘𝑃) |
3 | | eqid 2760 |
. . 3
⊢ (◡𝑃 “ {0}) = (◡𝑃 “ {0}) |
4 | | basel.n |
. . . . 5
⊢ 𝑁 = ((2 · 𝑀) + 1) |
5 | | basel.p |
. . . . 5
⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗))) |
6 | 4, 5 | basellem2 25028 |
. . . 4
⊢ (𝑀 ∈ ℕ → (𝑃 ∈ (Poly‘ℂ)
∧ (deg‘𝑃) = 𝑀 ∧ (coeff‘𝑃) = (𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛)))))) |
7 | 6 | simp1d 1137 |
. . 3
⊢ (𝑀 ∈ ℕ → 𝑃 ∈
(Poly‘ℂ)) |
8 | 6 | simp2d 1138 |
. . . 4
⊢ (𝑀 ∈ ℕ →
(deg‘𝑃) = 𝑀) |
9 | | nnnn0 11511 |
. . . . 5
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
10 | | hashfz1 13348 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝑀 ∈ ℕ →
(♯‘(1...𝑀)) =
𝑀) |
12 | | basel.t |
. . . . . . 7
⊢ 𝑇 = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) |
13 | 4, 5, 12 | basellem4 25030 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 𝑇:(1...𝑀)–1-1-onto→(◡𝑃 “ {0})) |
14 | | ovex 6842 |
. . . . . . 7
⊢
(1...𝑀) ∈
V |
15 | 14 | f1oen 8144 |
. . . . . 6
⊢ (𝑇:(1...𝑀)–1-1-onto→(◡𝑃 “ {0}) → (1...𝑀) ≈ (◡𝑃 “ {0})) |
16 | 13, 15 | syl 17 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
(1...𝑀) ≈ (◡𝑃 “ {0})) |
17 | | fzfid 12986 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
(1...𝑀) ∈
Fin) |
18 | | nnne0 11265 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0) |
19 | 8, 18 | eqnetrd 2999 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(deg‘𝑃) ≠
0) |
20 | | fveq2 6353 |
. . . . . . . . . . 11
⊢ (𝑃 = 0𝑝 →
(deg‘𝑃) =
(deg‘0𝑝)) |
21 | | dgr0 24237 |
. . . . . . . . . . 11
⊢
(deg‘0𝑝) = 0 |
22 | 20, 21 | syl6eq 2810 |
. . . . . . . . . 10
⊢ (𝑃 = 0𝑝 →
(deg‘𝑃) =
0) |
23 | 22 | necon3i 2964 |
. . . . . . . . 9
⊢
((deg‘𝑃) ≠
0 → 𝑃 ≠
0𝑝) |
24 | 19, 23 | syl 17 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑃 ≠
0𝑝) |
25 | 3 | fta1 24282 |
. . . . . . . 8
⊢ ((𝑃 ∈ (Poly‘ℂ)
∧ 𝑃 ≠
0𝑝) → ((◡𝑃 “ {0}) ∈ Fin ∧
(♯‘(◡𝑃 “ {0})) ≤ (deg‘𝑃))) |
26 | 7, 24, 25 | syl2anc 696 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((◡𝑃 “ {0}) ∈ Fin ∧
(♯‘(◡𝑃 “ {0})) ≤ (deg‘𝑃))) |
27 | 26 | simpld 477 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (◡𝑃 “ {0}) ∈ Fin) |
28 | | hashen 13349 |
. . . . . 6
⊢
(((1...𝑀) ∈ Fin
∧ (◡𝑃 “ {0}) ∈ Fin) →
((♯‘(1...𝑀)) =
(♯‘(◡𝑃 “ {0})) ↔ (1...𝑀) ≈ (◡𝑃 “ {0}))) |
29 | 17, 27, 28 | syl2anc 696 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((♯‘(1...𝑀)) =
(♯‘(◡𝑃 “ {0})) ↔ (1...𝑀) ≈ (◡𝑃 “ {0}))) |
30 | 16, 29 | mpbird 247 |
. . . 4
⊢ (𝑀 ∈ ℕ →
(♯‘(1...𝑀)) =
(♯‘(◡𝑃 “ {0}))) |
31 | 8, 11, 30 | 3eqtr2rd 2801 |
. . 3
⊢ (𝑀 ∈ ℕ →
(♯‘(◡𝑃 “ {0})) = (deg‘𝑃)) |
32 | | id 22 |
. . . 4
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ) |
33 | 8, 32 | eqeltrd 2839 |
. . 3
⊢ (𝑀 ∈ ℕ →
(deg‘𝑃) ∈
ℕ) |
34 | 1, 2, 3, 7, 31, 33 | vieta1 24286 |
. 2
⊢ (𝑀 ∈ ℕ →
Σ𝑥 ∈ (◡𝑃 “ {0})𝑥 = -(((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃)))) |
35 | | id 22 |
. . 3
⊢ (𝑥 = ((tan‘((𝑘 · π) / 𝑁))↑-2) → 𝑥 = ((tan‘((𝑘 · π) / 𝑁))↑-2)) |
36 | | oveq1 6821 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝑛 · π) = (𝑘 · π)) |
37 | 36 | oveq1d 6829 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → ((𝑛 · π) / 𝑁) = ((𝑘 · π) / 𝑁)) |
38 | 37 | fveq2d 6357 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (tan‘((𝑛 · π) / 𝑁)) = (tan‘((𝑘 · π) / 𝑁))) |
39 | 38 | oveq1d 6829 |
. . . . 5
⊢ (𝑛 = 𝑘 → ((tan‘((𝑛 · π) / 𝑁))↑-2) = ((tan‘((𝑘 · π) / 𝑁))↑-2)) |
40 | | ovex 6842 |
. . . . 5
⊢
((tan‘((𝑘
· π) / 𝑁))↑-2) ∈ V |
41 | 39, 12, 40 | fvmpt 6445 |
. . . 4
⊢ (𝑘 ∈ (1...𝑀) → (𝑇‘𝑘) = ((tan‘((𝑘 · π) / 𝑁))↑-2)) |
42 | 41 | adantl 473 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑇‘𝑘) = ((tan‘((𝑘 · π) / 𝑁))↑-2)) |
43 | | cnvimass 5643 |
. . . . 5
⊢ (◡𝑃 “ {0}) ⊆ dom 𝑃 |
44 | | plyf 24173 |
. . . . . 6
⊢ (𝑃 ∈ (Poly‘ℂ)
→ 𝑃:ℂ⟶ℂ) |
45 | | fdm 6212 |
. . . . . 6
⊢ (𝑃:ℂ⟶ℂ →
dom 𝑃 =
ℂ) |
46 | 7, 44, 45 | 3syl 18 |
. . . . 5
⊢ (𝑀 ∈ ℕ → dom 𝑃 = ℂ) |
47 | 43, 46 | syl5sseq 3794 |
. . . 4
⊢ (𝑀 ∈ ℕ → (◡𝑃 “ {0}) ⊆
ℂ) |
48 | 47 | sselda 3744 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑥 ∈ (◡𝑃 “ {0})) → 𝑥 ∈ ℂ) |
49 | 35, 17, 13, 42, 48 | fsumf1o 14673 |
. 2
⊢ (𝑀 ∈ ℕ →
Σ𝑥 ∈ (◡𝑃 “ {0})𝑥 = Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) |
50 | 6 | simp3d 1139 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(coeff‘𝑃) = (𝑛 ∈ ℕ0
↦ ((𝑁C(2 ·
𝑛)) ·
(-1↑(𝑀 − 𝑛))))) |
51 | 8 | oveq1d 6829 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
((deg‘𝑃) − 1) =
(𝑀 −
1)) |
52 | 50, 51 | fveq12d 6359 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘((deg‘𝑃) − 1)) = ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘(𝑀 − 1))) |
53 | | nnm1nn0 11546 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℕ0) |
54 | | oveq2 6822 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑀 − 1) → (2 · 𝑛) = (2 · (𝑀 − 1))) |
55 | 54 | oveq2d 6830 |
. . . . . . . . 9
⊢ (𝑛 = (𝑀 − 1) → (𝑁C(2 · 𝑛)) = (𝑁C(2 · (𝑀 − 1)))) |
56 | | oveq2 6822 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑀 − 1) → (𝑀 − 𝑛) = (𝑀 − (𝑀 − 1))) |
57 | 56 | oveq2d 6830 |
. . . . . . . . 9
⊢ (𝑛 = (𝑀 − 1) → (-1↑(𝑀 − 𝑛)) = (-1↑(𝑀 − (𝑀 − 1)))) |
58 | 55, 57 | oveq12d 6832 |
. . . . . . . 8
⊢ (𝑛 = (𝑀 − 1) → ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))) = ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1))))) |
59 | | eqid 2760 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ ((𝑁C(2 ·
𝑛)) ·
(-1↑(𝑀 − 𝑛)))) = (𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛)))) |
60 | | ovex 6842 |
. . . . . . . 8
⊢ ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))) ∈ V |
61 | 58, 59, 60 | fvmpt 6445 |
. . . . . . 7
⊢ ((𝑀 − 1) ∈
ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘(𝑀 − 1)) = ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1))))) |
62 | 53, 61 | syl 17 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑛 ∈ ℕ0
↦ ((𝑁C(2 ·
𝑛)) ·
(-1↑(𝑀 − 𝑛))))‘(𝑀 − 1)) = ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1))))) |
63 | | nncn 11240 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
64 | | ax-1cn 10206 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
65 | | nncan 10522 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑀 −
(𝑀 − 1)) =
1) |
66 | 63, 64, 65 | sylancl 697 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑀 − (𝑀 − 1)) = 1) |
67 | 66 | oveq2d 6830 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(-1↑(𝑀 − (𝑀 − 1))) =
(-1↑1)) |
68 | | neg1cn 11336 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
69 | | exp1 13080 |
. . . . . . . . . 10
⊢ (-1
∈ ℂ → (-1↑1) = -1) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . 9
⊢
(-1↑1) = -1 |
71 | 67, 70 | syl6eq 2810 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(-1↑(𝑀 − (𝑀 − 1))) =
-1) |
72 | 71 | oveq2d 6830 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))) = ((𝑁C(2 · (𝑀 − 1))) · -1)) |
73 | | 2nn 11397 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ |
74 | | nnmulcl 11255 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ ∧ 𝑀
∈ ℕ) → (2 · 𝑀) ∈ ℕ) |
75 | 73, 74 | mpan 708 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℕ) |
76 | 75 | peano2nnd 11249 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) + 1) ∈
ℕ) |
77 | 4, 76 | syl5eqel 2843 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℕ) |
78 | 77 | nnnn0d 11563 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℕ0) |
79 | | 2z 11621 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
80 | | nnz 11611 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
81 | | peano2zm 11632 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℤ) |
83 | | zmulcl 11638 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ (𝑀
− 1) ∈ ℤ) → (2 · (𝑀 − 1)) ∈
ℤ) |
84 | 79, 82, 83 | sylancr 698 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ ℤ) |
85 | | bccl 13323 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (2 · (𝑀
− 1)) ∈ ℤ) → (𝑁C(2 · (𝑀 − 1))) ∈
ℕ0) |
86 | 78, 84, 85 | syl2anc 696 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈
ℕ0) |
87 | 86 | nn0cnd 11565 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈
ℂ) |
88 | | mulcom 10234 |
. . . . . . . 8
⊢ (((𝑁C(2 · (𝑀 − 1))) ∈ ℂ ∧ -1 ∈
ℂ) → ((𝑁C(2
· (𝑀 − 1)))
· -1) = (-1 · (𝑁C(2 · (𝑀 − 1))))) |
89 | 87, 68, 88 | sylancl 697 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · -1) = (-1 ·
(𝑁C(2 · (𝑀 − 1))))) |
90 | 87 | mulm1d 10694 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (-1
· (𝑁C(2 ·
(𝑀 − 1)))) = -(𝑁C(2 · (𝑀 − 1)))) |
91 | 72, 89, 90 | 3eqtrd 2798 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))) = -(𝑁C(2 · (𝑀 − 1)))) |
92 | 52, 62, 91 | 3eqtrd 2798 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘((deg‘𝑃) − 1)) = -(𝑁C(2 · (𝑀 − 1)))) |
93 | 87 | negcld 10591 |
. . . . 5
⊢ (𝑀 ∈ ℕ → -(𝑁C(2 · (𝑀 − 1))) ∈
ℂ) |
94 | 92, 93 | eqeltrd 2839 |
. . . 4
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘((deg‘𝑃) − 1)) ∈
ℂ) |
95 | 50, 8 | fveq12d 6359 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘(deg‘𝑃)) = ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘𝑀)) |
96 | | oveq2 6822 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (2 · 𝑛) = (2 · 𝑀)) |
97 | 96 | oveq2d 6830 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → (𝑁C(2 · 𝑛)) = (𝑁C(2 · 𝑀))) |
98 | | oveq2 6822 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (𝑀 − 𝑛) = (𝑀 − 𝑀)) |
99 | 98 | oveq2d 6830 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → (-1↑(𝑀 − 𝑛)) = (-1↑(𝑀 − 𝑀))) |
100 | 97, 99 | oveq12d 6832 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))) = ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀)))) |
101 | | ovex 6842 |
. . . . . . . 8
⊢ ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀))) ∈ V |
102 | 100, 59, 101 | fvmpt 6445 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘𝑀) = ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀)))) |
103 | 9, 102 | syl 17 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑛 ∈ ℕ0
↦ ((𝑁C(2 ·
𝑛)) ·
(-1↑(𝑀 − 𝑛))))‘𝑀) = ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀)))) |
104 | 63 | subidd 10592 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑀 − 𝑀) = 0) |
105 | 104 | oveq2d 6830 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(-1↑(𝑀 − 𝑀)) =
(-1↑0)) |
106 | | exp0 13078 |
. . . . . . . . . 10
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
107 | 68, 106 | ax-mp 5 |
. . . . . . . . 9
⊢
(-1↑0) = 1 |
108 | 105, 107 | syl6eq 2810 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(-1↑(𝑀 − 𝑀)) = 1) |
109 | 108 | oveq2d 6830 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀))) = ((𝑁C(2 · 𝑀)) · 1)) |
110 | | fz1ssfz0 12649 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
(0...𝑁) |
111 | 75 | nnred 11247 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℝ) |
112 | 111 | lep1d 11167 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ≤ ((2
· 𝑀) +
1)) |
113 | 112, 4 | syl6breqr 4846 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ≤ 𝑁) |
114 | | nnuz 11936 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
115 | 75, 114 | syl6eleq 2849 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
(ℤ≥‘1)) |
116 | 77 | nnzd 11693 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℤ) |
117 | | elfz5 12547 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝑀) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑀) ∈ (1...𝑁) ↔ (2 · 𝑀) ≤ 𝑁)) |
118 | 115, 116,
117 | syl2anc 696 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) ∈
(1...𝑁) ↔ (2 ·
𝑀) ≤ 𝑁)) |
119 | 113, 118 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
(1...𝑁)) |
120 | 110, 119 | sseldi 3742 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
(0...𝑁)) |
121 | | bccl2 13324 |
. . . . . . . . . 10
⊢ ((2
· 𝑀) ∈
(0...𝑁) → (𝑁C(2 · 𝑀)) ∈ ℕ) |
122 | 120, 121 | syl 17 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) ∈ ℕ) |
123 | 122 | nncnd 11248 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) ∈ ℂ) |
124 | 123 | mulid1d 10269 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) · 1) = (𝑁C(2 · 𝑀))) |
125 | 109, 124 | eqtrd 2794 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀))) = (𝑁C(2 · 𝑀))) |
126 | 95, 103, 125 | 3eqtrd 2798 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘(deg‘𝑃)) = (𝑁C(2 · 𝑀))) |
127 | 126, 123 | eqeltrd 2839 |
. . . 4
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘(deg‘𝑃)) ∈ ℂ) |
128 | 122 | nnne0d 11277 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) ≠ 0) |
129 | 126, 128 | eqnetrd 2999 |
. . . 4
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘(deg‘𝑃)) ≠ 0) |
130 | 94, 127, 129 | divnegd 11026 |
. . 3
⊢ (𝑀 ∈ ℕ →
-(((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))) = (-((coeff‘𝑃)‘((deg‘𝑃) − 1)) /
((coeff‘𝑃)‘(deg‘𝑃)))) |
131 | 92 | negeqd 10487 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
-((coeff‘𝑃)‘((deg‘𝑃) − 1)) = --(𝑁C(2 · (𝑀 − 1)))) |
132 | 87 | negnegd 10595 |
. . . . 5
⊢ (𝑀 ∈ ℕ → --(𝑁C(2 · (𝑀 − 1))) = (𝑁C(2 · (𝑀 − 1)))) |
133 | 131, 132 | eqtrd 2794 |
. . . 4
⊢ (𝑀 ∈ ℕ →
-((coeff‘𝑃)‘((deg‘𝑃) − 1)) = (𝑁C(2 · (𝑀 − 1)))) |
134 | 133, 126 | oveq12d 6832 |
. . 3
⊢ (𝑀 ∈ ℕ →
(-((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))) = ((𝑁C(2 · (𝑀 − 1))) / (𝑁C(2 · 𝑀)))) |
135 | | bcm1k 13316 |
. . . . . . . . . 10
⊢ ((2
· 𝑀) ∈
(1...𝑁) → (𝑁C(2 · 𝑀)) = ((𝑁C((2 · 𝑀) − 1)) · ((𝑁 − ((2 · 𝑀) − 1)) / (2 · 𝑀)))) |
136 | 119, 135 | syl 17 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) = ((𝑁C((2 · 𝑀) − 1)) · ((𝑁 − ((2 · 𝑀) − 1)) / (2 · 𝑀)))) |
137 | 75 | nncnd 11248 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℂ) |
138 | | 1cnd 10268 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → 1 ∈
ℂ) |
139 | 137, 138,
138 | pnncand 10643 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) + 1) −
((2 · 𝑀) − 1))
= (1 + 1)) |
140 | 4 | oveq1i 6824 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 − ((2 · 𝑀) − 1)) = (((2 ·
𝑀) + 1) − ((2
· 𝑀) −
1)) |
141 | | df-2 11291 |
. . . . . . . . . . . . . . . 16
⊢ 2 = (1 +
1) |
142 | 139, 140,
141 | 3eqtr4g 2819 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → (𝑁 − ((2 · 𝑀) − 1)) =
2) |
143 | | 2nn0 11521 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ0 |
144 | 142, 143 | syl6eqel 2847 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (𝑁 − ((2 · 𝑀) − 1)) ∈
ℕ0) |
145 | | nnm1nn0 11546 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑀) ∈ ℕ
→ ((2 · 𝑀)
− 1) ∈ ℕ0) |
146 | 75, 145 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℕ0) |
147 | | nn0sub 11555 |
. . . . . . . . . . . . . . 15
⊢ ((((2
· 𝑀) − 1)
∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (((2
· 𝑀) − 1) ≤
𝑁 ↔ (𝑁 − ((2 · 𝑀) − 1)) ∈
ℕ0)) |
148 | 146, 78, 147 | syl2anc 696 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1) ≤
𝑁 ↔ (𝑁 − ((2 · 𝑀) − 1)) ∈
ℕ0)) |
149 | 144, 148 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1) ≤
𝑁) |
150 | 63 | 2timesd 11487 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) = (𝑀 + 𝑀)) |
151 | 150 | oveq1d 6829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1) =
((𝑀 + 𝑀) − 1)) |
152 | 63, 63, 138 | addsubd 10625 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → ((𝑀 + 𝑀) − 1) = ((𝑀 − 1) + 𝑀)) |
153 | 151, 152 | eqtrd 2794 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1) =
((𝑀 − 1) + 𝑀)) |
154 | | nn0nnaddcl 11536 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 − 1) ∈
ℕ0 ∧ 𝑀
∈ ℕ) → ((𝑀
− 1) + 𝑀) ∈
ℕ) |
155 | 53, 154 | mpancom 706 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → ((𝑀 − 1) + 𝑀) ∈ ℕ) |
156 | 153, 155 | eqeltrd 2839 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℕ) |
157 | 156, 114 | syl6eleq 2849 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ (ℤ≥‘1)) |
158 | | elfz5 12547 |
. . . . . . . . . . . . . 14
⊢ ((((2
· 𝑀) − 1)
∈ (ℤ≥‘1) ∧ 𝑁 ∈ ℤ) → (((2 · 𝑀) − 1) ∈ (1...𝑁) ↔ ((2 · 𝑀) − 1) ≤ 𝑁)) |
159 | 157, 116,
158 | syl2anc 696 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
∈ (1...𝑁) ↔ ((2
· 𝑀) − 1) ≤
𝑁)) |
160 | 149, 159 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ (1...𝑁)) |
161 | | bcm1k 13316 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑀) − 1)
∈ (1...𝑁) →
(𝑁C((2 · 𝑀) − 1)) = ((𝑁C(((2 · 𝑀) − 1) − 1)) · ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2
· 𝑀) −
1)))) |
162 | 160, 161 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑁C((2 · 𝑀) − 1)) = ((𝑁C(((2 · 𝑀) − 1) − 1)) · ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2
· 𝑀) −
1)))) |
163 | 64 | 2timesi 11359 |
. . . . . . . . . . . . . . . 16
⊢ (2
· 1) = (1 + 1) |
164 | 163 | eqcomi 2769 |
. . . . . . . . . . . . . . 15
⊢ (1 + 1) =
(2 · 1) |
165 | 164 | oveq2i 6825 |
. . . . . . . . . . . . . 14
⊢ ((2
· 𝑀) − (1 +
1)) = ((2 · 𝑀)
− (2 · 1)) |
166 | 137, 138,
138 | subsub4d 10635 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
− 1) = ((2 · 𝑀) − (1 + 1))) |
167 | | 2cnd 11305 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 2 ∈
ℂ) |
168 | 167, 63, 138 | subdid 10698 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1)) =
((2 · 𝑀) − (2
· 1))) |
169 | 165, 166,
168 | 3eqtr4a 2820 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
− 1) = (2 · (𝑀
− 1))) |
170 | 169 | oveq2d 6830 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (𝑁C(((2 · 𝑀) − 1) − 1)) = (𝑁C(2 · (𝑀 − 1)))) |
171 | 77 | nncnd 11248 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℂ) |
172 | 156 | nncnd 11248 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℂ) |
173 | 171, 172,
138 | subsubd 10632 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (𝑁 − (((2 · 𝑀) − 1) − 1)) =
((𝑁 − ((2 ·
𝑀) − 1)) +
1)) |
174 | 142 | oveq1d 6829 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → ((𝑁 − ((2 · 𝑀) − 1)) + 1) = (2 +
1)) |
175 | | df-3 11292 |
. . . . . . . . . . . . . . 15
⊢ 3 = (2 +
1) |
176 | 174, 175 | syl6eqr 2812 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → ((𝑁 − ((2 · 𝑀) − 1)) + 1) =
3) |
177 | 173, 176 | eqtrd 2794 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (𝑁 − (((2 · 𝑀) − 1) − 1)) =
3) |
178 | 177 | oveq1d 6829 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2
· 𝑀) − 1)) =
(3 / ((2 · 𝑀)
− 1))) |
179 | 170, 178 | oveq12d 6832 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((𝑁C(((2 · 𝑀) − 1) − 1)) · ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2
· 𝑀) − 1))) =
((𝑁C(2 · (𝑀 − 1))) · (3 / ((2
· 𝑀) −
1)))) |
180 | 162, 179 | eqtrd 2794 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁C((2 · 𝑀) − 1)) = ((𝑁C(2 · (𝑀 − 1))) · (3 / ((2 ·
𝑀) −
1)))) |
181 | 142 | oveq1d 6829 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((𝑁 − ((2 · 𝑀) − 1)) / (2 ·
𝑀)) = (2 / (2 ·
𝑀))) |
182 | 180, 181 | oveq12d 6832 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁C((2 · 𝑀) − 1)) · ((𝑁 − ((2 · 𝑀) − 1)) / (2 · 𝑀))) = (((𝑁C(2 · (𝑀 − 1))) · (3 / ((2 ·
𝑀) − 1))) · (2
/ (2 · 𝑀)))) |
183 | | 3re 11306 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℝ |
184 | | nndivre 11268 |
. . . . . . . . . . . 12
⊢ ((3
∈ ℝ ∧ ((2 · 𝑀) − 1) ∈ ℕ) → (3 / ((2
· 𝑀) − 1))
∈ ℝ) |
185 | 183, 156,
184 | sylancr 698 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (3 / ((2
· 𝑀) − 1))
∈ ℝ) |
186 | 185 | recnd 10280 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (3 / ((2
· 𝑀) − 1))
∈ ℂ) |
187 | | 2re 11302 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
188 | | nndivre 11268 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ (2 · 𝑀) ∈ ℕ) → (2 / (2 ·
𝑀)) ∈
ℝ) |
189 | 187, 75, 188 | sylancr 698 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2 / (2
· 𝑀)) ∈
ℝ) |
190 | 189 | recnd 10280 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2 / (2
· 𝑀)) ∈
ℂ) |
191 | 87, 186, 190 | mulassd 10275 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (((𝑁C(2 · (𝑀 − 1))) · (3 / ((2 ·
𝑀) − 1))) · (2
/ (2 · 𝑀))) =
((𝑁C(2 · (𝑀 − 1))) · ((3 / ((2
· 𝑀) − 1))
· (2 / (2 · 𝑀))))) |
192 | 136, 182,
191 | 3eqtrd 2798 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) = ((𝑁C(2 · (𝑀 − 1))) · ((3 / ((2 ·
𝑀) − 1)) · (2
/ (2 · 𝑀))))) |
193 | | 3cn 11307 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℂ |
194 | 193 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 3 ∈
ℂ) |
195 | 156 | nnne0d 11277 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1) ≠
0) |
196 | 75 | nnne0d 11277 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ≠
0) |
197 | 194, 172,
167, 137, 195, 196 | divmuldivd 11054 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((3 / ((2
· 𝑀) − 1))
· (2 / (2 · 𝑀))) = ((3 · 2) / (((2 · 𝑀) − 1) · (2
· 𝑀)))) |
198 | | 3t2e6 11391 |
. . . . . . . . . . . 12
⊢ (3
· 2) = 6 |
199 | 198 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (3
· 2) = 6) |
200 | 172, 137 | mulcomd 10273 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
· (2 · 𝑀)) =
((2 · 𝑀) ·
((2 · 𝑀) −
1))) |
201 | 199, 200 | oveq12d 6832 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((3
· 2) / (((2 · 𝑀) − 1) · (2 · 𝑀))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) |
202 | 197, 201 | eqtrd 2794 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((3 / ((2
· 𝑀) − 1))
· (2 / (2 · 𝑀))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) |
203 | 202 | oveq2d 6830 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · ((3 / ((2 ·
𝑀) − 1)) · (2
/ (2 · 𝑀)))) =
((𝑁C(2 · (𝑀 − 1))) · (6 / ((2
· 𝑀) · ((2
· 𝑀) −
1))))) |
204 | 192, 203 | eqtrd 2794 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) = ((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 ·
𝑀) · ((2 ·
𝑀) −
1))))) |
205 | 204 | oveq1d 6829 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1)))) = (((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 ·
𝑀) · ((2 ·
𝑀) − 1)))) / (𝑁C(2 · (𝑀 − 1))))) |
206 | | 6re 11313 |
. . . . . . . . 9
⊢ 6 ∈
ℝ |
207 | 75, 156 | nnmulcld 11280 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · ((2
· 𝑀) − 1))
∈ ℕ) |
208 | | nndivre 11268 |
. . . . . . . . 9
⊢ ((6
∈ ℝ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℕ) → (6 /
((2 · 𝑀) ·
((2 · 𝑀) −
1))) ∈ ℝ) |
209 | 206, 207,
208 | sylancr 698 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (6 / ((2
· 𝑀) · ((2
· 𝑀) − 1)))
∈ ℝ) |
210 | 209 | recnd 10280 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (6 / ((2
· 𝑀) · ((2
· 𝑀) − 1)))
∈ ℂ) |
211 | | nnm1nn0 11546 |
. . . . . . . . . . . . . 14
⊢ (((2
· 𝑀) − 1)
∈ ℕ → (((2 · 𝑀) − 1) − 1) ∈
ℕ0) |
212 | 156, 211 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
− 1) ∈ ℕ0) |
213 | 169, 212 | eqeltrrd 2840 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ ℕ0) |
214 | 213 | nn0red 11564 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ ℝ) |
215 | 156 | nnred 11247 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℝ) |
216 | 77 | nnred 11247 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℝ) |
217 | 215 | ltm1d 11168 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
− 1) < ((2 · 𝑀) − 1)) |
218 | 169, 217 | eqbrtrrd 4828 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
< ((2 · 𝑀)
− 1)) |
219 | 214, 215,
218 | ltled 10397 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
≤ ((2 · 𝑀)
− 1)) |
220 | 214, 215,
216, 219, 149 | letrd 10406 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
≤ 𝑁) |
221 | | nn0uz 11935 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
222 | 213, 221 | syl6eleq 2849 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ (ℤ≥‘0)) |
223 | | elfz5 12547 |
. . . . . . . . . . 11
⊢ (((2
· (𝑀 − 1))
∈ (ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → ((2 · (𝑀 − 1)) ∈ (0...𝑁) ↔ (2 · (𝑀 − 1)) ≤ 𝑁)) |
224 | 222, 116,
223 | syl2anc 696 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((2
· (𝑀 − 1))
∈ (0...𝑁) ↔ (2
· (𝑀 − 1))
≤ 𝑁)) |
225 | 220, 224 | mpbird 247 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ (0...𝑁)) |
226 | | bccl2 13324 |
. . . . . . . . 9
⊢ ((2
· (𝑀 − 1))
∈ (0...𝑁) →
(𝑁C(2 · (𝑀 − 1))) ∈
ℕ) |
227 | 225, 226 | syl 17 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈
ℕ) |
228 | 227 | nnne0d 11277 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ≠ 0) |
229 | 210, 87, 228 | divcan3d 11018 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 ·
𝑀) · ((2 ·
𝑀) − 1)))) / (𝑁C(2 · (𝑀 − 1)))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) |
230 | 205, 229 | eqtrd 2794 |
. . . . 5
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1)))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) |
231 | 230 | oveq2d 6830 |
. . . 4
⊢ (𝑀 ∈ ℕ → (1 /
((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1))))) = (1 / (6 / ((2 ·
𝑀) · ((2 ·
𝑀) −
1))))) |
232 | 123, 87, 128, 228 | recdivd 11030 |
. . . 4
⊢ (𝑀 ∈ ℕ → (1 /
((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1))))) = ((𝑁C(2 · (𝑀 − 1))) / (𝑁C(2 · 𝑀)))) |
233 | 207 | nncnd 11248 |
. . . . 5
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · ((2
· 𝑀) − 1))
∈ ℂ) |
234 | 207 | nnne0d 11277 |
. . . . 5
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · ((2
· 𝑀) − 1))
≠ 0) |
235 | | 6cn 11314 |
. . . . . 6
⊢ 6 ∈
ℂ |
236 | | 6nn 11401 |
. . . . . . 7
⊢ 6 ∈
ℕ |
237 | 236 | nnne0i 11267 |
. . . . . 6
⊢ 6 ≠
0 |
238 | | recdiv 10943 |
. . . . . 6
⊢ (((6
∈ ℂ ∧ 6 ≠ 0) ∧ (((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ ∧ ((2
· 𝑀) · ((2
· 𝑀) − 1))
≠ 0)) → (1 / (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) /
6)) |
239 | 235, 237,
238 | mpanl12 720 |
. . . . 5
⊢ ((((2
· 𝑀) · ((2
· 𝑀) − 1))
∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ≠ 0) → (1 / (6 / ((2
· 𝑀) · ((2
· 𝑀) − 1)))) =
(((2 · 𝑀) ·
((2 · 𝑀) − 1))
/ 6)) |
240 | 233, 234,
239 | syl2anc 696 |
. . . 4
⊢ (𝑀 ∈ ℕ → (1 / (6 /
((2 · 𝑀) ·
((2 · 𝑀) −
1)))) = (((2 · 𝑀)
· ((2 · 𝑀)
− 1)) / 6)) |
241 | 231, 232,
240 | 3eqtr3d 2802 |
. . 3
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) / (𝑁C(2 · 𝑀))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) |
242 | 130, 134,
241 | 3eqtrd 2798 |
. 2
⊢ (𝑀 ∈ ℕ →
-(((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) /
6)) |
243 | 34, 49, 242 | 3eqtr3d 2802 |
1
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) = (((2 ·
𝑀) · ((2 ·
𝑀) − 1)) /
6)) |