Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(coeff‘𝑃) =
(coeff‘𝑃) |
2 | | eqid 2622 |
. . 3
⊢
(deg‘𝑃) =
(deg‘𝑃) |
3 | | eqid 2622 |
. . 3
⊢ (◡𝑃 “ {0}) = (◡𝑃 “ {0}) |
4 | | basel.n |
. . . . 5
⊢ 𝑁 = ((2 · 𝑀) + 1) |
5 | | basel.p |
. . . . 5
⊢ 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑡↑𝑗))) |
6 | 4, 5 | basellem2 24808 |
. . . 4
⊢ (𝑀 ∈ ℕ → (𝑃 ∈ (Poly‘ℂ)
∧ (deg‘𝑃) = 𝑀 ∧ (coeff‘𝑃) = (𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛)))))) |
7 | 6 | simp1d 1073 |
. . 3
⊢ (𝑀 ∈ ℕ → 𝑃 ∈
(Poly‘ℂ)) |
8 | 6 | simp2d 1074 |
. . . 4
⊢ (𝑀 ∈ ℕ →
(deg‘𝑃) = 𝑀) |
9 | | nnnn0 11299 |
. . . . 5
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
10 | | hashfz1 13134 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ (#‘(1...𝑀)) =
𝑀) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (𝑀 ∈ ℕ →
(#‘(1...𝑀)) = 𝑀) |
12 | | basel.t |
. . . . . . 7
⊢ 𝑇 = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) |
13 | 4, 5, 12 | basellem4 24810 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 𝑇:(1...𝑀)–1-1-onto→(◡𝑃 “ {0})) |
14 | | ovex 6678 |
. . . . . . 7
⊢
(1...𝑀) ∈
V |
15 | 14 | f1oen 7976 |
. . . . . 6
⊢ (𝑇:(1...𝑀)–1-1-onto→(◡𝑃 “ {0}) → (1...𝑀) ≈ (◡𝑃 “ {0})) |
16 | 13, 15 | syl 17 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
(1...𝑀) ≈ (◡𝑃 “ {0})) |
17 | | fzfid 12772 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
(1...𝑀) ∈
Fin) |
18 | | nnne0 11053 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0) |
19 | 8, 18 | eqnetrd 2861 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(deg‘𝑃) ≠
0) |
20 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑃 = 0𝑝 →
(deg‘𝑃) =
(deg‘0𝑝)) |
21 | | dgr0 24018 |
. . . . . . . . . . 11
⊢
(deg‘0𝑝) = 0 |
22 | 20, 21 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑃 = 0𝑝 →
(deg‘𝑃) =
0) |
23 | 22 | necon3i 2826 |
. . . . . . . . 9
⊢
((deg‘𝑃) ≠
0 → 𝑃 ≠
0𝑝) |
24 | 19, 23 | syl 17 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑃 ≠
0𝑝) |
25 | 3 | fta1 24063 |
. . . . . . . 8
⊢ ((𝑃 ∈ (Poly‘ℂ)
∧ 𝑃 ≠
0𝑝) → ((◡𝑃 “ {0}) ∈ Fin ∧
(#‘(◡𝑃 “ {0})) ≤ (deg‘𝑃))) |
26 | 7, 24, 25 | syl2anc 693 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((◡𝑃 “ {0}) ∈ Fin ∧
(#‘(◡𝑃 “ {0})) ≤ (deg‘𝑃))) |
27 | 26 | simpld 475 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (◡𝑃 “ {0}) ∈ Fin) |
28 | | hashen 13135 |
. . . . . 6
⊢
(((1...𝑀) ∈ Fin
∧ (◡𝑃 “ {0}) ∈ Fin) →
((#‘(1...𝑀)) =
(#‘(◡𝑃 “ {0})) ↔ (1...𝑀) ≈ (◡𝑃 “ {0}))) |
29 | 17, 27, 28 | syl2anc 693 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((#‘(1...𝑀)) =
(#‘(◡𝑃 “ {0})) ↔ (1...𝑀) ≈ (◡𝑃 “ {0}))) |
30 | 16, 29 | mpbird 247 |
. . . 4
⊢ (𝑀 ∈ ℕ →
(#‘(1...𝑀)) =
(#‘(◡𝑃 “ {0}))) |
31 | 8, 11, 30 | 3eqtr2rd 2663 |
. . 3
⊢ (𝑀 ∈ ℕ →
(#‘(◡𝑃 “ {0})) = (deg‘𝑃)) |
32 | | id 22 |
. . . 4
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ) |
33 | 8, 32 | eqeltrd 2701 |
. . 3
⊢ (𝑀 ∈ ℕ →
(deg‘𝑃) ∈
ℕ) |
34 | 1, 2, 3, 7, 31, 33 | vieta1 24067 |
. 2
⊢ (𝑀 ∈ ℕ →
Σ𝑥 ∈ (◡𝑃 “ {0})𝑥 = -(((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃)))) |
35 | | id 22 |
. . 3
⊢ (𝑥 = ((tan‘((𝑘 · π) / 𝑁))↑-2) → 𝑥 = ((tan‘((𝑘 · π) / 𝑁))↑-2)) |
36 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝑛 · π) = (𝑘 · π)) |
37 | 36 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → ((𝑛 · π) / 𝑁) = ((𝑘 · π) / 𝑁)) |
38 | 37 | fveq2d 6195 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (tan‘((𝑛 · π) / 𝑁)) = (tan‘((𝑘 · π) / 𝑁))) |
39 | 38 | oveq1d 6665 |
. . . . 5
⊢ (𝑛 = 𝑘 → ((tan‘((𝑛 · π) / 𝑁))↑-2) = ((tan‘((𝑘 · π) / 𝑁))↑-2)) |
40 | | ovex 6678 |
. . . . 5
⊢
((tan‘((𝑘
· π) / 𝑁))↑-2) ∈ V |
41 | 39, 12, 40 | fvmpt 6282 |
. . . 4
⊢ (𝑘 ∈ (1...𝑀) → (𝑇‘𝑘) = ((tan‘((𝑘 · π) / 𝑁))↑-2)) |
42 | 41 | adantl 482 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑇‘𝑘) = ((tan‘((𝑘 · π) / 𝑁))↑-2)) |
43 | | cnvimass 5485 |
. . . . 5
⊢ (◡𝑃 “ {0}) ⊆ dom 𝑃 |
44 | | plyf 23954 |
. . . . . 6
⊢ (𝑃 ∈ (Poly‘ℂ)
→ 𝑃:ℂ⟶ℂ) |
45 | | fdm 6051 |
. . . . . 6
⊢ (𝑃:ℂ⟶ℂ →
dom 𝑃 =
ℂ) |
46 | 7, 44, 45 | 3syl 18 |
. . . . 5
⊢ (𝑀 ∈ ℕ → dom 𝑃 = ℂ) |
47 | 43, 46 | syl5sseq 3653 |
. . . 4
⊢ (𝑀 ∈ ℕ → (◡𝑃 “ {0}) ⊆
ℂ) |
48 | 47 | sselda 3603 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑥 ∈ (◡𝑃 “ {0})) → 𝑥 ∈ ℂ) |
49 | 35, 17, 13, 42, 48 | fsumf1o 14454 |
. 2
⊢ (𝑀 ∈ ℕ →
Σ𝑥 ∈ (◡𝑃 “ {0})𝑥 = Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) |
50 | 6 | simp3d 1075 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
(coeff‘𝑃) = (𝑛 ∈ ℕ0
↦ ((𝑁C(2 ·
𝑛)) ·
(-1↑(𝑀 − 𝑛))))) |
51 | 8 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ →
((deg‘𝑃) − 1) =
(𝑀 −
1)) |
52 | 50, 51 | fveq12d 6197 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘((deg‘𝑃) − 1)) = ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘(𝑀 − 1))) |
53 | | nnm1nn0 11334 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℕ0) |
54 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑀 − 1) → (2 · 𝑛) = (2 · (𝑀 − 1))) |
55 | 54 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑛 = (𝑀 − 1) → (𝑁C(2 · 𝑛)) = (𝑁C(2 · (𝑀 − 1)))) |
56 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑀 − 1) → (𝑀 − 𝑛) = (𝑀 − (𝑀 − 1))) |
57 | 56 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑛 = (𝑀 − 1) → (-1↑(𝑀 − 𝑛)) = (-1↑(𝑀 − (𝑀 − 1)))) |
58 | 55, 57 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑛 = (𝑀 − 1) → ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))) = ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1))))) |
59 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ ((𝑁C(2 ·
𝑛)) ·
(-1↑(𝑀 − 𝑛)))) = (𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛)))) |
60 | | ovex 6678 |
. . . . . . . 8
⊢ ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))) ∈ V |
61 | 58, 59, 60 | fvmpt 6282 |
. . . . . . 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 11028 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
64 | | ax-1cn 9994 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
65 | | nncan 10310 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑀 −
(𝑀 − 1)) =
1) |
66 | 63, 64, 65 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑀 − (𝑀 − 1)) = 1) |
67 | 66 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(-1↑(𝑀 − (𝑀 − 1))) =
(-1↑1)) |
68 | | neg1cn 11124 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
69 | | exp1 12866 |
. . . . . . . . . 10
⊢ (-1
∈ ℂ → (-1↑1) = -1) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . 9
⊢
(-1↑1) = -1 |
71 | 67, 70 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(-1↑(𝑀 − (𝑀 − 1))) =
-1) |
72 | 71 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))) = ((𝑁C(2 · (𝑀 − 1))) · -1)) |
73 | | 2nn 11185 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ |
74 | | nnmulcl 11043 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ ∧ 𝑀
∈ ℕ) → (2 · 𝑀) ∈ ℕ) |
75 | 73, 74 | mpan 706 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℕ) |
76 | 75 | peano2nnd 11037 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) + 1) ∈
ℕ) |
77 | 4, 76 | syl5eqel 2705 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℕ) |
78 | 77 | nnnn0d 11351 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℕ0) |
79 | | 2z 11409 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
80 | | nnz 11399 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
81 | | peano2zm 11420 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℤ) |
83 | | zmulcl 11426 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ (𝑀
− 1) ∈ ℤ) → (2 · (𝑀 − 1)) ∈
ℤ) |
84 | 79, 82, 83 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ ℤ) |
85 | | bccl 13109 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (2 · (𝑀
− 1)) ∈ ℤ) → (𝑁C(2 · (𝑀 − 1))) ∈
ℕ0) |
86 | 78, 84, 85 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈
ℕ0) |
87 | 86 | nn0cnd 11353 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈
ℂ) |
88 | | mulcom 10022 |
. . . . . . . 8
⊢ (((𝑁C(2 · (𝑀 − 1))) ∈ ℂ ∧ -1 ∈
ℂ) → ((𝑁C(2
· (𝑀 − 1)))
· -1) = (-1 · (𝑁C(2 · (𝑀 − 1))))) |
89 | 87, 68, 88 | sylancl 694 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · -1) = (-1 ·
(𝑁C(2 · (𝑀 − 1))))) |
90 | 87 | mulm1d 10482 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (-1
· (𝑁C(2 ·
(𝑀 − 1)))) = -(𝑁C(2 · (𝑀 − 1)))) |
91 | 72, 89, 90 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))) = -(𝑁C(2 · (𝑀 − 1)))) |
92 | 52, 62, 91 | 3eqtrd 2660 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘((deg‘𝑃) − 1)) = -(𝑁C(2 · (𝑀 − 1)))) |
93 | 87 | negcld 10379 |
. . . . 5
⊢ (𝑀 ∈ ℕ → -(𝑁C(2 · (𝑀 − 1))) ∈
ℂ) |
94 | 92, 93 | eqeltrd 2701 |
. . . 4
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘((deg‘𝑃) − 1)) ∈
ℂ) |
95 | 50, 8 | fveq12d 6197 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘(deg‘𝑃)) = ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘𝑀)) |
96 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (2 · 𝑛) = (2 · 𝑀)) |
97 | 96 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → (𝑁C(2 · 𝑛)) = (𝑁C(2 · 𝑀))) |
98 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → (𝑀 − 𝑛) = (𝑀 − 𝑀)) |
99 | 98 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → (-1↑(𝑀 − 𝑛)) = (-1↑(𝑀 − 𝑀))) |
100 | 97, 99 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))) = ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀)))) |
101 | | ovex 6678 |
. . . . . . . 8
⊢ ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀))) ∈ V |
102 | 100, 59, 101 | fvmpt 6282 |
. . . . . . 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 10380 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑀 − 𝑀) = 0) |
105 | 104 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ →
(-1↑(𝑀 − 𝑀)) =
(-1↑0)) |
106 | | exp0 12864 |
. . . . . . . . . 10
⊢ (-1
∈ ℂ → (-1↑0) = 1) |
107 | 68, 106 | ax-mp 5 |
. . . . . . . . 9
⊢
(-1↑0) = 1 |
108 | 105, 107 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ →
(-1↑(𝑀 − 𝑀)) = 1) |
109 | 108 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀))) = ((𝑁C(2 · 𝑀)) · 1)) |
110 | | 1eluzge0 11732 |
. . . . . . . . . . . 12
⊢ 1 ∈
(ℤ≥‘0) |
111 | | fzss1 12380 |
. . . . . . . . . . . 12
⊢ (1 ∈
(ℤ≥‘0) → (1...𝑁) ⊆ (0...𝑁)) |
112 | 110, 111 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
(0...𝑁) |
113 | 75 | nnred 11035 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℝ) |
114 | 113 | lep1d 10955 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ≤ ((2
· 𝑀) +
1)) |
115 | 114, 4 | syl6breqr 4695 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ≤ 𝑁) |
116 | | nnuz 11723 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
117 | 75, 116 | syl6eleq 2711 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
(ℤ≥‘1)) |
118 | 77 | nnzd 11481 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℤ) |
119 | | elfz5 12334 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝑀) ∈
(ℤ≥‘1) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑀) ∈ (1...𝑁) ↔ (2 · 𝑀) ≤ 𝑁)) |
120 | 117, 118,
119 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) ∈
(1...𝑁) ↔ (2 ·
𝑀) ≤ 𝑁)) |
121 | 115, 120 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
(1...𝑁)) |
122 | 112, 121 | sseldi 3601 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
(0...𝑁)) |
123 | | bccl2 13110 |
. . . . . . . . . 10
⊢ ((2
· 𝑀) ∈
(0...𝑁) → (𝑁C(2 · 𝑀)) ∈ ℕ) |
124 | 122, 123 | syl 17 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) ∈ ℕ) |
125 | 124 | nncnd 11036 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) ∈ ℂ) |
126 | 125 | mulid1d 10057 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) · 1) = (𝑁C(2 · 𝑀))) |
127 | 109, 126 | eqtrd 2656 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀))) = (𝑁C(2 · 𝑀))) |
128 | 95, 103, 127 | 3eqtrd 2660 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘(deg‘𝑃)) = (𝑁C(2 · 𝑀))) |
129 | 128, 125 | eqeltrd 2701 |
. . . 4
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘(deg‘𝑃)) ∈ ℂ) |
130 | 124 | nnne0d 11065 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) ≠ 0) |
131 | 128, 130 | eqnetrd 2861 |
. . . 4
⊢ (𝑀 ∈ ℕ →
((coeff‘𝑃)‘(deg‘𝑃)) ≠ 0) |
132 | 94, 129, 131 | divnegd 10814 |
. . 3
⊢ (𝑀 ∈ ℕ →
-(((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))) = (-((coeff‘𝑃)‘((deg‘𝑃) − 1)) /
((coeff‘𝑃)‘(deg‘𝑃)))) |
133 | 92 | negeqd 10275 |
. . . . 5
⊢ (𝑀 ∈ ℕ →
-((coeff‘𝑃)‘((deg‘𝑃) − 1)) = --(𝑁C(2 · (𝑀 − 1)))) |
134 | 87 | negnegd 10383 |
. . . . 5
⊢ (𝑀 ∈ ℕ → --(𝑁C(2 · (𝑀 − 1))) = (𝑁C(2 · (𝑀 − 1)))) |
135 | 133, 134 | eqtrd 2656 |
. . . 4
⊢ (𝑀 ∈ ℕ →
-((coeff‘𝑃)‘((deg‘𝑃) − 1)) = (𝑁C(2 · (𝑀 − 1)))) |
136 | 135, 128 | oveq12d 6668 |
. . 3
⊢ (𝑀 ∈ ℕ →
(-((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))) = ((𝑁C(2 · (𝑀 − 1))) / (𝑁C(2 · 𝑀)))) |
137 | | bcm1k 13102 |
. . . . . . . . . 10
⊢ ((2
· 𝑀) ∈
(1...𝑁) → (𝑁C(2 · 𝑀)) = ((𝑁C((2 · 𝑀) − 1)) · ((𝑁 − ((2 · 𝑀) − 1)) / (2 · 𝑀)))) |
138 | 121, 137 | syl 17 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) = ((𝑁C((2 · 𝑀) − 1)) · ((𝑁 − ((2 · 𝑀) − 1)) / (2 · 𝑀)))) |
139 | 75 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ∈
ℂ) |
140 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → 1 ∈
ℂ) |
141 | 139, 140,
140 | pnncand 10431 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) + 1) −
((2 · 𝑀) − 1))
= (1 + 1)) |
142 | 4 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 − ((2 · 𝑀) − 1)) = (((2 ·
𝑀) + 1) − ((2
· 𝑀) −
1)) |
143 | | df-2 11079 |
. . . . . . . . . . . . . . . 16
⊢ 2 = (1 +
1) |
144 | 141, 142,
143 | 3eqtr4g 2681 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → (𝑁 − ((2 · 𝑀) − 1)) =
2) |
145 | | 2nn0 11309 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℕ0 |
146 | 144, 145 | syl6eqel 2709 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (𝑁 − ((2 · 𝑀) − 1)) ∈
ℕ0) |
147 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑀) ∈ ℕ
→ ((2 · 𝑀)
− 1) ∈ ℕ0) |
148 | 75, 147 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℕ0) |
149 | | nn0sub 11343 |
. . . . . . . . . . . . . . 15
⊢ ((((2
· 𝑀) − 1)
∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (((2
· 𝑀) − 1) ≤
𝑁 ↔ (𝑁 − ((2 · 𝑀) − 1)) ∈
ℕ0)) |
150 | 148, 78, 149 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1) ≤
𝑁 ↔ (𝑁 − ((2 · 𝑀) − 1)) ∈
ℕ0)) |
151 | 146, 150 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1) ≤
𝑁) |
152 | 63 | 2timesd 11275 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) = (𝑀 + 𝑀)) |
153 | 152 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1) =
((𝑀 + 𝑀) − 1)) |
154 | 63, 63, 140 | addsubd 10413 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → ((𝑀 + 𝑀) − 1) = ((𝑀 − 1) + 𝑀)) |
155 | 153, 154 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1) =
((𝑀 − 1) + 𝑀)) |
156 | | nn0nnaddcl 11324 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 − 1) ∈
ℕ0 ∧ 𝑀
∈ ℕ) → ((𝑀
− 1) + 𝑀) ∈
ℕ) |
157 | 53, 156 | mpancom 703 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → ((𝑀 − 1) + 𝑀) ∈ ℕ) |
158 | 155, 157 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℕ) |
159 | 158, 116 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ (ℤ≥‘1)) |
160 | | elfz5 12334 |
. . . . . . . . . . . . . 14
⊢ ((((2
· 𝑀) − 1)
∈ (ℤ≥‘1) ∧ 𝑁 ∈ ℤ) → (((2 · 𝑀) − 1) ∈ (1...𝑁) ↔ ((2 · 𝑀) − 1) ≤ 𝑁)) |
161 | 159, 118,
160 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
∈ (1...𝑁) ↔ ((2
· 𝑀) − 1) ≤
𝑁)) |
162 | 151, 161 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ (1...𝑁)) |
163 | | bcm1k 13102 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑀) − 1)
∈ (1...𝑁) →
(𝑁C((2 · 𝑀) − 1)) = ((𝑁C(((2 · 𝑀) − 1) − 1)) · ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2
· 𝑀) −
1)))) |
164 | 162, 163 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝑁C((2 · 𝑀) − 1)) = ((𝑁C(((2 · 𝑀) − 1) − 1)) · ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2
· 𝑀) −
1)))) |
165 | 64 | 2timesi 11147 |
. . . . . . . . . . . . . . . 16
⊢ (2
· 1) = (1 + 1) |
166 | 165 | eqcomi 2631 |
. . . . . . . . . . . . . . 15
⊢ (1 + 1) =
(2 · 1) |
167 | 166 | oveq2i 6661 |
. . . . . . . . . . . . . 14
⊢ ((2
· 𝑀) − (1 +
1)) = ((2 · 𝑀)
− (2 · 1)) |
168 | 139, 140,
140 | subsub4d 10423 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
− 1) = ((2 · 𝑀) − (1 + 1))) |
169 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 2 ∈
ℂ) |
170 | 169, 63, 140 | subdid 10486 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1)) =
((2 · 𝑀) − (2
· 1))) |
171 | 167, 168,
170 | 3eqtr4a 2682 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
− 1) = (2 · (𝑀
− 1))) |
172 | 171 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (𝑁C(((2 · 𝑀) − 1) − 1)) = (𝑁C(2 · (𝑀 − 1)))) |
173 | 77 | nncnd 11036 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℂ) |
174 | 158 | nncnd 11036 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℂ) |
175 | 173, 174,
140 | subsubd 10420 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → (𝑁 − (((2 · 𝑀) − 1) − 1)) =
((𝑁 − ((2 ·
𝑀) − 1)) +
1)) |
176 | 144 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ → ((𝑁 − ((2 · 𝑀) − 1)) + 1) = (2 +
1)) |
177 | | df-3 11080 |
. . . . . . . . . . . . . . 15
⊢ 3 = (2 +
1) |
178 | 176, 177 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → ((𝑁 − ((2 · 𝑀) − 1)) + 1) =
3) |
179 | 175, 178 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (𝑁 − (((2 · 𝑀) − 1) − 1)) =
3) |
180 | 179 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2
· 𝑀) − 1)) =
(3 / ((2 · 𝑀)
− 1))) |
181 | 172, 180 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((𝑁C(((2 · 𝑀) − 1) − 1)) · ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2
· 𝑀) − 1))) =
((𝑁C(2 · (𝑀 − 1))) · (3 / ((2
· 𝑀) −
1)))) |
182 | 164, 181 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (𝑁C((2 · 𝑀) − 1)) = ((𝑁C(2 · (𝑀 − 1))) · (3 / ((2 ·
𝑀) −
1)))) |
183 | 144 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((𝑁 − ((2 · 𝑀) − 1)) / (2 ·
𝑀)) = (2 / (2 ·
𝑀))) |
184 | 182, 183 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((𝑁C((2 · 𝑀) − 1)) · ((𝑁 − ((2 · 𝑀) − 1)) / (2 · 𝑀))) = (((𝑁C(2 · (𝑀 − 1))) · (3 / ((2 ·
𝑀) − 1))) · (2
/ (2 · 𝑀)))) |
185 | | 3re 11094 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℝ |
186 | | nndivre 11056 |
. . . . . . . . . . . 12
⊢ ((3
∈ ℝ ∧ ((2 · 𝑀) − 1) ∈ ℕ) → (3 / ((2
· 𝑀) − 1))
∈ ℝ) |
187 | 185, 158,
186 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (3 / ((2
· 𝑀) − 1))
∈ ℝ) |
188 | 187 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (3 / ((2
· 𝑀) − 1))
∈ ℂ) |
189 | | 2re 11090 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
190 | | nndivre 11056 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ (2 · 𝑀) ∈ ℕ) → (2 / (2 ·
𝑀)) ∈
ℝ) |
191 | 189, 75, 190 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2 / (2
· 𝑀)) ∈
ℝ) |
192 | 191 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2 / (2
· 𝑀)) ∈
ℂ) |
193 | 87, 188, 192 | mulassd 10063 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (((𝑁C(2 · (𝑀 − 1))) · (3 / ((2 ·
𝑀) − 1))) · (2
/ (2 · 𝑀))) =
((𝑁C(2 · (𝑀 − 1))) · ((3 / ((2
· 𝑀) − 1))
· (2 / (2 · 𝑀))))) |
194 | 138, 184,
193 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) = ((𝑁C(2 · (𝑀 − 1))) · ((3 / ((2 ·
𝑀) − 1)) · (2
/ (2 · 𝑀))))) |
195 | | 3cn 11095 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℂ |
196 | 195 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 3 ∈
ℂ) |
197 | 158 | nnne0d 11065 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1) ≠
0) |
198 | 75 | nnne0d 11065 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· 𝑀) ≠
0) |
199 | 196, 174,
169, 139, 197, 198 | divmuldivd 10842 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((3 / ((2
· 𝑀) − 1))
· (2 / (2 · 𝑀))) = ((3 · 2) / (((2 · 𝑀) − 1) · (2
· 𝑀)))) |
200 | | 3t2e6 11179 |
. . . . . . . . . . . 12
⊢ (3
· 2) = 6 |
201 | 200 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (3
· 2) = 6) |
202 | 174, 139 | mulcomd 10061 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
· (2 · 𝑀)) =
((2 · 𝑀) ·
((2 · 𝑀) −
1))) |
203 | 201, 202 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((3
· 2) / (((2 · 𝑀) − 1) · (2 · 𝑀))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) |
204 | 199, 203 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((3 / ((2
· 𝑀) − 1))
· (2 / (2 · 𝑀))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) |
205 | 204 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · ((3 / ((2 ·
𝑀) − 1)) · (2
/ (2 · 𝑀)))) =
((𝑁C(2 · (𝑀 − 1))) · (6 / ((2
· 𝑀) · ((2
· 𝑀) −
1))))) |
206 | 194, 205 | eqtrd 2656 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) = ((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 ·
𝑀) · ((2 ·
𝑀) −
1))))) |
207 | 206 | oveq1d 6665 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1)))) = (((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 ·
𝑀) · ((2 ·
𝑀) − 1)))) / (𝑁C(2 · (𝑀 − 1))))) |
208 | | 6re 11101 |
. . . . . . . . 9
⊢ 6 ∈
ℝ |
209 | 75, 158 | nnmulcld 11068 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · ((2
· 𝑀) − 1))
∈ ℕ) |
210 | | nndivre 11056 |
. . . . . . . . 9
⊢ ((6
∈ ℝ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℕ) → (6 /
((2 · 𝑀) ·
((2 · 𝑀) −
1))) ∈ ℝ) |
211 | 208, 209,
210 | sylancr 695 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (6 / ((2
· 𝑀) · ((2
· 𝑀) − 1)))
∈ ℝ) |
212 | 211 | recnd 10068 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (6 / ((2
· 𝑀) · ((2
· 𝑀) − 1)))
∈ ℂ) |
213 | | nnm1nn0 11334 |
. . . . . . . . . . . . . 14
⊢ (((2
· 𝑀) − 1)
∈ ℕ → (((2 · 𝑀) − 1) − 1) ∈
ℕ0) |
214 | 158, 213 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
− 1) ∈ ℕ0) |
215 | 171, 214 | eqeltrrd 2702 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ ℕ0) |
216 | 215 | nn0red 11352 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ ℝ) |
217 | 158 | nnred 11035 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) − 1)
∈ ℝ) |
218 | 77 | nnred 11035 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑁 ∈
ℝ) |
219 | 217 | ltm1d 10956 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ → (((2
· 𝑀) − 1)
− 1) < ((2 · 𝑀) − 1)) |
220 | 171, 219 | eqbrtrrd 4677 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
< ((2 · 𝑀)
− 1)) |
221 | 216, 217,
220 | ltled 10185 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
≤ ((2 · 𝑀)
− 1)) |
222 | 216, 217,
218, 221, 151 | letrd 10194 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
≤ 𝑁) |
223 | | nn0uz 11722 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
224 | 215, 223 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ (ℤ≥‘0)) |
225 | | elfz5 12334 |
. . . . . . . . . . 11
⊢ (((2
· (𝑀 − 1))
∈ (ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → ((2 · (𝑀 − 1)) ∈ (0...𝑁) ↔ (2 · (𝑀 − 1)) ≤ 𝑁)) |
226 | 224, 118,
225 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ → ((2
· (𝑀 − 1))
∈ (0...𝑁) ↔ (2
· (𝑀 − 1))
≤ 𝑁)) |
227 | 222, 226 | mpbird 247 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → (2
· (𝑀 − 1))
∈ (0...𝑁)) |
228 | | bccl2 13110 |
. . . . . . . . 9
⊢ ((2
· (𝑀 − 1))
∈ (0...𝑁) →
(𝑁C(2 · (𝑀 − 1))) ∈
ℕ) |
229 | 227, 228 | syl 17 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈
ℕ) |
230 | 229 | nnne0d 11065 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ≠ 0) |
231 | 212, 87, 230 | divcan3d 10806 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → (((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 ·
𝑀) · ((2 ·
𝑀) − 1)))) / (𝑁C(2 · (𝑀 − 1)))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) |
232 | 207, 231 | eqtrd 2656 |
. . . . 5
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1)))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) |
233 | 232 | oveq2d 6666 |
. . . 4
⊢ (𝑀 ∈ ℕ → (1 /
((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1))))) = (1 / (6 / ((2 ·
𝑀) · ((2 ·
𝑀) −
1))))) |
234 | 125, 87, 130, 230 | recdivd 10818 |
. . . 4
⊢ (𝑀 ∈ ℕ → (1 /
((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1))))) = ((𝑁C(2 · (𝑀 − 1))) / (𝑁C(2 · 𝑀)))) |
235 | 209 | nncnd 11036 |
. . . . 5
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · ((2
· 𝑀) − 1))
∈ ℂ) |
236 | 209 | nnne0d 11065 |
. . . . 5
⊢ (𝑀 ∈ ℕ → ((2
· 𝑀) · ((2
· 𝑀) − 1))
≠ 0) |
237 | | 6cn 11102 |
. . . . . 6
⊢ 6 ∈
ℂ |
238 | | 6nn 11189 |
. . . . . . 7
⊢ 6 ∈
ℕ |
239 | 238 | nnne0i 11055 |
. . . . . 6
⊢ 6 ≠
0 |
240 | | recdiv 10731 |
. . . . . 6
⊢ (((6
∈ ℂ ∧ 6 ≠ 0) ∧ (((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ ∧ ((2
· 𝑀) · ((2
· 𝑀) − 1))
≠ 0)) → (1 / (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) /
6)) |
241 | 237, 239,
240 | mpanl12 718 |
. . . . 5
⊢ ((((2
· 𝑀) · ((2
· 𝑀) − 1))
∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ≠ 0) → (1 / (6 / ((2
· 𝑀) · ((2
· 𝑀) − 1)))) =
(((2 · 𝑀) ·
((2 · 𝑀) − 1))
/ 6)) |
242 | 235, 236,
241 | syl2anc 693 |
. . . 4
⊢ (𝑀 ∈ ℕ → (1 / (6 /
((2 · 𝑀) ·
((2 · 𝑀) −
1)))) = (((2 · 𝑀)
· ((2 · 𝑀)
− 1)) / 6)) |
243 | 233, 234,
242 | 3eqtr3d 2664 |
. . 3
⊢ (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) / (𝑁C(2 · 𝑀))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) |
244 | 132, 136,
243 | 3eqtrd 2660 |
. 2
⊢ (𝑀 ∈ ℕ →
-(((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) /
6)) |
245 | 34, 49, 244 | 3eqtr3d 2664 |
1
⊢ (𝑀 ∈ ℕ →
Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) = (((2 ·
𝑀) · ((2 ·
𝑀) − 1)) /
6)) |