basellem8 - Metamath Proof Explorer

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

Theorem basellem8 27420

Description: Lemma for basel 27422. The function 𝐹 of partial sums of the inverse squares is bounded below by 𝐽 and above by 𝐾, obtained by summing the inequality cot↑2𝑥 ≤ 1 / 𝑥↑2 ≤ csc↑2𝑥 = cot↑2𝑥 + 1 over the 𝑀 roots of the polynomial 𝑃, and applying the identity basellem5 27417. (Contributed by Mario Carneiro, 29-Jul-2014.)

**Hypotheses**
Ref	Expression
basel.g	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
basel.f	⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑ -2)))
basel.h	⊢ 𝐻 = ((ℕ × {((π↑2) / 6)}) ∘_f · ((ℕ × {1}) ∘_f − 𝐺))
basel.j	⊢ 𝐽 = (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × { -2}) ∘_f · 𝐺)))
basel.k	⊢ 𝐾 = (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺))
basellem8.n	⊢ 𝑁 = ((2 · 𝑀) + 1)

**Assertion**
Ref	Expression
basellem8	⊢ (𝑀 ∈ ℕ → ((𝐽‘𝑀) ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ (𝐾‘𝑀)))

Distinct variable groups: 𝑛,𝐹 𝑛,𝑀 𝑛,𝐽 𝑛,𝑁 Allowed substitution hints: 𝐺(𝑛) 𝐻(𝑛) 𝐾(𝑛)

Proof of Theorem basellem8 Dummy variables 𝑘 𝑥 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 14119	. . . 4 ⊢ (𝑀 ∈ ℕ → (1...𝑀) ∈ Fin)
2		pire 26788	. . . . . . . 8 ⊢ π ∈ ℝ
3		basellem8.n	. . . . . . . . 9 ⊢ 𝑁 = ((2 · 𝑀) + 1)
4		2nn 12419	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
5		nnmulcl 12362	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
6	4, 5	mpan 703	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℕ)
7	6	peano2nnd 12355	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) + 1) ∈ ℕ)
8	3, 7	eqeltrid 2864	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → 𝑁 ∈ ℕ)
9		nndivre 12382	. . . . . . . 8 ⊢ ((π ∈ ℝ ∧ 𝑁 ∈ ℕ) → (π / 𝑁) ∈ ℝ)
10	2, 8, 9	sylancr 599	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (π / 𝑁) ∈ ℝ)
11	10	resqcld 14271	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) ∈ ℝ)
12	11	adantr 486	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℝ)
13	3	basellem1 27413	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)))
14		tanrpcl 26838	. . . . . . . 8 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
15	13, 14	syl 18	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
16	15	rpred 13167	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ)
17	15	rpne0d 13172	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ≠ 0)
18		2z 12731	. . . . . . . 8 ⊢ 2 ∈ ℤ
19		znegcl 12734	. . . . . . . 8 ⊢ (2 ∈ ℤ → -2 ∈ ℤ)
20	18, 19	ax-mp 5	. . . . . . 7 ⊢ -2 ∈ ℤ
21	20	a1i 11	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → -2 ∈ ℤ)
22	16, 17, 21	reexpclzd 14396	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑ -2) ∈ ℝ)
23	12, 22	remulcld 11342	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑ -2)) ∈ ℝ)
24		elfznn 13690	. . . . . . 7 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ)
25	24	adantl 487	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℕ)
26	25	nnred 12353	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ)
27	25	nnne0d 12391	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ≠ 0)
28	26, 27, 21	reexpclzd 14396	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑ -2) ∈ ℝ)
29	15	rpcnd 13169	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℂ)
30		2nn0 12626	. . . . . . . 8 ⊢ 2 ∈ ℕ₀
31		expneg 14215	. . . . . . . 8 ⊢ (((tan‘((𝑘 · π) / 𝑁)) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((tan‘((𝑘 · π) / 𝑁))↑ -2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)))
32	29, 30, 31	sylancl 598	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑ -2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)))
33	32	oveq2d 7436	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑ -2)) = (((π / 𝑁)↑2) · (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))))
34	10	recnd 11340	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (π / 𝑁) ∈ ℂ)
35	34	sqcld 14290	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) ∈ ℂ)
36	35	adantr 486	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℂ)
37		rpexpcl 14226	. . . . . . . . 9 ⊢ (((tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
38	15, 18, 37	sylancl 598	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
39	38	rpcnd 13169	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
40	38	rpne0d 13172	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
41	36, 39, 40	divrecd 12099	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))))
42	33, 41	eqtr4d 2798	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑ -2)) = (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)))
43	25	nnrpd 13165	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ⁺)
44		rpexpcl 14226	. . . . . . 7 ⊢ ((𝑘 ∈ ℝ⁺ ∧ -2 ∈ ℤ) → (𝑘↑ -2) ∈ ℝ⁺)
45	43, 20, 44	sylancl 598	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑ -2) ∈ ℝ⁺)
46	25	nncnd 12354	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℂ)
47	46, 27, 21	expnegd 14299	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑ - -2) = (1 / (𝑘↑ -2)))
48		2cn 12421	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
49	48	negnegi 11631	. . . . . . . . . . 11 ⊢ - -2 = 2
50	49	oveq2i 7431	. . . . . . . . . 10 ⊢ (𝑘↑ - -2) = (𝑘↑2)
51	47, 50	eqtr3di 2810	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (𝑘↑ -2)) = (𝑘↑2))
52	51	oveq1d 7435	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((1 / (𝑘↑ -2)) · ((π / 𝑁)↑2)) = ((𝑘↑2) · ((π / 𝑁)↑2)))
53		nncn 12346	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
54		nnne0 12375	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0)
55	20	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → -2 ∈ ℤ)
56	53, 54, 55	expclzd 14297	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝑘↑ -2) ∈ ℂ)
57	25, 56	syl 18	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑ -2) ∈ ℂ)
58	46, 27, 21	expne0d 14298	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑ -2) ≠ 0)
59	36, 57, 58	divrec2d 12100	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑ -2)) = ((1 / (𝑘↑ -2)) · ((π / 𝑁)↑2)))
60		picn 26790	. . . . . . . . . . . 12 ⊢ π ∈ ℂ
61	60	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → π ∈ ℂ)
62	8	nncnd 12354	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 𝑁 ∈ ℂ)
63	62	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑁 ∈ ℂ)
64	8	nnne0d 12391	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 𝑁 ≠ 0)
65	64	adantr 486	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑁 ≠ 0)
66	46, 61, 63, 65	divassd 12131	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) = (𝑘 · (π / 𝑁)))
67	66	oveq1d 7435	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘 · (π / 𝑁))↑2))
68	34	adantr 486	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (π / 𝑁) ∈ ℂ)
69	46, 68	sqmuld 14304	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · (π / 𝑁))↑2) = ((𝑘↑2) · ((π / 𝑁)↑2)))
70	67, 69	eqtrd 2795	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘↑2) · ((π / 𝑁)↑2)))
71	52, 59, 70	3eqtr4d 2805	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑ -2)) = (((𝑘 · π) / 𝑁)↑2))
72		elioore 13509	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → ((𝑘 · π) / 𝑁) ∈ ℝ)
73	13, 72	syl 18	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℝ)
74	73	resqcld 14271	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ∈ ℝ)
75	38	rpred 13167	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ)
76		tangtx 26839	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → ((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)))
77	13, 76	syl 18	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)))
78		eliooord 13539	. . . . . . . . . . . . . 14 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (0 < ((𝑘 · π) / 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π / 2)))
79	13, 78	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < ((𝑘 · π) / 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π / 2)))
80	79	simpld 500	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < ((𝑘 · π) / 𝑁))
81	73, 80	elrpd 13164	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℝ⁺)
82	81	rpge0d 13171	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ ((𝑘 · π) / 𝑁))
83	15	rpge0d 13171	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (tan‘((𝑘 · π) / 𝑁)))
84	73, 16, 82, 83	lt2sqd 14403	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)) ↔ (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2)))
85	77, 84	mpbid 235	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2))
86	74, 75, 85	ltled 11461	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2))
87	71, 86	eqbrtrd 5126	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑ -2)) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2))
88	12, 45, 38, 87	lediv23d 13235	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) ≤ (𝑘↑ -2))
89	42, 88	eqbrtrd 5126	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑ -2)) ≤ (𝑘↑ -2))
90	1, 23, 28, 89	fsumle 15971	. . 3 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑ -2)) ≤ Σ𝑘 ∈ (1...𝑀)(𝑘↑ -2))
91		oveq2 7428	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑀 → (2 · 𝑛) = (2 · 𝑀))
92	91	oveq1d 7435	. . . . . . . . . 10 ⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = ((2 · 𝑀) + 1))
93	92, 3	eqtr4di 2813	. . . . . . . . 9 ⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = 𝑁)
94	93	oveq2d 7436	. . . . . . . 8 ⊢ (𝑛 = 𝑀 → (1 / ((2 · 𝑛) + 1)) = (1 / 𝑁))
95	94	oveq2d 7436	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / 𝑁)))
96	95	oveq2d 7436	. . . . . 6 ⊢ (𝑛 = 𝑀 → (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) = (((π↑2) / 6) · (1 − (1 / 𝑁))))
97	94	oveq2d 7436	. . . . . . 7 ⊢ (𝑛 = 𝑀 → ( -2 · (1 / ((2 · 𝑛) + 1))) = ( -2 · (1 / 𝑁)))
98	97	oveq2d 7436	. . . . . 6 ⊢ (𝑛 = 𝑀 → (1 + ( -2 · (1 / ((2 · 𝑛) + 1)))) = (1 + ( -2 · (1 / 𝑁))))
99	96, 98	oveq12d 7438	. . . . 5 ⊢ (𝑛 = 𝑀 → ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + ( -2 · (1 / ((2 · 𝑛) + 1))))) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + ( -2 · (1 / 𝑁)))))
100		basel.j	. . . . . 6 ⊢ 𝐽 = (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × { -2}) ∘_f · 𝐺)))
101		nnex 12344	. . . . . . . . 9 ⊢ ℕ ∈ V
102	101	a1i 11	. . . . . . . 8 ⊢ (⊤ → ℕ ∈ V)
103		ovexd 7455	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V)
104		ovexd 7455	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 + ( -2 · (1 / ((2 · 𝑛) + 1)))) ∈ V)
105		basel.h	. . . . . . . . 9 ⊢ 𝐻 = ((ℕ × {((π↑2) / 6)}) ∘_f · ((ℕ × {1}) ∘_f − 𝐺))
106	2	resqcli 14332	. . . . . . . . . . . 12 ⊢ (π↑2) ∈ ℝ
107		6re 12436	. . . . . . . . . . . 12 ⊢ 6 ∈ ℝ
108		6nn 12435	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ
109	108	nnne0i 12381	. . . . . . . . . . . 12 ⊢ 6 ≠ 0
110	106, 107, 109	redivcli 12087	. . . . . . . . . . 11 ⊢ ((π↑2) / 6) ∈ ℝ
111	110	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ((π↑2) / 6) ∈ ℝ)
112		ovexd 7455	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / ((2 · 𝑛) + 1))) ∈ V)
113		fconstmpt 5712	. . . . . . . . . . 11 ⊢ (ℕ × {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) / 6))
114	113	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℕ × {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) / 6)))
115		1zzd 12730	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℤ)
116		ovexd 7455	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / ((2 · 𝑛) + 1)) ∈ V)
117		fconstmpt 5712	. . . . . . . . . . . 12 ⊢ (ℕ × {1}) = (𝑛 ∈ ℕ ↦ 1)
118	117	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (ℕ × {1}) = (𝑛 ∈ ℕ ↦ 1))
119		basel.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
120	119	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))))
121	102, 115, 116, 118, 120	offval2 7713	. . . . . . . . . 10 ⊢ (⊤ → ((ℕ × {1}) ∘_f − 𝐺) = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
122	102, 111, 112, 114, 121	offval2 7713	. . . . . . . . 9 ⊢ (⊤ → ((ℕ × {((π↑2) / 6)}) ∘_f · ((ℕ × {1}) ∘_f − 𝐺)) = (𝑛 ∈ ℕ ↦ (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1))))))
123	105, 122	eqtrid 2807	. . . . . . . 8 ⊢ (⊤ → 𝐻 = (𝑛 ∈ ℕ ↦ (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1))))))
124		ovexd 7455	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ( -2 · (1 / ((2 · 𝑛) + 1))) ∈ V)
125	48	negcli 11629	. . . . . . . . . . 11 ⊢ -2 ∈ ℂ
126	125	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → -2 ∈ ℂ)
127		fconstmpt 5712	. . . . . . . . . . 11 ⊢ (ℕ × { -2}) = (𝑛 ∈ ℕ ↦ -2)
128	127	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℕ × { -2}) = (𝑛 ∈ ℕ ↦ -2))
129	102, 126, 116, 128, 120	offval2 7713	. . . . . . . . 9 ⊢ (⊤ → ((ℕ × { -2}) ∘_f · 𝐺) = (𝑛 ∈ ℕ ↦ ( -2 · (1 / ((2 · 𝑛) + 1)))))
130	102, 115, 124, 118, 129	offval2 7713	. . . . . . . 8 ⊢ (⊤ → ((ℕ × {1}) ∘_f + ((ℕ × { -2}) ∘_f · 𝐺)) = (𝑛 ∈ ℕ ↦ (1 + ( -2 · (1 / ((2 · 𝑛) + 1))))))
131	102, 103, 104, 123, 130	offval2 7713	. . . . . . 7 ⊢ (⊤ → (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × { -2}) ∘_f · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + ( -2 · (1 / ((2 · 𝑛) + 1)))))))
132	131	mptru 1576	. . . . . 6 ⊢ (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × { -2}) ∘_f · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + ( -2 · (1 / ((2 · 𝑛) + 1))))))
133	100, 132	eqtri 2783	. . . . 5 ⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + ( -2 · (1 / ((2 · 𝑛) + 1))))))
134		ovex 7453	. . . . 5 ⊢ ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + ( -2 · (1 / 𝑁)))) ∈ V
135	99, 133, 134	fvmpt 6993	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + ( -2 · (1 / 𝑁)))))
136	110	recni 11326	. . . . . . . 8 ⊢ ((π↑2) / 6) ∈ ℂ
137	136	a1i 11	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((π↑2) / 6) ∈ ℂ)
138	6	nncnd 12354	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℂ)
139	138, 62, 64	divcld 12096	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) / 𝑁) ∈ ℂ)
140		ax-1cn 11261	. . . . . . . . 9 ⊢ 1 ∈ ℂ
141		subcl 11559	. . . . . . . . 9 ⊢ (((2 · 𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → ((2 · 𝑀) − 1) ∈ ℂ)
142	138, 140, 141	sylancl 598	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ∈ ℂ)
143	142, 62, 64	divcld 12096	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) / 𝑁) ∈ ℂ)
144	137, 139, 143	mulassd 11335	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · (((2 · 𝑀) − 1) / 𝑁)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))))
145		1cnd 11305	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 1 ∈ ℂ)
146	62, 145, 62, 64	divsubdird 12135	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((𝑁 / 𝑁) − (1 / 𝑁)))
147	3	oveq1i 7430	. . . . . . . . . . 11 ⊢ (𝑁 − 1) = (((2 · 𝑀) + 1) − 1)
148		pncan 11566	. . . . . . . . . . . 12 ⊢ (((2 · 𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑀) + 1) − 1) = (2 · 𝑀))
149	138, 140, 148	sylancl 598	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) − 1) = (2 · 𝑀))
150	147, 149	eqtrid 2807	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 − 1) = (2 · 𝑀))
151	150	oveq1d 7435	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((2 · 𝑀) / 𝑁))
152	62, 64	dividd 12094	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 / 𝑁) = 1)
153	152	oveq1d 7435	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) − (1 / 𝑁)) = (1 − (1 / 𝑁)))
154	146, 151, 153	3eqtr3rd 2804	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (1 − (1 / 𝑁)) = ((2 · 𝑀) / 𝑁))
155	154	oveq2d 7436	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (1 − (1 / 𝑁))) = (((π↑2) / 6) · ((2 · 𝑀) / 𝑁)))
156	125	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → -2 ∈ ℂ)
157	62, 156, 62, 64	divdird 12134	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = ((𝑁 / 𝑁) + ( -2 / 𝑁)))
158		negsub 11609	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑁 + -2) = (𝑁 − 2))
159	62, 48, 158	sylancl 598	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = (𝑁 − 2))
160		df-2 12408	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
161	3, 160	oveq12i 7432	. . . . . . . . . . 11 ⊢ (𝑁 − 2) = (((2 · 𝑀) + 1) − (1 + 1))
162	138, 145, 145	pnpcan2d 11710	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) − (1 + 1)) = ((2 · 𝑀) − 1))
163	161, 162	eqtrid 2807	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 − 2) = ((2 · 𝑀) − 1))
164	159, 163	eqtrd 2795	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = ((2 · 𝑀) − 1))
165	164	oveq1d 7435	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = (((2 · 𝑀) − 1) / 𝑁))
166	156, 62, 64	divrecd 12099	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ( -2 / 𝑁) = ( -2 · (1 / 𝑁)))
167	152, 166	oveq12d 7438	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + ( -2 / 𝑁)) = (1 + ( -2 · (1 / 𝑁))))
168	157, 165, 167	3eqtr3rd 2804	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (1 + ( -2 · (1 / 𝑁))) = (((2 · 𝑀) − 1) / 𝑁))
169	155, 168	oveq12d 7438	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + ( -2 · (1 / 𝑁)))) = ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · (((2 · 𝑀) − 1) / 𝑁)))
170	8	nnsqcld 14391	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈ ℕ)
171	170	nncnd 12354	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈ ℂ)
172		6cn 12437	. . . . . . . . . . 11 ⊢ 6 ∈ ℂ
173	172	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 6 ∈ ℂ)
174	171, 173	mulcomd 11333	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁↑2) · 6) = (6 · (𝑁↑2)))
175	174	oveq2d 7436	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
176	106	recni 11326	. . . . . . . . . 10 ⊢ (π↑2) ∈ ℂ
177	176	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (π↑2) ∈ ℂ)
178	138, 142	mulcld 11332	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ)
179	170	nnne0d 12391	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ≠ 0)
180	171, 179	jca 521	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))
181	172, 109	pm3.2i 476	. . . . . . . . . 10 ⊢ (6 ∈ ℂ ∧ 6 ≠ 0)
182	181	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (6 ∈ ℂ ∧ 6 ≠ 0))
183		divmuldiv 12020	. . . . . . . . 9 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ) ∧ (((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0) ∧ (6 ∈ ℂ ∧ 6 ≠ 0))) → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)))
184	177, 178, 180, 182, 183	syl22anc 852	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)))
185		divmuldiv 12020	. . . . . . . . 9 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ) ∧ ((6 ∈ ℂ ∧ 6 ≠ 0) ∧ ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))) → (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
186	177, 178, 182, 180, 185	syl22anc 852	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
187	175, 184, 186	3eqtr4d 2805	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))))
188	60	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → π ∈ ℂ)
189	188, 62, 64	sqdivd 14305	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) = ((π↑2) / (𝑁↑2)))
190	189	oveq1d 7435	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
191	138, 62, 142, 62, 64, 64	divmuldivd 12137	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁 · 𝑁)))
192	62	sqvald 14289	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) = (𝑁 · 𝑁))
193	192	oveq2d 7436	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁 · 𝑁)))
194	191, 193	eqtr4d 2798	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2)))
195	194	oveq2d 7436	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))) = (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))))
196	187, 190, 195	3eqtr4d 2805	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))))
197	144, 169, 196	3eqtr4d 2805	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + ( -2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
198		eqid 2760	. . . . . . 7 ⊢ (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (𝑥↑𝑗))) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · ( -1↑(𝑀 − 𝑗))) · (𝑥↑𝑗)))
199		eqid 2760	. . . . . . 7 ⊢ (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑ -2)) = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑ -2))
200	3, 198, 199	basellem5 27417	. . . . . 6 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑ -2) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6))
201	200	oveq2d 7436	. . . . 5 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑ -2)) = (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
202	197, 201	eqtr4d 2798	. . . 4 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + ( -2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑ -2)))
203	22	recnd 11340	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑ -2) ∈ ℂ)
204	1, 35, 203	fsummulc2 15955	. . . 4 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑ -2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑ -2)))
205	135, 202, 204	3eqtrd 2799	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑ -2)))
206		basel.f	. . . . 5 ⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑ -2)))
207	206	fveq1i 6886	. . . 4 ⊢ (𝐹‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑ -2)))‘𝑀)
208		oveq1 7427	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛↑ -2) = (𝑘↑ -2))
209		eqid 2760	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ (𝑛↑ -2)) = (𝑛 ∈ ℕ ↦ (𝑛↑ -2))
210		ovex 7453	. . . . . . 7 ⊢ (𝑘↑ -2) ∈ V
211	208, 209, 210	fvmpt 6993	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑛↑ -2))‘𝑘) = (𝑘↑ -2))
212	25, 211	syl 18	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ (𝑛↑ -2))‘𝑘) = (𝑘↑ -2))
213		id 23	. . . . . 6 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ)
214		nnuz 13007	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
215	213, 214	eleqtrdi 2870	. . . . 5 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (ℤ_≥‘1))
216	212, 215, 57	fsumser 15901	. . . 4 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(𝑘↑ -2) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑ -2)))‘𝑀))
217	207, 216	eqtr4id 2814	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) = Σ𝑘 ∈ (1...𝑀)(𝑘↑ -2))
218	90, 205, 217	3brtr4d 5136	. 2 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) ≤ (𝐹‘𝑀))
219	73	resincld 16316	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ)
220		sincosq1sgn 26832	. . . . . . . . 9 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (0 < (sin‘((𝑘 · π) / 𝑁)) ∧ 0 < (cos‘((𝑘 · π) / 𝑁))))
221	13, 220	syl 18	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) ∧ 0 < (cos‘((𝑘 · π) / 𝑁))))
222	221	simpld 500	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (sin‘((𝑘 · π) / 𝑁)))
223	222	gt0ne0d 11883	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≠ 0)
224	219, 223, 21	reexpclzd 14396	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑ -2) ∈ ℝ)
225	12, 224	remulcld 11342	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑ -2)) ∈ ℝ)
226		sinltx 16362	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ ℝ⁺ → (sin‘((𝑘 · π) / 𝑁)) < ((𝑘 · π) / 𝑁))
227	81, 226	syl 18	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) < ((𝑘 · π) / 𝑁))
228	219, 73, 227	ltled 11461	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁))
229		0re 11313	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
230		ltle 11401	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ) → (0 < (sin‘((𝑘 · π) / 𝑁)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁))))
231	229, 219, 230	sylancr 599	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁))))
232	222, 231	mpd 16	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁)))
233	219, 73, 232, 82	le2sqd 14404	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁) ↔ ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2)))
234	228, 233	mpbid 235	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2))
235	234, 71	breqtrrd 5132	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑ -2)))
236	219	resqcld 14271	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ)
237	236, 12, 45	lemuldiv2d 13217	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑ -2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔ ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑ -2))))
238	219, 222	elrpd 13164	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
239		rpexpcl 14226	. . . . . . . . 9 ⊢ (((sin‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
240	238, 18, 239	sylancl 598	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
241	28, 12, 240	lemuldivd 13216	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑ -2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔ (𝑘↑ -2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
242	237, 241	bitr3d 284	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑ -2)) ↔ (𝑘↑ -2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
243	235, 242	mpbid 235	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑ -2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
244	219	recnd 11340	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℂ)
245		expneg 14215	. . . . . . . 8 ⊢ (((sin‘((𝑘 · π) / 𝑁)) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((sin‘((𝑘 · π) / 𝑁))↑ -2) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
246	244, 30, 245	sylancl 598	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑ -2) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
247	246	oveq2d 7436	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑ -2)) = (((π / 𝑁)↑2) · (1 / ((sin‘((𝑘 · π) / 𝑁))↑2))))
248	236	recnd 11340	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
249	240	rpne0d 13172	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
250	36, 248, 249	divrecd 12099	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((sin‘((𝑘 · π) / 𝑁))↑2))))
251	247, 250	eqtr4d 2798	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑ -2)) = (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
252	243, 251	breqtrrd 5132	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑ -2) ≤ (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑ -2)))
253	1, 28, 225, 252	fsumle 15971	. . 3 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(𝑘↑ -2) ≤ Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑ -2)))
254	94	oveq2d 7436	. . . . . 6 ⊢ (𝑛 = 𝑀 → (1 + (1 / ((2 · 𝑛) + 1))) = (1 + (1 / 𝑁)))
255	96, 254	oveq12d 7438	. . . . 5 ⊢ (𝑛 = 𝑀 → ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))))
256		basel.k	. . . . . 6 ⊢ 𝐾 = (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺))
257		ovexd 7455	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 + (1 / ((2 · 𝑛) + 1))) ∈ V)
258	102, 115, 116, 118, 120	offval2 7713	. . . . . . . 8 ⊢ (⊤ → ((ℕ × {1}) ∘_f + 𝐺) = (𝑛 ∈ ℕ ↦ (1 + (1 / ((2 · 𝑛) + 1)))))
259	102, 103, 257, 123, 258	offval2 7713	. . . . . . 7 ⊢ (⊤ → (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1))))))
260	259	mptru 1576	. . . . . 6 ⊢ (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))))
261	256, 260	eqtri 2783	. . . . 5 ⊢ 𝐾 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))))
262		ovex 7453	. . . . 5 ⊢ ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) ∈ V
263	255, 261, 262	fvmpt 6993	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))))
264		peano2cn 11485	. . . . . . . 8 ⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈ ℂ)
265	62, 264	syl 18	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
266	265, 62, 64	divcld 12096	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
267	137, 139, 266	mulassd 11335	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))))
268	62, 145, 62, 64	divdird 12134	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) = ((𝑁 / 𝑁) + (1 / 𝑁)))
269	152	oveq1d 7435	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (1 / 𝑁)) = (1 + (1 / 𝑁)))
270	268, 269	eqtr2d 2796	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (1 + (1 / 𝑁)) = ((𝑁 + 1) / 𝑁))
271	155, 270	oveq12d 7438	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁)))
272	174	oveq2d 7436	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
273	138, 265	mulcld 11332	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ)
274		divmuldiv 12020	. . . . . . . 8 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ) ∧ (((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0) ∧ (6 ∈ ℂ ∧ 6 ≠ 0))) → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)))
275	177, 273, 180, 182, 274	syl22anc 852	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)))
276		divmuldiv 12020	. . . . . . . 8 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ) ∧ ((6 ∈ ℂ ∧ 6 ≠ 0) ∧ ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))) → (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
277	177, 273, 182, 180, 276	syl22anc 852	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
278	272, 275, 277	3eqtr4d 2805	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))))
279	73	recoscld 16317	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℝ)
280	279	recnd 11340	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℂ)
281	280	sqcld 14290	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
282	248, 281, 248, 249	divdird 12134	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = ((((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) + (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
283	73	recnd 11340	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℂ)
284		sincossq 16349	. . . . . . . . . . . . . 14 ⊢ (((𝑘 · π) / 𝑁) ∈ ℂ → (((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) = 1)
285	283, 284	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) = 1)
286	285	oveq1d 7435	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
287	248, 249	dividd 12094	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = 1)
288	221	simprd 501	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (cos‘((𝑘 · π) / 𝑁)))
289	288	gt0ne0d 11883	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ≠ 0)
290		tanval 16301	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑘 · π) / 𝑁) ∈ ℂ ∧ (cos‘((𝑘 · π) / 𝑁)) ≠ 0) → (tan‘((𝑘 · π) / 𝑁)) = ((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁))))
291	283, 289, 290	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) = ((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁))))
292	291	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2))
293	244, 280, 289	sqdivd 14305	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2)))
294	292, 293	eqtrd 2795	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2)))
295	294	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (1 / (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))))
296		sqne0 14269	. . . . . . . . . . . . . . . . 17 ⊢ ((cos‘((𝑘 · π) / 𝑁)) ∈ ℂ → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0))
297	280, 296	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0))
298	289, 297	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
299	248, 281, 249, 298	recdivd 12113	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))) = (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
300	32, 295, 299	3eqtrrd 2800	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = ((tan‘((𝑘 · π) / 𝑁))↑ -2))
301	287, 300	oveq12d 7438	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) + (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))) = (1 + ((tan‘((𝑘 · π) / 𝑁))↑ -2)))
302	282, 286, 301	3eqtr3d 2803	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (1 + ((tan‘((𝑘 · π) / 𝑁))↑ -2)))
303		addcom 11499	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ ((tan‘((𝑘 · π) / 𝑁))↑ -2) ∈ ℂ) → (1 + ((tan‘((𝑘 · π) / 𝑁))↑ -2)) = (((tan‘((𝑘 · π) / 𝑁))↑ -2) + 1))
304	140, 203, 303	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 + ((tan‘((𝑘 · π) / 𝑁))↑ -2)) = (((tan‘((𝑘 · π) / 𝑁))↑ -2) + 1))
305	246, 302, 304	3eqtrd 2799	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑ -2) = (((tan‘((𝑘 · π) / 𝑁))↑ -2) + 1))
306	305	sumeq2dv 15874	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑ -2) = Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑ -2) + 1))
307		1cnd 11305	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 1 ∈ ℂ)
308	1, 203, 307	fsumadd 15911	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑ -2) + 1) = (Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑ -2) + Σ𝑘 ∈ (1...𝑀)1))
309		fsumconst 15961	. . . . . . . . . . . 12 ⊢ (((1...𝑀) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑘 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1))
310	1, 140, 309	sylancl 598	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1))
311		nnnn0 12616	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
312		hashfz1 14493	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
313	311, 312	syl 18	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (♯‘(1...𝑀)) = 𝑀)
314	313	oveq1d 7435	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((♯‘(1...𝑀)) · 1) = (𝑀 · 1))
315		nncn 12346	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
316	315	mulridd 11329	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑀 · 1) = 𝑀)
317	310, 314, 316	3eqtrd 2799	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)1 = 𝑀)
318	200, 317	oveq12d 7438	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑ -2) + Σ𝑘 ∈ (1...𝑀)1) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
319	306, 308, 318	3eqtrd 2799	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑ -2) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
320		3cn 12427	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℂ
321	320	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 3 ∈ ℂ)
322	138, 142, 321	adddid 11336	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (((2 · 𝑀) − 1) + 3)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + ((2 · 𝑀) · 3)))
323		3m1e2 12473	. . . . . . . . . . . . . . . 16 ⊢ (3 − 1) = 2
324	323, 160	eqtri 2783	. . . . . . . . . . . . . . 15 ⊢ (3 − 1) = (1 + 1)
325	324	oveq2i 7431	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑀) + (3 − 1)) = ((2 · 𝑀) + (1 + 1))
326	138, 145, 321	subadd23d 11694	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = ((2 · 𝑀) + (3 − 1)))
327	138, 145, 145	addassd 11334	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
328	325, 326, 327	3eqtr4a 2821	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = (((2 · 𝑀) + 1) + 1))
329	3	oveq1i 7430	. . . . . . . . . . . . 13 ⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
330	328, 329	eqtr4di 2813	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = (𝑁 + 1))
331	330	oveq2d 7436	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (((2 · 𝑀) − 1) + 3)) = ((2 · 𝑀) · (𝑁 + 1)))
332		2cnd 12424	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → 2 ∈ ℂ)
333	332, 315, 321	mul32d 11523	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · 3) = ((2 · 3) · 𝑀))
334		2t3e6 12512	. . . . . . . . . . . . . 14 ⊢ (2 · 3) = 6
335	334	oveq1i 7430	. . . . . . . . . . . . 13 ⊢ ((2 · 3) · 𝑀) = (6 · 𝑀)
336	333, 335	eqtrdi 2811	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · 3) = (6 · 𝑀))
337	336	oveq2d 7436	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · ((2 · 𝑀) − 1)) + ((2 · 𝑀) · 3)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)))
338	322, 331, 337	3eqtr3d 2803	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (𝑁 + 1)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)))
339	338	oveq1d 7435	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)) / 6))
340		mulcl 11287	. . . . . . . . . . 11 ⊢ ((6 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (6 · 𝑀) ∈ ℂ)
341	172, 315, 340	sylancr 599	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (6 · 𝑀) ∈ ℂ)
342	109	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 6 ≠ 0)
343	178, 341, 173, 342	divdird 12134	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + ((6 · 𝑀) / 6)))
344	315, 173, 342	divcan3d 12101	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → ((6 · 𝑀) / 6) = 𝑀)
345	344	oveq2d 7436	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + ((6 · 𝑀) / 6)) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
346	339, 343, 345	3eqtrd 2799	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
347	319, 346	eqtr4d 2798	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑ -2) = (((2 · 𝑀) · (𝑁 + 1)) / 6))
348	189, 347	oveq12d 7438	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑ -2)) = (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)))
349	138, 62, 265, 62, 64, 64	divmuldivd 12137	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁)))
350	192	oveq2d 7436	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁)))
351	349, 350	eqtr4d 2798	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2)))
352	351	oveq2d 7436	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))) = (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))))
353	278, 348, 352	3eqtr4d 2805	. . . . 5 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑ -2)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))))
354	267, 271, 353	3eqtr4d 2805	. . . 4 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑ -2)))
355	224	recnd 11340	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑ -2) ∈ ℂ)
356	1, 35, 355	fsummulc2 15955	. . . 4 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑ -2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑ -2)))
357	263, 354, 356	3eqtrd 2799	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑ -2)))
358	253, 217, 357	3brtr4d 5136	. 2 ⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) ≤ (𝐾‘𝑀))
359	218, 358	jca 521	1 ⊢ (𝑀 ∈ ℕ → ((𝐽‘𝑀) ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ (𝐾‘𝑀)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ⊤wtru 1570 ∈ wcel 2144 ≠ wne 2955 Vcvv 3450 {csn 4584 class class class wbr 5102 ↦ cmpt 5185 × cxp 5648 ‘cfv 6538 (class class class)co 7420 ∘_f cof 7691 Fincfn 8976 ℂcc 11201 ℝcr 11202 0cc0 11203 1c1 11204 + caddc 11206 · cmul 11208 < clt 11346 ≤ cle 11347 − cmin 11544 -cneg 11545 / cdiv 11976 ℕcn 12338 2c2 12400 3c3 12401 6c6 12404 ℕ₀cn0 12609 ℤcz 12696 ℤ_≥cuz 12968 ℝ⁺crp 13123 (,)cioo 13479 ...cfz 13642 seqcseq 14147 ↑cexp 14207 Ccbc 14449 ♯chash 14477 Σcsu 15858 sincsin 16234 cosccos 16235 tanctan 16236 πcpi 16237

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9645 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-pre-sup 11281 ax-addf 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8180 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-2o 8480 df-oadd 8483 df-er 8720 df-map 8852 df-pm 8853 df-ixp 8929 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-fsupp 9357 df-fi 9406 df-sup 9437 df-inf 9438 df-oi 9507 df-dju 9985 df-card 10023 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-div 11977 df-nn 12339 df-2 12408 df-3 12409 df-4 12410 df-5 12411 df-6 12412 df-7 12413 df-8 12414 df-9 12415 df-n0 12610 df-xnn0 12683 df-z 12697 df-dec 12818 df-uz 12969 df-q 13079 df-rp 13124 df-xneg 13244 df-xadd 13245 df-xmul 13246 df-ioo 13483 df-ioc 13484 df-ico 13485 df-icc 13486 df-fz 13643 df-fzo 13792 df-fl 13935 df-mod 14013 df-seq 14148 df-exp 14208 df-fac 14421 df-bc 14450 df-hash 14478 df-shft 15225 df-cj 15271 df-re 15272 df-im 15273 df-sqrt 15407 df-abs 15408 df-limsup 15643 df-clim 15660 df-rlim 15661 df-sum 15859 df-ef 16238 df-sin 16240 df-cos 16241 df-tan 16242 df-pi 16243 df-struct 17330 df-sets 17347 df-slot 17365 df-ndx 17377 df-base 17393 df-ress 17414 df-plusg 17446 df-mulr 17447 df-starv 17448 df-sca 17449 df-vsca 17450 df-ip 17451 df-tset 17452 df-ple 17453 df-ds 17455 df-unif 17456 df-hom 17457 df-cco 17458 df-rest 17598 df-topn 17599 df-0g 17617 df-gsum 17618 df-topgen 17619 df-pt 17620 df-prds 17623 df-xrs 17679 df-qtop 17684 df-imas 17685 df-xps 17687 df-mre 17761 df-mrc 17762 df-acs 17764 df-mgm 18821 df-sgrp 18913 df-mnd 18929 df-submnd 18984 df-mulg 19283 df-cntz 19536 df-cmn 20001 df-psmet 21675 df-xmet 21676 df-met 21677 df-bl 21678 df-mopn 21679 df-fbas 21680 df-fg 21681 df-cnfld 21684 df-top 23217 df-topon 23234 df-topsp 23256 df-bases 23269 df-cld 23342 df-ntr 23343 df-cls 23344 df-nei 23421 df-lp 23459 df-perf 23460 df-cn 23550 df-cnp 23551 df-haus 23638 df-tx 23886 df-hmeo 24079 df-fil 24170 df-fm 24262 df-flim 24263 df-flf 24264 df-xms 24644 df-ms 24645 df-tms 24646 df-cncf 25204 df-0p 25996 df-limc 26191 df-dv 26192 df-ply 26511 df-idp 26512 df-coe 26513 df-dgr 26514 df-quot 26617

This theorem is used by: basellem9 27421

W3C validator