MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  basellem5 Structured version   Visualization version   GIF version

Theorem basellem5 27129
Description: Lemma for basel 27134. Using vieta1 26355, we can calculate the sum of the roots of 𝑃 as the quotient of the top two coefficients, and since the function 𝑇 enumerates the roots, we are left with an equation that sums the cot↑2 function at the 𝑀 different roots. (Contributed by Mario Carneiro, 29-Jul-2014.)
Hypotheses
Ref Expression
basel.n 𝑁 = ((2 · 𝑀) + 1)
basel.p 𝑃 = (𝑡 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀𝑗))) · (𝑡𝑗)))
basel.t 𝑇 = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2))
Assertion
Ref Expression
basellem5 (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6))
Distinct variable groups:   𝑗,𝑘,𝑡,𝑛,𝑀   𝑗,𝑁,𝑘,𝑛,𝑡   𝑃,𝑘,𝑛   𝑇,𝑘
Allowed substitution hints:   𝑃(𝑡,𝑗)   𝑇(𝑡,𝑗,𝑛)

Proof of Theorem basellem5
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef 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↑(𝑀𝑗))) · (𝑡𝑗)))
64, 5basellem2 27126 . . . 4 (𝑀 ∈ ℕ → (𝑃 ∈ (Poly‘ℂ) ∧ (deg‘𝑃) = 𝑀 ∧ (coeff‘𝑃) = (𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀𝑛))))))
76simp1d 1142 . . 3 (𝑀 ∈ ℕ → 𝑃 ∈ (Poly‘ℂ))
86simp2d 1143 . . . 4 (𝑀 ∈ ℕ → (deg‘𝑃) = 𝑀)
9 nnnn0 12535 . . . . 5 (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
10 hashfz1 14386 . . . . 5 (𝑀 ∈ ℕ0 → (♯‘(1...𝑀)) = 𝑀)
119, 10syl 17 . . . 4 (𝑀 ∈ ℕ → (♯‘(1...𝑀)) = 𝑀)
12 fzfid 14015 . . . . 5 (𝑀 ∈ ℕ → (1...𝑀) ∈ Fin)
13 basel.t . . . . . 6 𝑇 = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2))
144, 5, 13basellem4 27128 . . . . 5 (𝑀 ∈ ℕ → 𝑇:(1...𝑀)–1-1-onto→(𝑃 “ {0}))
1512, 14hasheqf1od 14393 . . . 4 (𝑀 ∈ ℕ → (♯‘(1...𝑀)) = (♯‘(𝑃 “ {0})))
168, 11, 153eqtr2rd 2783 . . 3 (𝑀 ∈ ℕ → (♯‘(𝑃 “ {0})) = (deg‘𝑃))
17 id 22 . . . 4 (𝑀 ∈ ℕ → 𝑀 ∈ ℕ)
188, 17eqeltrd 2840 . . 3 (𝑀 ∈ ℕ → (deg‘𝑃) ∈ ℕ)
191, 2, 3, 7, 16, 18vieta1 26355 . 2 (𝑀 ∈ ℕ → Σ𝑥 ∈ (𝑃 “ {0})𝑥 = -(((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))))
20 id 22 . . 3 (𝑥 = ((tan‘((𝑘 · π) / 𝑁))↑-2) → 𝑥 = ((tan‘((𝑘 · π) / 𝑁))↑-2))
21 oveq1 7439 . . . . . . 7 (𝑛 = 𝑘 → (𝑛 · π) = (𝑘 · π))
2221fvoveq1d 7454 . . . . . 6 (𝑛 = 𝑘 → (tan‘((𝑛 · π) / 𝑁)) = (tan‘((𝑘 · π) / 𝑁)))
2322oveq1d 7447 . . . . 5 (𝑛 = 𝑘 → ((tan‘((𝑛 · π) / 𝑁))↑-2) = ((tan‘((𝑘 · π) / 𝑁))↑-2))
24 ovex 7465 . . . . 5 ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ V
2523, 13, 24fvmpt 7015 . . . 4 (𝑘 ∈ (1...𝑀) → (𝑇𝑘) = ((tan‘((𝑘 · π) / 𝑁))↑-2))
2625adantl 481 . . 3 ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑇𝑘) = ((tan‘((𝑘 · π) / 𝑁))↑-2))
27 cnvimass 6099 . . . . 5 (𝑃 “ {0}) ⊆ dom 𝑃
28 plyf 26238 . . . . . 6 (𝑃 ∈ (Poly‘ℂ) → 𝑃:ℂ⟶ℂ)
29 fdm 6744 . . . . . 6 (𝑃:ℂ⟶ℂ → dom 𝑃 = ℂ)
307, 28, 293syl 18 . . . . 5 (𝑀 ∈ ℕ → dom 𝑃 = ℂ)
3127, 30sseqtrid 4025 . . . 4 (𝑀 ∈ ℕ → (𝑃 “ {0}) ⊆ ℂ)
3231sselda 3982 . . 3 ((𝑀 ∈ ℕ ∧ 𝑥 ∈ (𝑃 “ {0})) → 𝑥 ∈ ℂ)
3320, 12, 14, 26, 32fsumf1o 15760 . 2 (𝑀 ∈ ℕ → Σ𝑥 ∈ (𝑃 “ {0})𝑥 = Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2))
346simp3d 1144 . . . . . . 7 (𝑀 ∈ ℕ → (coeff‘𝑃) = (𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀𝑛)))))
358oveq1d 7447 . . . . . . 7 (𝑀 ∈ ℕ → ((deg‘𝑃) − 1) = (𝑀 − 1))
3634, 35fveq12d 6912 . . . . . 6 (𝑀 ∈ ℕ → ((coeff‘𝑃)‘((deg‘𝑃) − 1)) = ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀𝑛))))‘(𝑀 − 1)))
37 nnm1nn0 12569 . . . . . . 7 (𝑀 ∈ ℕ → (𝑀 − 1) ∈ ℕ0)
38 oveq2 7440 . . . . . . . . . 10 (𝑛 = (𝑀 − 1) → (2 · 𝑛) = (2 · (𝑀 − 1)))
3938oveq2d 7448 . . . . . . . . 9 (𝑛 = (𝑀 − 1) → (𝑁C(2 · 𝑛)) = (𝑁C(2 · (𝑀 − 1))))
40 oveq2 7440 . . . . . . . . . 10 (𝑛 = (𝑀 − 1) → (𝑀𝑛) = (𝑀 − (𝑀 − 1)))
4140oveq2d 7448 . . . . . . . . 9 (𝑛 = (𝑀 − 1) → (-1↑(𝑀𝑛)) = (-1↑(𝑀 − (𝑀 − 1))))
4239, 41oveq12d 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
4542, 43, 44fvmpt 7015 . . . . . . 7 ((𝑀 − 1) ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀𝑛))))‘(𝑀 − 1)) = ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))))
4637, 45syl 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)
5047, 48, 49sylancl 586 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑀 − (𝑀 − 1)) = 1)
5150oveq2d 7448 . . . . . . . . 9 (𝑀 ∈ ℕ → (-1↑(𝑀 − (𝑀 − 1))) = (-1↑1))
52 neg1cn 12381 . . . . . . . . . 10 -1 ∈ ℂ
53 exp1 14109 . . . . . . . . . 10 (-1 ∈ ℂ → (-1↑1) = -1)
5452, 53ax-mp 5 . . . . . . . . 9 (-1↑1) = -1
5551, 54eqtrdi 2792 . . . . . . . 8 (𝑀 ∈ ℕ → (-1↑(𝑀 − (𝑀 − 1))) = -1)
5655oveq2d 7448 . . . . . . 7 (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))) = ((𝑁C(2 · (𝑀 − 1))) · -1))
57 2nn 12340 . . . . . . . . . . . . . 14 2 ∈ ℕ
58 nnmulcl 12291 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
5957, 58mpan 690 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℕ)
6059peano2nnd 12284 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → ((2 · 𝑀) + 1) ∈ ℕ)
614, 60eqeltrid 2844 . . . . . . . . . . 11 (𝑀 ∈ ℕ → 𝑁 ∈ ℕ)
6261nnnn0d 12589 . . . . . . . . . 10 (𝑀 ∈ ℕ → 𝑁 ∈ ℕ0)
63 2z 12651 . . . . . . . . . . 11 2 ∈ ℤ
64 nnz 12636 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → 𝑀 ∈ ℤ)
65 peano2zm 12662 . . . . . . . . . . . 12 (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
6664, 65syl 17 . . . . . . . . . . 11 (𝑀 ∈ ℕ → (𝑀 − 1) ∈ ℤ)
67 zmulcl 12668 . . . . . . . . . . 11 ((2 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ) → (2 · (𝑀 − 1)) ∈ ℤ)
6863, 66, 67sylancr 587 . . . . . . . . . 10 (𝑀 ∈ ℕ → (2 · (𝑀 − 1)) ∈ ℤ)
69 bccl 14362 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (2 · (𝑀 − 1)) ∈ ℤ) → (𝑁C(2 · (𝑀 − 1))) ∈ ℕ0)
7062, 68, 69syl2anc 584 . . . . . . . . 9 (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈ ℕ0)
7170nn0cnd 12591 . . . . . . . 8 (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈ ℂ)
72 mulcom 11242 . . . . . . . 8 (((𝑁C(2 · (𝑀 − 1))) ∈ ℂ ∧ -1 ∈ ℂ) → ((𝑁C(2 · (𝑀 − 1))) · -1) = (-1 · (𝑁C(2 · (𝑀 − 1)))))
7371, 52, 72sylancl 586 . . . . . . 7 (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · -1) = (-1 · (𝑁C(2 · (𝑀 − 1)))))
7471mulm1d 11716 . . . . . . 7 (𝑀 ∈ ℕ → (-1 · (𝑁C(2 · (𝑀 − 1)))) = -(𝑁C(2 · (𝑀 − 1))))
7556, 73, 743eqtrd 2780 . . . . . 6 (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))) = -(𝑁C(2 · (𝑀 − 1))))
7636, 46, 753eqtrd 2780 . . . . 5 (𝑀 ∈ ℕ → ((coeff‘𝑃)‘((deg‘𝑃) − 1)) = -(𝑁C(2 · (𝑀 − 1))))
7771negcld 11608 . . . . 5 (𝑀 ∈ ℕ → -(𝑁C(2 · (𝑀 − 1))) ∈ ℂ)
7876, 77eqeltrd 2840 . . . 4 (𝑀 ∈ ℕ → ((coeff‘𝑃)‘((deg‘𝑃) − 1)) ∈ ℂ)
7934, 8fveq12d 6912 . . . . . 6 (𝑀 ∈ ℕ → ((coeff‘𝑃)‘(deg‘𝑃)) = ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀𝑛))))‘𝑀))
80 oveq2 7440 . . . . . . . . . 10 (𝑛 = 𝑀 → (2 · 𝑛) = (2 · 𝑀))
8180oveq2d 7448 . . . . . . . . 9 (𝑛 = 𝑀 → (𝑁C(2 · 𝑛)) = (𝑁C(2 · 𝑀)))
82 oveq2 7440 . . . . . . . . . 10 (𝑛 = 𝑀 → (𝑀𝑛) = (𝑀𝑀))
8382oveq2d 7448 . . . . . . . . 9 (𝑛 = 𝑀 → (-1↑(𝑀𝑛)) = (-1↑(𝑀𝑀)))
8481, 83oveq12d 7450 . . . . . . . 8 (𝑛 = 𝑀 → ((𝑁C(2 · 𝑛)) · (-1↑(𝑀𝑛))) = ((𝑁C(2 · 𝑀)) · (-1↑(𝑀𝑀))))
85 ovex 7465 . . . . . . . 8 ((𝑁C(2 · 𝑀)) · (-1↑(𝑀𝑀))) ∈ V
8684, 43, 85fvmpt 7015 . . . . . . 7 (𝑀 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀𝑛))))‘𝑀) = ((𝑁C(2 · 𝑀)) · (-1↑(𝑀𝑀))))
879, 86syl 17 . . . . . 6 (𝑀 ∈ ℕ → ((𝑛 ∈ ℕ0 ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀𝑛))))‘𝑀) = ((𝑁C(2 · 𝑀)) · (-1↑(𝑀𝑀))))
8847subidd 11609 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑀𝑀) = 0)
8988oveq2d 7448 . . . . . . . . 9 (𝑀 ∈ ℕ → (-1↑(𝑀𝑀)) = (-1↑0))
90 exp0 14107 . . . . . . . . . 10 (-1 ∈ ℂ → (-1↑0) = 1)
9152, 90ax-mp 5 . . . . . . . . 9 (-1↑0) = 1
9289, 91eqtrdi 2792 . . . . . . . 8 (𝑀 ∈ ℕ → (-1↑(𝑀𝑀)) = 1)
9392oveq2d 7448 . . . . . . 7 (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) · (-1↑(𝑀𝑀))) = ((𝑁C(2 · 𝑀)) · 1))
94 fz1ssfz0 13664 . . . . . . . . . . 11 (1...𝑁) ⊆ (0...𝑁)
9559nnred 12282 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℝ)
9695lep1d 12200 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → (2 · 𝑀) ≤ ((2 · 𝑀) + 1))
9796, 4breqtrrdi 5184 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → (2 · 𝑀) ≤ 𝑁)
98 nnuz 12922 . . . . . . . . . . . . . 14 ℕ = (ℤ‘1)
9959, 98eleqtrdi 2850 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → (2 · 𝑀) ∈ (ℤ‘1))
10061nnzd 12642 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → 𝑁 ∈ ℤ)
101 elfz5 13557 . . . . . . . . . . . . 13 (((2 · 𝑀) ∈ (ℤ‘1) ∧ 𝑁 ∈ ℤ) → ((2 · 𝑀) ∈ (1...𝑁) ↔ (2 · 𝑀) ≤ 𝑁))
10299, 100, 101syl2anc 584 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → ((2 · 𝑀) ∈ (1...𝑁) ↔ (2 · 𝑀) ≤ 𝑁))
10397, 102mpbird 257 . . . . . . . . . . 11 (𝑀 ∈ ℕ → (2 · 𝑀) ∈ (1...𝑁))
10494, 103sselid 3980 . . . . . . . . . 10 (𝑀 ∈ ℕ → (2 · 𝑀) ∈ (0...𝑁))
105 bccl2 14363 . . . . . . . . . 10 ((2 · 𝑀) ∈ (0...𝑁) → (𝑁C(2 · 𝑀)) ∈ ℕ)
106104, 105syl 17 . . . . . . . . 9 (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) ∈ ℕ)
107106nncnd 12283 . . . . . . . 8 (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) ∈ ℂ)
108107mulridd 11279 . . . . . . 7 (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) · 1) = (𝑁C(2 · 𝑀)))
10993, 108eqtrd 2776 . . . . . 6 (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) · (-1↑(𝑀𝑀))) = (𝑁C(2 · 𝑀)))
11079, 87, 1093eqtrd 2780 . . . . 5 (𝑀 ∈ ℕ → ((coeff‘𝑃)‘(deg‘𝑃)) = (𝑁C(2 · 𝑀)))
111110, 107eqeltrd 2840 . . . 4 (𝑀 ∈ ℕ → ((coeff‘𝑃)‘(deg‘𝑃)) ∈ ℂ)
112106nnne0d 12317 . . . . 5 (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) ≠ 0)
113110, 112eqnetrd 3007 . . . 4 (𝑀 ∈ ℕ → ((coeff‘𝑃)‘(deg‘𝑃)) ≠ 0)
11478, 111, 113divnegd 12057 . . 3 (𝑀 ∈ ℕ → -(((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))) = (-((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))))
11576negeqd 11503 . . . . 5 (𝑀 ∈ ℕ → -((coeff‘𝑃)‘((deg‘𝑃) − 1)) = --(𝑁C(2 · (𝑀 − 1))))
11671negnegd 11612 . . . . 5 (𝑀 ∈ ℕ → --(𝑁C(2 · (𝑀 − 1))) = (𝑁C(2 · (𝑀 − 1))))
117115, 116eqtrd 2776 . . . 4 (𝑀 ∈ ℕ → -((coeff‘𝑃)‘((deg‘𝑃) − 1)) = (𝑁C(2 · (𝑀 − 1))))
118117, 110oveq12d 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 · 𝑀))))
120103, 119syl 17 . . . . . . . . 9 (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) = ((𝑁C((2 · 𝑀) − 1)) · ((𝑁 − ((2 · 𝑀) − 1)) / (2 · 𝑀))))
12159nncnd 12283 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℂ)
122 1cnd 11257 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → 1 ∈ ℂ)
123121, 122, 122pnncand 11660 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) − ((2 · 𝑀) − 1)) = (1 + 1))
1244oveq1i 7442 . . . . . . . . . . . . . . . 16 (𝑁 − ((2 · 𝑀) − 1)) = (((2 · 𝑀) + 1) − ((2 · 𝑀) − 1))
125 df-2 12330 . . . . . . . . . . . . . . . 16 2 = (1 + 1)
126123, 124, 1253eqtr4g 2801 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → (𝑁 − ((2 · 𝑀) − 1)) = 2)
127 2nn0 12545 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
128126, 127eqeltrdi 2848 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → (𝑁 − ((2 · 𝑀) − 1)) ∈ ℕ0)
129 nnm1nn0 12569 . . . . . . . . . . . . . . . 16 ((2 · 𝑀) ∈ ℕ → ((2 · 𝑀) − 1) ∈ ℕ0)
13059, 129syl 17 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ∈ ℕ0)
131 nn0sub 12578 . . . . . . . . . . . . . . 15 ((((2 · 𝑀) − 1) ∈ ℕ0𝑁 ∈ ℕ0) → (((2 · 𝑀) − 1) ≤ 𝑁 ↔ (𝑁 − ((2 · 𝑀) − 1)) ∈ ℕ0))
132130, 62, 131syl2anc 584 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) ≤ 𝑁 ↔ (𝑁 − ((2 · 𝑀) − 1)) ∈ ℕ0))
133128, 132mpbird 257 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ≤ 𝑁)
134472timesd 12511 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℕ → (2 · 𝑀) = (𝑀 + 𝑀))
135134oveq1d 7447 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) = ((𝑀 + 𝑀) − 1))
13647, 47, 122addsubd 11642 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → ((𝑀 + 𝑀) − 1) = ((𝑀 − 1) + 𝑀))
137135, 136eqtrd 2776 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) = ((𝑀 − 1) + 𝑀))
138 nn0nnaddcl 12559 . . . . . . . . . . . . . . . . 17 (((𝑀 − 1) ∈ ℕ0𝑀 ∈ ℕ) → ((𝑀 − 1) + 𝑀) ∈ ℕ)
13937, 138mpancom 688 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → ((𝑀 − 1) + 𝑀) ∈ ℕ)
140137, 139eqeltrd 2840 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ∈ ℕ)
141140, 98eleqtrdi 2850 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ∈ (ℤ‘1))
142 elfz5 13557 . . . . . . . . . . . . . 14 ((((2 · 𝑀) − 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ ℤ) → (((2 · 𝑀) − 1) ∈ (1...𝑁) ↔ ((2 · 𝑀) − 1) ≤ 𝑁))
143141, 100, 142syl2anc 584 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) ∈ (1...𝑁) ↔ ((2 · 𝑀) − 1) ≤ 𝑁))
144133, 143mpbird 257 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ∈ (1...𝑁))
145 bcm1k 14355 . . . . . . . . . . . 12 (((2 · 𝑀) − 1) ∈ (1...𝑁) → (𝑁C((2 · 𝑀) − 1)) = ((𝑁C(((2 · 𝑀) − 1) − 1)) · ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2 · 𝑀) − 1))))
146144, 145syl 17 . . . . . . . . . . 11 (𝑀 ∈ ℕ → (𝑁C((2 · 𝑀) − 1)) = ((𝑁C(((2 · 𝑀) − 1) − 1)) · ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2 · 𝑀) − 1))))
147482timesi 12405 . . . . . . . . . . . . . . . 16 (2 · 1) = (1 + 1)
148147eqcomi 2745 . . . . . . . . . . . . . . 15 (1 + 1) = (2 · 1)
149148oveq2i 7443 . . . . . . . . . . . . . 14 ((2 · 𝑀) − (1 + 1)) = ((2 · 𝑀) − (2 · 1))
150121, 122, 122subsub4d 11652 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) − 1) = ((2 · 𝑀) − (1 + 1)))
151 2cnd 12345 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → 2 ∈ ℂ)
152151, 47, 122subdid 11720 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → (2 · (𝑀 − 1)) = ((2 · 𝑀) − (2 · 1)))
153149, 150, 1523eqtr4a 2802 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) − 1) = (2 · (𝑀 − 1)))
154153oveq2d 7448 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → (𝑁C(((2 · 𝑀) − 1) − 1)) = (𝑁C(2 · (𝑀 − 1))))
15561nncnd 12283 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → 𝑁 ∈ ℂ)
156140nncnd 12283 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ∈ ℂ)
157155, 156, 122subsubd 11649 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → (𝑁 − (((2 · 𝑀) − 1) − 1)) = ((𝑁 − ((2 · 𝑀) − 1)) + 1))
158126oveq1d 7447 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → ((𝑁 − ((2 · 𝑀) − 1)) + 1) = (2 + 1))
159 df-3 12331 . . . . . . . . . . . . . . 15 3 = (2 + 1)
160158, 159eqtr4di 2794 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ → ((𝑁 − ((2 · 𝑀) − 1)) + 1) = 3)
161157, 160eqtrd 2776 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → (𝑁 − (((2 · 𝑀) − 1) − 1)) = 3)
162161oveq1d 7447 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2 · 𝑀) − 1)) = (3 / ((2 · 𝑀) − 1)))
163154, 162oveq12d 7450 . . . . . . . . . . 11 (𝑀 ∈ ℕ → ((𝑁C(((2 · 𝑀) − 1) − 1)) · ((𝑁 − (((2 · 𝑀) − 1) − 1)) / ((2 · 𝑀) − 1))) = ((𝑁C(2 · (𝑀 − 1))) · (3 / ((2 · 𝑀) − 1))))
164146, 163eqtrd 2776 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑁C((2 · 𝑀) − 1)) = ((𝑁C(2 · (𝑀 − 1))) · (3 / ((2 · 𝑀) − 1))))
165126oveq1d 7447 . . . . . . . . . 10 (𝑀 ∈ ℕ → ((𝑁 − ((2 · 𝑀) − 1)) / (2 · 𝑀)) = (2 / (2 · 𝑀)))
166164, 165oveq12d 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)) ∈ ℝ)
169167, 140, 168sylancr 587 . . . . . . . . . . 11 (𝑀 ∈ ℕ → (3 / ((2 · 𝑀) − 1)) ∈ ℝ)
170169recnd 11290 . . . . . . . . . 10 (𝑀 ∈ ℕ → (3 / ((2 · 𝑀) − 1)) ∈ ℂ)
171 2re 12341 . . . . . . . . . . . 12 2 ∈ ℝ
172 nndivre 12308 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ (2 · 𝑀) ∈ ℕ) → (2 / (2 · 𝑀)) ∈ ℝ)
173171, 59, 172sylancr 587 . . . . . . . . . . 11 (𝑀 ∈ ℕ → (2 / (2 · 𝑀)) ∈ ℝ)
174173recnd 11290 . . . . . . . . . 10 (𝑀 ∈ ℕ → (2 / (2 · 𝑀)) ∈ ℂ)
17571, 170, 174mulassd 11285 . . . . . . . . 9 (𝑀 ∈ ℕ → (((𝑁C(2 · (𝑀 − 1))) · (3 / ((2 · 𝑀) − 1))) · (2 / (2 · 𝑀))) = ((𝑁C(2 · (𝑀 − 1))) · ((3 / ((2 · 𝑀) − 1)) · (2 / (2 · 𝑀)))))
176120, 166, 1753eqtrd 2780 . . . . . . . 8 (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) = ((𝑁C(2 · (𝑀 − 1))) · ((3 / ((2 · 𝑀) − 1)) · (2 / (2 · 𝑀)))))
177 3cn 12348 . . . . . . . . . . . 12 3 ∈ ℂ
178177a1i 11 . . . . . . . . . . 11 (𝑀 ∈ ℕ → 3 ∈ ℂ)
179140nnne0d 12317 . . . . . . . . . . 11 (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ≠ 0)
18059nnne0d 12317 . . . . . . . . . . 11 (𝑀 ∈ ℕ → (2 · 𝑀) ≠ 0)
181178, 156, 151, 121, 179, 180divmuldivd 12085 . . . . . . . . . 10 (𝑀 ∈ ℕ → ((3 / ((2 · 𝑀) − 1)) · (2 / (2 · 𝑀))) = ((3 · 2) / (((2 · 𝑀) − 1) · (2 · 𝑀))))
182 3t2e6 12433 . . . . . . . . . . . 12 (3 · 2) = 6
183182a1i 11 . . . . . . . . . . 11 (𝑀 ∈ ℕ → (3 · 2) = 6)
184156, 121mulcomd 11283 . . . . . . . . . . 11 (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) · (2 · 𝑀)) = ((2 · 𝑀) · ((2 · 𝑀) − 1)))
185183, 184oveq12d 7450 . . . . . . . . . 10 (𝑀 ∈ ℕ → ((3 · 2) / (((2 · 𝑀) − 1) · (2 · 𝑀))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1))))
186181, 185eqtrd 2776 . . . . . . . . 9 (𝑀 ∈ ℕ → ((3 / ((2 · 𝑀) − 1)) · (2 / (2 · 𝑀))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1))))
187186oveq2d 7448 . . . . . . . 8 (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) · ((3 / ((2 · 𝑀) − 1)) · (2 / (2 · 𝑀)))) = ((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))))
188176, 187eqtrd 2776 . . . . . . 7 (𝑀 ∈ ℕ → (𝑁C(2 · 𝑀)) = ((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))))
189188oveq1d 7447 . . . . . 6 (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1)))) = (((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) / (𝑁C(2 · (𝑀 − 1)))))
190 6re 12357 . . . . . . . . 9 6 ∈ ℝ
19159, 140nnmulcld 12320 . . . . . . . . 9 (𝑀 ∈ ℕ → ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℕ)
192 nndivre 12308 . . . . . . . . 9 ((6 ∈ ℝ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℕ) → (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1))) ∈ ℝ)
193190, 191, 192sylancr 587 . . . . . . . 8 (𝑀 ∈ ℕ → (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1))) ∈ ℝ)
194193recnd 11290 . . . . . . 7 (𝑀 ∈ ℕ → (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1))) ∈ ℂ)
195 nnm1nn0 12569 . . . . . . . . . . . . . 14 (((2 · 𝑀) − 1) ∈ ℕ → (((2 · 𝑀) − 1) − 1) ∈ ℕ0)
196140, 195syl 17 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) − 1) ∈ ℕ0)
197153, 196eqeltrrd 2841 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → (2 · (𝑀 − 1)) ∈ ℕ0)
198197nn0red 12590 . . . . . . . . . . 11 (𝑀 ∈ ℕ → (2 · (𝑀 − 1)) ∈ ℝ)
199140nnred 12282 . . . . . . . . . . 11 (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ∈ ℝ)
20061nnred 12282 . . . . . . . . . . 11 (𝑀 ∈ ℕ → 𝑁 ∈ ℝ)
201199ltm1d 12201 . . . . . . . . . . . . 13 (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) − 1) < ((2 · 𝑀) − 1))
202153, 201eqbrtrrd 5166 . . . . . . . . . . . 12 (𝑀 ∈ ℕ → (2 · (𝑀 − 1)) < ((2 · 𝑀) − 1))
203198, 199, 202ltled 11410 . . . . . . . . . . 11 (𝑀 ∈ ℕ → (2 · (𝑀 − 1)) ≤ ((2 · 𝑀) − 1))
204198, 199, 200, 203, 133letrd 11419 . . . . . . . . . 10 (𝑀 ∈ ℕ → (2 · (𝑀 − 1)) ≤ 𝑁)
205 nn0uz 12921 . . . . . . . . . . . 12 0 = (ℤ‘0)
206197, 205eleqtrdi 2850 . . . . . . . . . . 11 (𝑀 ∈ ℕ → (2 · (𝑀 − 1)) ∈ (ℤ‘0))
207 elfz5 13557 . . . . . . . . . . 11 (((2 · (𝑀 − 1)) ∈ (ℤ‘0) ∧ 𝑁 ∈ ℤ) → ((2 · (𝑀 − 1)) ∈ (0...𝑁) ↔ (2 · (𝑀 − 1)) ≤ 𝑁))
208206, 100, 207syl2anc 584 . . . . . . . . . 10 (𝑀 ∈ ℕ → ((2 · (𝑀 − 1)) ∈ (0...𝑁) ↔ (2 · (𝑀 − 1)) ≤ 𝑁))
209204, 208mpbird 257 . . . . . . . . 9 (𝑀 ∈ ℕ → (2 · (𝑀 − 1)) ∈ (0...𝑁))
210 bccl2 14363 . . . . . . . . 9 ((2 · (𝑀 − 1)) ∈ (0...𝑁) → (𝑁C(2 · (𝑀 − 1))) ∈ ℕ)
211209, 210syl 17 . . . . . . . 8 (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈ ℕ)
212211nnne0d 12317 . . . . . . 7 (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ≠ 0)
213194, 71, 212divcan3d 12049 . . . . . 6 (𝑀 ∈ ℕ → (((𝑁C(2 · (𝑀 − 1))) · (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) / (𝑁C(2 · (𝑀 − 1)))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1))))
214189, 213eqtrd 2776 . . . . 5 (𝑀 ∈ ℕ → ((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1)))) = (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1))))
215214oveq2d 7448 . . . 4 (𝑀 ∈ ℕ → (1 / ((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1))))) = (1 / (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))))
216107, 71, 112, 212recdivd 12061 . . . 4 (𝑀 ∈ ℕ → (1 / ((𝑁C(2 · 𝑀)) / (𝑁C(2 · (𝑀 − 1))))) = ((𝑁C(2 · (𝑀 − 1))) / (𝑁C(2 · 𝑀))))
217191nncnd 12283 . . . . 5 (𝑀 ∈ ℕ → ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ)
218191nnne0d 12317 . . . . 5 (𝑀 ∈ ℕ → ((2 · 𝑀) · ((2 · 𝑀) − 1)) ≠ 0)
219 6cn 12358 . . . . . 6 6 ∈ ℂ
220 6nn 12356 . . . . . . 7 6 ∈ ℕ
221220nnne0i 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))
223219, 221, 222mpanl12 702 . . . . 5 ((((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ≠ 0) → (1 / (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6))
224217, 218, 223syl2anc 584 . . . 4 (𝑀 ∈ ℕ → (1 / (6 / ((2 · 𝑀) · ((2 · 𝑀) − 1)))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6))
225215, 216, 2243eqtr3d 2784 . . 3 (𝑀 ∈ ℕ → ((𝑁C(2 · (𝑀 − 1))) / (𝑁C(2 · 𝑀))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6))
226114, 118, 2253eqtrd 2780 . 2 (𝑀 ∈ ℕ → -(((coeff‘𝑃)‘((deg‘𝑃) − 1)) / ((coeff‘𝑃)‘(deg‘𝑃))) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6))
22719, 33, 2263eqtr3d 2784 1 (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1539  wcel 2107  wne 2939  {csn 4625   class class class wbr 5142  cmpt 5224  ccnv 5683  dom cdm 5684  cima 5687  wf 6556  cfv 6560  (class class class)co 7432  Fincfn 8986  cc 11154  cr 11155  0cc0 11156  1c1 11157   + caddc 11159   · cmul 11161   < clt 11296  cle 11297  cmin 11493  -cneg 11494   / cdiv 11921  cn 12267  2c2 12322  3c3 12323  6c6 12326  0cn0 12528  cz 12615  cuz 12879  ...cfz 13548  cexp 14103  Ccbc 14342  chash 14370  Σcsu 15723  tanctan 16102  πcpi 16103  Polycply 26224  coeffccoe 26226  degcdgr 26227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-inf2 9682  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234  ax-addf 11235
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-iin 4993  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-se 5637  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-of 7698  df-om 7889  df-1st 8015  df-2nd 8016  df-supp 8187  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-2o 8508  df-oadd 8511  df-er 8746  df-map 8869  df-pm 8870  df-ixp 8939  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-fsupp 9403  df-fi 9452  df-sup 9483  df-inf 9484  df-oi 9551  df-dju 9942  df-card 9980  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-nn 12268  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337  df-n0 12529  df-xnn0 12602  df-z 12616  df-dec 12736  df-uz 12880  df-q 12992  df-rp 13036  df-xneg 13155  df-xadd 13156  df-xmul 13157  df-ioo 13392  df-ioc 13393  df-ico 13394  df-icc 13395  df-fz 13549  df-fzo 13696  df-fl 13833  df-mod 13911  df-seq 14044  df-exp 14104  df-fac 14314  df-bc 14343  df-hash 14371  df-shft 15107  df-cj 15139  df-re 15140  df-im 15141  df-sqrt 15275  df-abs 15276  df-limsup 15508  df-clim 15525  df-rlim 15526  df-sum 15724  df-ef 16104  df-sin 16106  df-cos 16107  df-tan 16108  df-pi 16109  df-struct 17185  df-sets 17202  df-slot 17220  df-ndx 17232  df-base 17249  df-ress 17276  df-plusg 17311  df-mulr 17312  df-starv 17313  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-hom 17322  df-cco 17323  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18654  df-sgrp 18733  df-mnd 18749  df-submnd 18798  df-mulg 19087  df-cntz 19336  df-cmn 19801  df-psmet 21357  df-xmet 21358  df-met 21359  df-bl 21360  df-mopn 21361  df-fbas 21362  df-fg 21363  df-cnfld 21366  df-top 22901  df-topon 22918  df-topsp 22940  df-bases 22954  df-cld 23028  df-ntr 23029  df-cls 23030  df-nei 23107  df-lp 23145  df-perf 23146  df-cn 23236  df-cnp 23237  df-haus 23324  df-tx 23571  df-hmeo 23764  df-fil 23855  df-fm 23947  df-flim 23948  df-flf 23949  df-xms 24331  df-ms 24332  df-tms 24333  df-cncf 24905  df-0p 25706  df-limc 25902  df-dv 25903  df-ply 26228  df-idp 26229  df-coe 26230  df-dgr 26231  df-quot 26334
This theorem is referenced by:  basellem8  27132
  Copyright terms: Public domain W3C validator