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 27023

Description: Lemma for basel 27025. 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 27020. (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 13877	. . . 4 ⊢ (𝑀 ∈ ℕ → (1...𝑀) ∈ Fin)
2		pire 26391	. . . . . . . 8 ⊢ π ∈ ℝ
3		basellem8.n	. . . . . . . . 9 ⊢ 𝑁 = ((2 · 𝑀) + 1)
4		2nn 12195	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
5		nnmulcl 12146	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
6	4, 5	mpan 690	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℕ)
7	6	peano2nnd 12139	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) + 1) ∈ ℕ)
8	3, 7	eqeltrid 2835	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → 𝑁 ∈ ℕ)
9		nndivre 12163	. . . . . . . 8 ⊢ ((π ∈ ℝ ∧ 𝑁 ∈ ℕ) → (π / 𝑁) ∈ ℝ)
10	2, 8, 9	sylancr 587	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (π / 𝑁) ∈ ℝ)
11	10	resqcld 14029	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) ∈ ℝ)
12	11	adantr 480	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℝ)
13	3	basellem1 27016	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)))
14		tanrpcl 26438	. . . . . . . 8 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
15	13, 14	syl 17	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
16	15	rpred 12931	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ)
17	15	rpne0d 12936	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ≠ 0)
18		2z 12501	. . . . . . . 8 ⊢ 2 ∈ ℤ
19		znegcl 12504	. . . . . . . 8 ⊢ (2 ∈ ℤ → -2 ∈ ℤ)
20	18, 19	ax-mp 5	. . . . . . 7 ⊢ -2 ∈ ℤ
21	20	a1i 11	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → -2 ∈ ℤ)
22	16, 17, 21	reexpclzd 14153	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℝ)
23	12, 22	remulcld 11139	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ∈ ℝ)
24		elfznn 13450	. . . . . . 7 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ)
25	24	adantl 481	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℕ)
26	25	nnred 12137	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ)
27	25	nnne0d 12172	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ≠ 0)
28	26, 27, 21	reexpclzd 14153	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℝ)
29	16	recnd 11137	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℂ)
30		2nn0 12395	. . . . . . . 8 ⊢ 2 ∈ ℕ₀
31		expneg 13973	. . . . . . . 8 ⊢ (((tan‘((𝑘 · π) / 𝑁)) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)))
32	29, 30, 31	sylancl 586	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)))
33	32	oveq2d 7362	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))))
34	10	recnd 11137	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (π / 𝑁) ∈ ℂ)
35	34	sqcld 14048	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) ∈ ℂ)
36	35	adantr 480	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℂ)
37		rpexpcl 13984	. . . . . . . . . 10 ⊢ (((tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
38	15, 18, 37	sylancl 586	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
39	38	rpred 12931	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ)
40	39	recnd 11137	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
41	38	rpne0d 12936	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
42	36, 40, 41	divrecd 11897	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))))
43	33, 42	eqtr4d 2769	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)))
44	25	nnrpd 12929	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ⁺)
45		rpexpcl 13984	. . . . . . 7 ⊢ ((𝑘 ∈ ℝ⁺ ∧ -2 ∈ ℤ) → (𝑘↑-2) ∈ ℝ⁺)
46	44, 20, 45	sylancl 586	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℝ⁺)
47	25	nncnd 12138	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℂ)
48	47, 27, 21	expnegd 14057	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑--2) = (1 / (𝑘↑-2)))
49		2cn 12197	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
50	49	negnegi 11428	. . . . . . . . . . 11 ⊢ --2 = 2
51	50	oveq2i 7357	. . . . . . . . . 10 ⊢ (𝑘↑--2) = (𝑘↑2)
52	48, 51	eqtr3di 2781	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (𝑘↑-2)) = (𝑘↑2))
53	52	oveq1d 7361	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((1 / (𝑘↑-2)) · ((π / 𝑁)↑2)) = ((𝑘↑2) · ((π / 𝑁)↑2)))
54		nncn 12130	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
55		nnne0 12156	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0)
56	20	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → -2 ∈ ℤ)
57	54, 55, 56	expclzd 14055	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝑘↑-2) ∈ ℂ)
58	25, 57	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℂ)
59	47, 27, 21	expne0d 14056	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≠ 0)
60	36, 58, 59	divrec2d 11898	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) = ((1 / (𝑘↑-2)) · ((π / 𝑁)↑2)))
61	2	recni 11123	. . . . . . . . . . . 12 ⊢ π ∈ ℂ
62	61	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → π ∈ ℂ)
63	8	nncnd 12138	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑁 ∈ ℂ)
64	8	nnne0d 12172	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑁 ≠ 0)
65	63, 64	jca 511	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
66	65	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
67		divass 11791	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℂ ∧ π ∈ ℂ ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → ((𝑘 · π) / 𝑁) = (𝑘 · (π / 𝑁)))
68	47, 62, 66, 67	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) = (𝑘 · (π / 𝑁)))
69	68	oveq1d 7361	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘 · (π / 𝑁))↑2))
70	34	adantr 480	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (π / 𝑁) ∈ ℂ)
71	47, 70	sqmuld 14062	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · (π / 𝑁))↑2) = ((𝑘↑2) · ((π / 𝑁)↑2)))
72	69, 71	eqtrd 2766	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘↑2) · ((π / 𝑁)↑2)))
73	53, 60, 72	3eqtr4d 2776	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) = (((𝑘 · π) / 𝑁)↑2))
74		elioore 13272	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → ((𝑘 · π) / 𝑁) ∈ ℝ)
75	13, 74	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℝ)
76	75	resqcld 14029	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ∈ ℝ)
77		tangtx 26439	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → ((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)))
78	13, 77	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)))
79		eliooord 13302	. . . . . . . . . . . . . 14 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (0 < ((𝑘 · π) / 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π / 2)))
80	13, 79	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < ((𝑘 · π) / 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π / 2)))
81	80	simpld 494	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < ((𝑘 · π) / 𝑁))
82	75, 81	elrpd 12928	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℝ⁺)
83	82	rpge0d 12935	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ ((𝑘 · π) / 𝑁))
84	15	rpge0d 12935	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (tan‘((𝑘 · π) / 𝑁)))
85	75, 16, 83, 84	lt2sqd 14160	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)) ↔ (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2)))
86	78, 85	mpbid 232	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2))
87	76, 39, 86	ltled 11258	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2))
88	73, 87	eqbrtrd 5113	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2))
89	12, 46, 38, 88	lediv23d 12999	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) ≤ (𝑘↑-2))
90	43, 89	eqbrtrd 5113	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ≤ (𝑘↑-2))
91	1, 23, 28, 90	fsumle 15703	. . 3 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ≤ Σ𝑘 ∈ (1...𝑀)(𝑘↑-2))
92		oveq2 7354	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑀 → (2 · 𝑛) = (2 · 𝑀))
93	92	oveq1d 7361	. . . . . . . . . 10 ⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = ((2 · 𝑀) + 1))
94	93, 3	eqtr4di 2784	. . . . . . . . 9 ⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = 𝑁)
95	94	oveq2d 7362	. . . . . . . 8 ⊢ (𝑛 = 𝑀 → (1 / ((2 · 𝑛) + 1)) = (1 / 𝑁))
96	95	oveq2d 7362	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / 𝑁)))
97	96	oveq2d 7362	. . . . . 6 ⊢ (𝑛 = 𝑀 → (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) = (((π↑2) / 6) · (1 − (1 / 𝑁))))
98	95	oveq2d 7362	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (-2 · (1 / ((2 · 𝑛) + 1))) = (-2 · (1 / 𝑁)))
99	98	oveq2d 7362	. . . . . 6 ⊢ (𝑛 = 𝑀 → (1 + (-2 · (1 / ((2 · 𝑛) + 1)))) = (1 + (-2 · (1 / 𝑁))))
100	97, 99	oveq12d 7364	. . . . 5 ⊢ (𝑛 = 𝑀 → ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1))))) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))))
101		basel.j	. . . . . 6 ⊢ 𝐽 = (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺)))
102		nnex 12128	. . . . . . . . 9 ⊢ ℕ ∈ V
103	102	a1i 11	. . . . . . . 8 ⊢ (⊤ → ℕ ∈ V)
104		ovexd 7381	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V)
105		ovexd 7381	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 + (-2 · (1 / ((2 · 𝑛) + 1)))) ∈ V)
106		basel.h	. . . . . . . . 9 ⊢ 𝐻 = ((ℕ × {((π↑2) / 6)}) ∘_f · ((ℕ × {1}) ∘_f − 𝐺))
107	2	resqcli 14090	. . . . . . . . . . . 12 ⊢ (π↑2) ∈ ℝ
108		6re 12212	. . . . . . . . . . . 12 ⊢ 6 ∈ ℝ
109		6nn 12211	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ
110	109	nnne0i 12162	. . . . . . . . . . . 12 ⊢ 6 ≠ 0
111	107, 108, 110	redivcli 11885	. . . . . . . . . . 11 ⊢ ((π↑2) / 6) ∈ ℝ
112	111	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ((π↑2) / 6) ∈ ℝ)
113		ovexd 7381	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / ((2 · 𝑛) + 1))) ∈ V)
114		fconstmpt 5678	. . . . . . . . . . 11 ⊢ (ℕ × {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) / 6))
115	114	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℕ × {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) / 6)))
116		1zzd 12500	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℤ)
117		ovexd 7381	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / ((2 · 𝑛) + 1)) ∈ V)
118		fconstmpt 5678	. . . . . . . . . . . 12 ⊢ (ℕ × {1}) = (𝑛 ∈ ℕ ↦ 1)
119	118	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (ℕ × {1}) = (𝑛 ∈ ℕ ↦ 1))
120		basel.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
121	120	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))))
122	103, 116, 117, 119, 121	offval2 7630	. . . . . . . . . 10 ⊢ (⊤ → ((ℕ × {1}) ∘_f − 𝐺) = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
123	103, 112, 113, 115, 122	offval2 7630	. . . . . . . . 9 ⊢ (⊤ → ((ℕ × {((π↑2) / 6)}) ∘_f · ((ℕ × {1}) ∘_f − 𝐺)) = (𝑛 ∈ ℕ ↦ (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1))))))
124	106, 123	eqtrid 2778	. . . . . . . 8 ⊢ (⊤ → 𝐻 = (𝑛 ∈ ℕ ↦ (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1))))))
125		ovexd 7381	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (-2 · (1 / ((2 · 𝑛) + 1))) ∈ V)
126	49	negcli 11426	. . . . . . . . . . 11 ⊢ -2 ∈ ℂ
127	126	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → -2 ∈ ℂ)
128		fconstmpt 5678	. . . . . . . . . . 11 ⊢ (ℕ × {-2}) = (𝑛 ∈ ℕ ↦ -2)
129	128	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℕ × {-2}) = (𝑛 ∈ ℕ ↦ -2))
130	103, 127, 117, 129, 121	offval2 7630	. . . . . . . . 9 ⊢ (⊤ → ((ℕ × {-2}) ∘_f · 𝐺) = (𝑛 ∈ ℕ ↦ (-2 · (1 / ((2 · 𝑛) + 1)))))
131	103, 116, 125, 119, 130	offval2 7630	. . . . . . . 8 ⊢ (⊤ → ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺)) = (𝑛 ∈ ℕ ↦ (1 + (-2 · (1 / ((2 · 𝑛) + 1))))))
132	103, 104, 105, 124, 131	offval2 7630	. . . . . . 7 ⊢ (⊤ → (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1)))))))
133	132	mptru 1548	. . . . . 6 ⊢ (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1))))))
134	101, 133	eqtri 2754	. . . . 5 ⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1))))))
135		ovex 7379	. . . . 5 ⊢ ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) ∈ V
136	100, 134, 135	fvmpt 6929	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))))
137	111	recni 11123	. . . . . . . 8 ⊢ ((π↑2) / 6) ∈ ℂ
138	137	a1i 11	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((π↑2) / 6) ∈ ℂ)
139	6	nncnd 12138	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℂ)
140	139, 63, 64	divcld 11894	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) / 𝑁) ∈ ℂ)
141		ax-1cn 11061	. . . . . . . . 9 ⊢ 1 ∈ ℂ
142		subcl 11356	. . . . . . . . 9 ⊢ (((2 · 𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → ((2 · 𝑀) − 1) ∈ ℂ)
143	139, 141, 142	sylancl 586	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ∈ ℂ)
144	143, 63, 64	divcld 11894	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) / 𝑁) ∈ ℂ)
145	138, 140, 144	mulassd 11132	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · (((2 · 𝑀) − 1) / 𝑁)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))))
146		1cnd 11104	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 1 ∈ ℂ)
147	63, 146, 63, 64	divsubdird 11933	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((𝑁 / 𝑁) − (1 / 𝑁)))
148	3	oveq1i 7356	. . . . . . . . . . 11 ⊢ (𝑁 − 1) = (((2 · 𝑀) + 1) − 1)
149		pncan 11363	. . . . . . . . . . . 12 ⊢ (((2 · 𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑀) + 1) − 1) = (2 · 𝑀))
150	139, 141, 149	sylancl 586	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) − 1) = (2 · 𝑀))
151	148, 150	eqtrid 2778	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 − 1) = (2 · 𝑀))
152	151	oveq1d 7361	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((2 · 𝑀) / 𝑁))
153	63, 64	dividd 11892	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 / 𝑁) = 1)
154	153	oveq1d 7361	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) − (1 / 𝑁)) = (1 − (1 / 𝑁)))
155	147, 152, 154	3eqtr3rd 2775	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (1 − (1 / 𝑁)) = ((2 · 𝑀) / 𝑁))
156	155	oveq2d 7362	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (1 − (1 / 𝑁))) = (((π↑2) / 6) · ((2 · 𝑀) / 𝑁)))
157	126	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → -2 ∈ ℂ)
158	63, 157, 63, 64	divdird 11932	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = ((𝑁 / 𝑁) + (-2 / 𝑁)))
159		negsub 11406	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑁 + -2) = (𝑁 − 2))
160	63, 49, 159	sylancl 586	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = (𝑁 − 2))
161		df-2 12185	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
162	3, 161	oveq12i 7358	. . . . . . . . . . 11 ⊢ (𝑁 − 2) = (((2 · 𝑀) + 1) − (1 + 1))
163	139, 146, 146	pnpcan2d 11507	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) − (1 + 1)) = ((2 · 𝑀) − 1))
164	162, 163	eqtrid 2778	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 − 2) = ((2 · 𝑀) − 1))
165	160, 164	eqtrd 2766	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = ((2 · 𝑀) − 1))
166	165	oveq1d 7361	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = (((2 · 𝑀) − 1) / 𝑁))
167	157, 63, 64	divrecd 11897	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (-2 / 𝑁) = (-2 · (1 / 𝑁)))
168	153, 167	oveq12d 7364	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (-2 / 𝑁)) = (1 + (-2 · (1 / 𝑁))))
169	158, 166, 168	3eqtr3rd 2775	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (1 + (-2 · (1 / 𝑁))) = (((2 · 𝑀) − 1) / 𝑁))
170	156, 169	oveq12d 7364	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · (((2 · 𝑀) − 1) / 𝑁)))
171	8	nnsqcld 14148	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈ ℕ)
172	171	nncnd 12138	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈ ℂ)
173		6cn 12213	. . . . . . . . . 10 ⊢ 6 ∈ ℂ
174		mulcom 11089	. . . . . . . . . 10 ⊢ (((𝑁↑2) ∈ ℂ ∧ 6 ∈ ℂ) → ((𝑁↑2) · 6) = (6 · (𝑁↑2)))
175	172, 173, 174	sylancl 586	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁↑2) · 6) = (6 · (𝑁↑2)))
176	175	oveq2d 7362	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
177	107	recni 11123	. . . . . . . . . 10 ⊢ (π↑2) ∈ ℂ
178	177	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (π↑2) ∈ ℂ)
179	139, 143	mulcld 11129	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ)
180	171	nnne0d 12172	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ≠ 0)
181	172, 180	jca 511	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))
182	173, 110	pm3.2i 470	. . . . . . . . . 10 ⊢ (6 ∈ ℂ ∧ 6 ≠ 0)
183	182	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (6 ∈ ℂ ∧ 6 ≠ 0))
184		divmuldiv 11818	. . . . . . . . 9 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ) ∧ (((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0) ∧ (6 ∈ ℂ ∧ 6 ≠ 0))) → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)))
185	178, 179, 181, 183, 184	syl22anc 838	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)))
186		divmuldiv 11818	. . . . . . . . 9 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ) ∧ ((6 ∈ ℂ ∧ 6 ≠ 0) ∧ ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))) → (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
187	178, 179, 183, 181, 186	syl22anc 838	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
188	176, 185, 187	3eqtr4d 2776	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))))
189	61	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → π ∈ ℂ)
190	189, 63, 64	sqdivd 14063	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) = ((π↑2) / (𝑁↑2)))
191	190	oveq1d 7361	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
192	139, 63, 143, 63, 64, 64	divmuldivd 11935	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁 · 𝑁)))
193	63	sqvald 14047	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) = (𝑁 · 𝑁))
194	193	oveq2d 7362	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁 · 𝑁)))
195	192, 194	eqtr4d 2769	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2)))
196	195	oveq2d 7362	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))) = (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))))
197	188, 191, 196	3eqtr4d 2776	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))))
198	145, 170, 197	3eqtr4d 2776	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
199		eqid 2731	. . . . . . 7 ⊢ (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑥↑𝑗))) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑥↑𝑗)))
200		eqid 2731	. . . . . . 7 ⊢ (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2))
201	3, 199, 200	basellem5 27020	. . . . . 6 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6))
202	201	oveq2d 7362	. . . . 5 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
203	198, 202	eqtr4d 2769	. . . 4 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)))
204	22	recnd 11137	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ)
205	1, 35, 204	fsummulc2 15688	. . . 4 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)))
206	136, 203, 205	3eqtrd 2770	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)))
207		basel.f	. . . . 5 ⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))
208	207	fveq1i 6823	. . . 4 ⊢ (𝐹‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))‘𝑀)
209		oveq1 7353	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛↑-2) = (𝑘↑-2))
210		eqid 2731	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ (𝑛↑-2)) = (𝑛 ∈ ℕ ↦ (𝑛↑-2))
211		ovex 7379	. . . . . . 7 ⊢ (𝑘↑-2) ∈ V
212	209, 210, 211	fvmpt 6929	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2))
213	25, 212	syl 17	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2))
214		id 22	. . . . . 6 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ)
215		nnuz 12772	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
216	214, 215	eleqtrdi 2841	. . . . 5 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (ℤ_≥‘1))
217	213, 216, 58	fsumser 15634	. . . 4 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(𝑘↑-2) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))‘𝑀))
218	208, 217	eqtr4id 2785	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) = Σ𝑘 ∈ (1...𝑀)(𝑘↑-2))
219	91, 206, 218	3brtr4d 5123	. 2 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) ≤ (𝐹‘𝑀))
220	75	resincld 16049	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ)
221		sincosq1sgn 26432	. . . . . . . . 9 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (0 < (sin‘((𝑘 · π) / 𝑁)) ∧ 0 < (cos‘((𝑘 · π) / 𝑁))))
222	13, 221	syl 17	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) ∧ 0 < (cos‘((𝑘 · π) / 𝑁))))
223	222	simpld 494	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (sin‘((𝑘 · π) / 𝑁)))
224	223	gt0ne0d 11678	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≠ 0)
225	220, 224, 21	reexpclzd 14153	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) ∈ ℝ)
226	12, 225	remulcld 11139	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) ∈ ℝ)
227		sinltx 16095	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ ℝ⁺ → (sin‘((𝑘 · π) / 𝑁)) < ((𝑘 · π) / 𝑁))
228	82, 227	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) < ((𝑘 · π) / 𝑁))
229	220, 75, 228	ltled 11258	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁))
230		0re 11111	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
231		ltle 11198	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ) → (0 < (sin‘((𝑘 · π) / 𝑁)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁))))
232	230, 220, 231	sylancr 587	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁))))
233	223, 232	mpd 15	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁)))
234	220, 75, 233, 83	le2sqd 14161	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁) ↔ ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2)))
235	229, 234	mpbid 232	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2))
236	235, 73	breqtrrd 5119	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2)))
237	220	resqcld 14029	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ)
238	237, 12, 46	lemuldiv2d 12981	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑-2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔ ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2))))
239	220, 223	elrpd 12928	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
240		rpexpcl 13984	. . . . . . . . 9 ⊢ (((sin‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
241	239, 18, 240	sylancl 586	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
242	28, 12, 241	lemuldivd 12980	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑-2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔ (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
243	238, 242	bitr3d 281	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2)) ↔ (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
244	236, 243	mpbid 232	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
245	220	recnd 11137	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℂ)
246		expneg 13973	. . . . . . . 8 ⊢ (((sin‘((𝑘 · π) / 𝑁)) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
247	245, 30, 246	sylancl 586	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
248	247	oveq2d 7362	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (1 / ((sin‘((𝑘 · π) / 𝑁))↑2))))
249	237	recnd 11137	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
250	241	rpne0d 12936	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
251	36, 249, 250	divrecd 11897	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((sin‘((𝑘 · π) / 𝑁))↑2))))
252	248, 251	eqtr4d 2769	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
253	244, 252	breqtrrd 5119	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≤ (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
254	1, 28, 226, 253	fsumle 15703	. . 3 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(𝑘↑-2) ≤ Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
255	95	oveq2d 7362	. . . . . 6 ⊢ (𝑛 = 𝑀 → (1 + (1 / ((2 · 𝑛) + 1))) = (1 + (1 / 𝑁)))
256	97, 255	oveq12d 7364	. . . . 5 ⊢ (𝑛 = 𝑀 → ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))))
257		basel.k	. . . . . 6 ⊢ 𝐾 = (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺))
258		ovexd 7381	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 + (1 / ((2 · 𝑛) + 1))) ∈ V)
259	103, 116, 117, 119, 121	offval2 7630	. . . . . . . 8 ⊢ (⊤ → ((ℕ × {1}) ∘_f + 𝐺) = (𝑛 ∈ ℕ ↦ (1 + (1 / ((2 · 𝑛) + 1)))))
260	103, 104, 258, 124, 259	offval2 7630	. . . . . . 7 ⊢ (⊤ → (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1))))))
261	260	mptru 1548	. . . . . 6 ⊢ (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))))
262	257, 261	eqtri 2754	. . . . 5 ⊢ 𝐾 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))))
263		ovex 7379	. . . . 5 ⊢ ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) ∈ V
264	256, 262, 263	fvmpt 6929	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))))
265		peano2cn 11282	. . . . . . . 8 ⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈ ℂ)
266	63, 265	syl 17	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
267	266, 63, 64	divcld 11894	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
268	138, 140, 267	mulassd 11132	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))))
269	63, 146, 63, 64	divdird 11932	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) = ((𝑁 / 𝑁) + (1 / 𝑁)))
270	153	oveq1d 7361	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (1 / 𝑁)) = (1 + (1 / 𝑁)))
271	269, 270	eqtr2d 2767	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (1 + (1 / 𝑁)) = ((𝑁 + 1) / 𝑁))
272	156, 271	oveq12d 7364	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁)))
273	175	oveq2d 7362	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
274	139, 266	mulcld 11129	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ)
275		divmuldiv 11818	. . . . . . . 8 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ) ∧ (((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0) ∧ (6 ∈ ℂ ∧ 6 ≠ 0))) → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)))
276	178, 274, 181, 183, 275	syl22anc 838	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)))
277		divmuldiv 11818	. . . . . . . 8 ⊢ ((((π↑2) ∈ ℂ ∧ ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ) ∧ ((6 ∈ ℂ ∧ 6 ≠ 0) ∧ ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))) → (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
278	178, 274, 183, 181, 277	syl22anc 838	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
279	273, 276, 278	3eqtr4d 2776	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))))
280	75	recoscld 16050	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℝ)
281	280	recnd 11137	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℂ)
282	281	sqcld 14048	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
283	249, 282, 249, 250	divdird 11932	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = ((((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) + (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
284	75	recnd 11137	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℂ)
285		sincossq 16082	. . . . . . . . . . . . . 14 ⊢ (((𝑘 · π) / 𝑁) ∈ ℂ → (((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) = 1)
286	284, 285	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) = 1)
287	286	oveq1d 7361	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
288	249, 250	dividd 11892	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = 1)
289	222	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (cos‘((𝑘 · π) / 𝑁)))
290	289	gt0ne0d 11678	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ≠ 0)
291		tanval 16034	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑘 · π) / 𝑁) ∈ ℂ ∧ (cos‘((𝑘 · π) / 𝑁)) ≠ 0) → (tan‘((𝑘 · π) / 𝑁)) = ((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁))))
292	284, 290, 291	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) = ((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁))))
293	292	oveq1d 7361	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2))
294	245, 281, 290	sqdivd 14063	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2)))
295	293, 294	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2)))
296	295	oveq2d 7362	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (1 / (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))))
297		sqne0 14027	. . . . . . . . . . . . . . . . 17 ⊢ ((cos‘((𝑘 · π) / 𝑁)) ∈ ℂ → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0))
298	281, 297	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0))
299	290, 298	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
300	249, 282, 250, 299	recdivd 11911	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))) = (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
301	32, 296, 300	3eqtrrd 2771	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = ((tan‘((𝑘 · π) / 𝑁))↑-2))
302	288, 301	oveq12d 7364	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) + (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))) = (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)))
303	283, 287, 302	3eqtr3d 2774	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)))
304		addcom 11296	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ) → (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
305	141, 204, 304	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
306	247, 303, 305	3eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
307	306	sumeq2dv 15606	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
308		1cnd 11104	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 1 ∈ ℂ)
309	1, 204, 308	fsumadd 15644	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑-2) + 1) = (Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) + Σ𝑘 ∈ (1...𝑀)1))
310		fsumconst 15694	. . . . . . . . . . . 12 ⊢ (((1...𝑀) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑘 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1))
311	1, 141, 310	sylancl 586	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1))
312		nnnn0 12385	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
313		hashfz1 14250	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
314	312, 313	syl 17	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (♯‘(1...𝑀)) = 𝑀)
315	314	oveq1d 7361	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((♯‘(1...𝑀)) · 1) = (𝑀 · 1))
316		nncn 12130	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
317	316	mulridd 11126	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑀 · 1) = 𝑀)
318	311, 315, 317	3eqtrd 2770	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)1 = 𝑀)
319	201, 318	oveq12d 7364	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) + Σ𝑘 ∈ (1...𝑀)1) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
320	307, 309, 319	3eqtrd 2770	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
321		3cn 12203	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℂ
322	321	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 3 ∈ ℂ)
323	139, 143, 322	adddid 11133	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (((2 · 𝑀) − 1) + 3)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + ((2 · 𝑀) · 3)))
324		df-3 12186	. . . . . . . . . . . . . . . . 17 ⊢ 3 = (2 + 1)
325	324	oveq1i 7356	. . . . . . . . . . . . . . . 16 ⊢ (3 − 1) = ((2 + 1) − 1)
326	49, 141	pncan3oi 11373	. . . . . . . . . . . . . . . 16 ⊢ ((2 + 1) − 1) = 2
327	325, 326, 161	3eqtri 2758	. . . . . . . . . . . . . . 15 ⊢ (3 − 1) = (1 + 1)
328	327	oveq2i 7357	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑀) + (3 − 1)) = ((2 · 𝑀) + (1 + 1))
329	139, 146, 322	subadd23d 11491	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = ((2 · 𝑀) + (3 − 1)))
330	139, 146, 146	addassd 11131	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
331	328, 329, 330	3eqtr4a 2792	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = (((2 · 𝑀) + 1) + 1))
332	3	oveq1i 7356	. . . . . . . . . . . . 13 ⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
333	331, 332	eqtr4di 2784	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = (𝑁 + 1))
334	333	oveq2d 7362	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (((2 · 𝑀) − 1) + 3)) = ((2 · 𝑀) · (𝑁 + 1)))
335		2cnd 12200	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → 2 ∈ ℂ)
336	335, 316, 322	mul32d 11320	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · 3) = ((2 · 3) · 𝑀))
337		3t2e6 12283	. . . . . . . . . . . . . . 15 ⊢ (3 · 2) = 6
338	321, 49	mulcomi 11117	. . . . . . . . . . . . . . 15 ⊢ (3 · 2) = (2 · 3)
339	337, 338	eqtr3i 2756	. . . . . . . . . . . . . 14 ⊢ 6 = (2 · 3)
340	339	oveq1i 7356	. . . . . . . . . . . . 13 ⊢ (6 · 𝑀) = ((2 · 3) · 𝑀)
341	336, 340	eqtr4di 2784	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · 3) = (6 · 𝑀))
342	341	oveq2d 7362	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · ((2 · 𝑀) − 1)) + ((2 · 𝑀) · 3)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)))
343	323, 334, 342	3eqtr3d 2774	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (𝑁 + 1)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)))
344	343	oveq1d 7361	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)) / 6))
345		mulcl 11087	. . . . . . . . . . 11 ⊢ ((6 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (6 · 𝑀) ∈ ℂ)
346	173, 316, 345	sylancr 587	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (6 · 𝑀) ∈ ℂ)
347	173	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 6 ∈ ℂ)
348	110	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 6 ≠ 0)
349	179, 346, 347, 348	divdird 11932	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + ((6 · 𝑀) / 6)))
350	316, 347, 348	divcan3d 11899	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → ((6 · 𝑀) / 6) = 𝑀)
351	350	oveq2d 7362	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + ((6 · 𝑀) / 6)) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
352	344, 349, 351	3eqtrd 2770	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
353	320, 352	eqtr4d 2769	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = (((2 · 𝑀) · (𝑁 + 1)) / 6))
354	190, 353	oveq12d 7364	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)))
355	139, 63, 266, 63, 64, 64	divmuldivd 11935	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁)))
356	193	oveq2d 7362	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁)))
357	355, 356	eqtr4d 2769	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2)))
358	357	oveq2d 7362	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))) = (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))))
359	279, 354, 358	3eqtr4d 2776	. . . . 5 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))))
360	268, 272, 359	3eqtr4d 2776	. . . 4 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)))
361	225	recnd 11137	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ)
362	1, 35, 361	fsummulc2 15688	. . . 4 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
363	264, 360, 362	3eqtrd 2770	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
364	254, 218, 363	3brtr4d 5123	. 2 ⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) ≤ (𝐾‘𝑀))
365	219, 364	jca 511	1 ⊢ (𝑀 ∈ ℕ → ((𝐽‘𝑀) ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ (𝐾‘𝑀)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ⊤wtru 1542 ∈ wcel 2111 ≠ wne 2928 Vcvv 3436 {csn 4576 class class class wbr 5091 ↦ cmpt 5172 × cxp 5614 ‘cfv 6481 (class class class)co 7346 ∘_f cof 7608 Fincfn 8869 ℂcc 11001 ℝcr 11002 0cc0 11003 1c1 11004 + caddc 11006 · cmul 11008 < clt 11143 ≤ cle 11144 − cmin 11341 -cneg 11342 / cdiv 11771 ℕcn 12122 2c2 12177 3c3 12178 6c6 12181 ℕ₀cn0 12378 ℤcz 12465 ℤ_≥cuz 12729 ℝ⁺crp 12887 (,)cioo 13242 ...cfz 13404 seqcseq 13905 ↑cexp 13965 Ccbc 14206 ♯chash 14234 Σcsu 15590 sincsin 15967 cosccos 15968 tanctan 15969 πcpi 15970

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-inf2 9531 ax-cnex 11059 ax-resscn 11060 ax-1cn 11061 ax-icn 11062 ax-addcl 11063 ax-addrcl 11064 ax-mulcl 11065 ax-mulrcl 11066 ax-mulcom 11067 ax-addass 11068 ax-mulass 11069 ax-distr 11070 ax-i2m1 11071 ax-1ne0 11072 ax-1rid 11073 ax-rnegex 11074 ax-rrecex 11075 ax-cnre 11076 ax-pre-lttri 11077 ax-pre-lttrn 11078 ax-pre-ltadd 11079 ax-pre-mulgt0 11080 ax-pre-sup 11081 ax-addf 11082

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-tp 4581 df-op 4583 df-uni 4860 df-int 4898 df-iun 4943 df-iin 4944 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-se 5570 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-om 7797 df-1st 7921 df-2nd 7922 df-supp 8091 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-oadd 8389 df-er 8622 df-map 8752 df-pm 8753 df-ixp 8822 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-fsupp 9246 df-fi 9295 df-sup 9326 df-inf 9327 df-oi 9396 df-dju 9791 df-card 9829 df-pnf 11145 df-mnf 11146 df-xr 11147 df-ltxr 11148 df-le 11149 df-sub 11343 df-neg 11344 df-div 11772 df-nn 12123 df-2 12185 df-3 12186 df-4 12187 df-5 12188 df-6 12189 df-7 12190 df-8 12191 df-9 12192 df-n0 12379 df-xnn0 12452 df-z 12466 df-dec 12586 df-uz 12730 df-q 12844 df-rp 12888 df-xneg 13008 df-xadd 13009 df-xmul 13010 df-ioo 13246 df-ioc 13247 df-ico 13248 df-icc 13249 df-fz 13405 df-fzo 13552 df-fl 13693 df-mod 13771 df-seq 13906 df-exp 13966 df-fac 14178 df-bc 14207 df-hash 14235 df-shft 14971 df-cj 15003 df-re 15004 df-im 15005 df-sqrt 15139 df-abs 15140 df-limsup 15375 df-clim 15392 df-rlim 15393 df-sum 15591 df-ef 15971 df-sin 15973 df-cos 15974 df-tan 15975 df-pi 15976 df-struct 17055 df-sets 17072 df-slot 17090 df-ndx 17102 df-base 17118 df-ress 17139 df-plusg 17171 df-mulr 17172 df-starv 17173 df-sca 17174 df-vsca 17175 df-ip 17176 df-tset 17177 df-ple 17178 df-ds 17180 df-unif 17181 df-hom 17182 df-cco 17183 df-rest 17323 df-topn 17324 df-0g 17342 df-gsum 17343 df-topgen 17344 df-pt 17345 df-prds 17348 df-xrs 17403 df-qtop 17408 df-imas 17409 df-xps 17411 df-mre 17485 df-mrc 17486 df-acs 17488 df-mgm 18545 df-sgrp 18624 df-mnd 18640 df-submnd 18689 df-mulg 18978 df-cntz 19227 df-cmn 19692 df-psmet 21281 df-xmet 21282 df-met 21283 df-bl 21284 df-mopn 21285 df-fbas 21286 df-fg 21287 df-cnfld 21290 df-top 22807 df-topon 22824 df-topsp 22846 df-bases 22859 df-cld 22932 df-ntr 22933 df-cls 22934 df-nei 23011 df-lp 23049 df-perf 23050 df-cn 23140 df-cnp 23141 df-haus 23228 df-tx 23475 df-hmeo 23668 df-fil 23759 df-fm 23851 df-flim 23852 df-flf 23853 df-xms 24233 df-ms 24234 df-tms 24235 df-cncf 24796 df-0p 25596 df-limc 25792 df-dv 25793 df-ply 26118 df-idp 26119 df-coe 26120 df-dgr 26121 df-quot 26224

This theorem is referenced by: basellem9 27024

W3C validator