basellem5 - Metamath Proof Explorer

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

Theorem basellem5 25031

Description: Lemma for basel 25036. Using vieta1 24286, 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.

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‘𝑃) = (𝑛 ∈ ℕ₀ ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))))
7	6	simp1d 1137	. . 3 ⊢ (𝑀 ∈ ℕ → 𝑃 ∈ (Poly‘ℂ))
8	6	simp2d 1138	. . . 4 ⊢ (𝑀 ∈ ℕ → (deg‘𝑃) = 𝑀)
9		nnnn0 11511	. . . . 5 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
10		hashfz1 13348	. . . . 5 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(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‘𝑃) = (𝑛 ∈ ℕ₀ ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛)))))
51	8	oveq1d 6829	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((deg‘𝑃) − 1) = (𝑀 − 1))
52	50, 51	fveq12d 6359	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((coeff‘𝑃)‘((deg‘𝑃) − 1)) = ((𝑛 ∈ ℕ₀ ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘(𝑀 − 1)))
53		nnm1nn0 11546	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈ ℕ₀)
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 ⊢ (𝑛 ∈ ℕ₀ ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛)))) = (𝑛 ∈ ℕ₀ ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))
60		ovex 6842	. . . . . . . 8 ⊢ ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))) ∈ V
61	58, 59, 60	fvmpt 6445	. . . . . . 7 ⊢ ((𝑀 − 1) ∈ ℕ₀ → ((𝑛 ∈ ℕ₀ ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘(𝑀 − 1)) = ((𝑁C(2 · (𝑀 − 1))) · (-1↑(𝑀 − (𝑀 − 1)))))
62	53, 61	syl 17	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((𝑛 ∈ ℕ₀ ↦ ((𝑁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 ⊢ (𝑀 ∈ ℕ → 𝑁 ∈ ℕ₀)
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 ⊢ ((𝑁 ∈ ℕ₀ ∧ (2 · (𝑀 − 1)) ∈ ℤ) → (𝑁C(2 · (𝑀 − 1))) ∈ ℕ₀)
86	78, 84, 85	syl2anc 696	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (𝑁C(2 · (𝑀 − 1))) ∈ ℕ₀)
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‘𝑃)) = ((𝑛 ∈ ℕ₀ ↦ ((𝑁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 ⊢ (𝑀 ∈ ℕ₀ → ((𝑛 ∈ ℕ₀ ↦ ((𝑁C(2 · 𝑛)) · (-1↑(𝑀 − 𝑛))))‘𝑀) = ((𝑁C(2 · 𝑀)) · (-1↑(𝑀 − 𝑀))))
103	9, 102	syl 17	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((𝑛 ∈ ℕ₀ ↦ ((𝑁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 ∈ ℕ₀
144	142, 143	syl6eqel 2847	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (𝑁 − ((2 · 𝑀) − 1)) ∈ ℕ₀)
145		nnm1nn0 11546	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 𝑀) ∈ ℕ → ((2 · 𝑀) − 1) ∈ ℕ₀)
146	75, 145	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ∈ ℕ₀)
147		nn0sub 11555	. . . . . . . . . . . . . . 15 ⊢ ((((2 · 𝑀) − 1) ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (((2 · 𝑀) − 1) ≤ 𝑁 ↔ (𝑁 − ((2 · 𝑀) − 1)) ∈ ℕ₀))
148	146, 78, 147	syl2anc 696	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) ≤ 𝑁 ↔ (𝑁 − ((2 · 𝑀) − 1)) ∈ ℕ₀))
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) ∈ ℕ₀ ∧ 𝑀 ∈ ℕ) → ((𝑀 − 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) ∈ ℕ₀)
212	156, 211	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) − 1) ∈ ℕ₀)
213	169, 212	eqeltrrd 2840	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (2 · (𝑀 − 1)) ∈ ℕ₀)
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)
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))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1632 ∈ wcel 2139 ≠ wne 2932 {csn 4321 class class class wbr 4804 ↦ cmpt 4881 ^◡ccnv 5265 dom cdm 5266 “ cima 5269 ⟶wf 6045 –1-1-onto→wf1o 6048 ‘cfv 6049 (class class class)co 6814 ≈ cen 8120 Fincfn 8123 ℂcc 10146 ℝcr 10147 0cc0 10148 1c1 10149 + caddc 10151 · cmul 10153 < clt 10286 ≤ cle 10287 − cmin 10478 -cneg 10479 / cdiv 10896 ℕcn 11232 2c2 11282 3c3 11283 6c6 11286 ℕ₀cn0 11504 ℤcz 11589 ℤ_≥cuz 11899 ...cfz 12539 ↑cexp 13074 Ccbc 13303 ♯chash 13331 Σcsu 14635 tanctan 15015 πcpi 15016 0_𝑝c0p 23655 Polycply 24159 coeffccoe 24161 degcdgr 24162

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-8 2141 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-rep 4923 ax-sep 4933 ax-nul 4941 ax-pow 4992 ax-pr 5055 ax-un 7115 ax-inf2 8713 ax-cnex 10204 ax-resscn 10205 ax-1cn 10206 ax-icn 10207 ax-addcl 10208 ax-addrcl 10209 ax-mulcl 10210 ax-mulrcl 10211 ax-mulcom 10212 ax-addass 10213 ax-mulass 10214 ax-distr 10215 ax-i2m1 10216 ax-1ne0 10217 ax-1rid 10218 ax-rnegex 10219 ax-rrecex 10220 ax-cnre 10221 ax-pre-lttri 10222 ax-pre-lttrn 10223 ax-pre-ltadd 10224 ax-pre-mulgt0 10225 ax-pre-sup 10226 ax-addf 10227 ax-mulf 10228

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-fal 1638 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-mo 2612 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ne 2933 df-nel 3036 df-ral 3055 df-rex 3056 df-reu 3057 df-rmo 3058 df-rab 3059 df-v 3342 df-sbc 3577 df-csb 3675 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-pss 3731 df-nul 4059 df-if 4231 df-pw 4304 df-sn 4322 df-pr 4324 df-tp 4326 df-op 4328 df-uni 4589 df-int 4628 df-iun 4674 df-iin 4675 df-br 4805 df-opab 4865 df-mpt 4882 df-tr 4905 df-id 5174 df-eprel 5179 df-po 5187 df-so 5188 df-fr 5225 df-se 5226 df-we 5227 df-xp 5272 df-rel 5273 df-cnv 5274 df-co 5275 df-dm 5276 df-rn 5277 df-res 5278 df-ima 5279 df-pred 5841 df-ord 5887 df-on 5888 df-lim 5889 df-suc 5890 df-iota 6012 df-fun 6051 df-fn 6052 df-f 6053 df-f1 6054 df-fo 6055 df-f1o 6056 df-fv 6057 df-isom 6058 df-riota 6775 df-ov 6817 df-oprab 6818 df-mpt2 6819 df-of 7063 df-om 7232 df-1st 7334 df-2nd 7335 df-supp 7465 df-wrecs 7577 df-recs 7638 df-rdg 7676 df-1o 7730 df-2o 7731 df-oadd 7734 df-er 7913 df-map 8027 df-pm 8028 df-ixp 8077 df-en 8124 df-dom 8125 df-sdom 8126 df-fin 8127 df-fsupp 8443 df-fi 8484 df-sup 8515 df-inf 8516 df-oi 8582 df-card 8975 df-cda 9202 df-pnf 10288 df-mnf 10289 df-xr 10290 df-ltxr 10291 df-le 10292 df-sub 10480 df-neg 10481 df-div 10897 df-nn 11233 df-2 11291 df-3 11292 df-4 11293 df-5 11294 df-6 11295 df-7 11296 df-8 11297 df-9 11298 df-n0 11505 df-xnn0 11576 df-z 11590 df-dec 11706 df-uz 11900 df-q 12002 df-rp 12046 df-xneg 12159 df-xadd 12160 df-xmul 12161 df-ioo 12392 df-ioc 12393 df-ico 12394 df-icc 12395 df-fz 12540 df-fzo 12680 df-fl 12807 df-mod 12883 df-seq 13016 df-exp 13075 df-fac 13275 df-bc 13304 df-hash 13332 df-shft 14026 df-cj 14058 df-re 14059 df-im 14060 df-sqrt 14194 df-abs 14195 df-limsup 14421 df-clim 14438 df-rlim 14439 df-sum 14636 df-ef 15017 df-sin 15019 df-cos 15020 df-tan 15021 df-pi 15022 df-struct 16081 df-ndx 16082 df-slot 16083 df-base 16085 df-sets 16086 df-ress 16087 df-plusg 16176 df-mulr 16177 df-starv 16178 df-sca 16179 df-vsca 16180 df-ip 16181 df-tset 16182 df-ple 16183 df-ds 16186 df-unif 16187 df-hom 16188 df-cco 16189 df-rest 16305 df-topn 16306 df-0g 16324 df-gsum 16325 df-topgen 16326 df-pt 16327 df-prds 16330 df-xrs 16384 df-qtop 16389 df-imas 16390 df-xps 16392 df-mre 16468 df-mrc 16469 df-acs 16471 df-mgm 17463 df-sgrp 17505 df-mnd 17516 df-submnd 17557 df-mulg 17762 df-cntz 17970 df-cmn 18415 df-psmet 19960 df-xmet 19961 df-met 19962 df-bl 19963 df-mopn 19964 df-fbas 19965 df-fg 19966 df-cnfld 19969 df-top 20921 df-topon 20938 df-topsp 20959 df-bases 20972 df-cld 21045 df-ntr 21046 df-cls 21047 df-nei 21124 df-lp 21162 df-perf 21163 df-cn 21253 df-cnp 21254 df-haus 21341 df-tx 21587 df-hmeo 21780 df-fil 21871 df-fm 21963 df-flim 21964 df-flf 21965 df-xms 22346 df-ms 22347 df-tms 22348 df-cncf 22902 df-0p 23656 df-limc 23849 df-dv 23850 df-ply 24163 df-idp 24164 df-coe 24165 df-dgr 24166 df-quot 24265

This theorem is referenced by: basellem8 25034

W3C validator