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 25665

Description: Lemma for basel 25667. 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 25662. (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 13342	. . . 4 ⊢ (𝑀 ∈ ℕ → (1...𝑀) ∈ Fin)
2		pire 25044	. . . . . . . 8 ⊢ π ∈ ℝ
3		basellem8.n	. . . . . . . . 9 ⊢ 𝑁 = ((2 · 𝑀) + 1)
4		2nn 11711	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ
5		nnmulcl 11662	. . . . . . . . . . 11 ⊢ ((2 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (2 · 𝑀) ∈ ℕ)
6	4, 5	mpan 688	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℕ)
7	6	peano2nnd 11655	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) + 1) ∈ ℕ)
8	3, 7	eqeltrid 2917	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → 𝑁 ∈ ℕ)
9		nndivre 11679	. . . . . . . 8 ⊢ ((π ∈ ℝ ∧ 𝑁 ∈ ℕ) → (π / 𝑁) ∈ ℝ)
10	2, 8, 9	sylancr 589	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (π / 𝑁) ∈ ℝ)
11	10	resqcld 13612	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) ∈ ℝ)
12	11	adantr 483	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℝ)
13	3	basellem1 25658	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)))
14		tanrpcl 25090	. . . . . . . 8 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
15	13, 14	syl 17	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
16	15	rpred 12432	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℝ)
17	15	rpne0d 12437	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ≠ 0)
18		2z 12015	. . . . . . . 8 ⊢ 2 ∈ ℤ
19		znegcl 12018	. . . . . . . 8 ⊢ (2 ∈ ℤ → -2 ∈ ℤ)
20	18, 19	ax-mp 5	. . . . . . 7 ⊢ -2 ∈ ℤ
21	20	a1i 11	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → -2 ∈ ℤ)
22	16, 17, 21	reexpclzd 13611	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℝ)
23	12, 22	remulcld 10671	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ∈ ℝ)
24		elfznn 12937	. . . . . . 7 ⊢ (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ)
25	24	adantl 484	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℕ)
26	25	nnred 11653	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ)
27	25	nnne0d 11688	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ≠ 0)
28	26, 27, 21	reexpclzd 13611	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℝ)
29	16	recnd 10669	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) ∈ ℂ)
30		2nn0 11915	. . . . . . . 8 ⊢ 2 ∈ ℕ₀
31		expneg 13438	. . . . . . . 8 ⊢ (((tan‘((𝑘 · π) / 𝑁)) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)))
32	29, 30, 31	sylancl 588	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)))
33	32	oveq2d 7172	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))))
34	10	recnd 10669	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (π / 𝑁) ∈ ℂ)
35	34	sqcld 13509	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) ∈ ℂ)
36	35	adantr 483	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((π / 𝑁)↑2) ∈ ℂ)
37		rpexpcl 13449	. . . . . . . . . 10 ⊢ (((tan‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
38	15, 18, 37	sylancl 588	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
39	38	rpred 12432	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ)
40	39	recnd 10669	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
41	38	rpne0d 12437	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
42	36, 40, 41	divrecd 11419	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((tan‘((𝑘 · π) / 𝑁))↑2))))
43	33, 42	eqtr4d 2859	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)))
44	25	nnrpd 12430	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℝ⁺)
45		rpexpcl 13449	. . . . . . 7 ⊢ ((𝑘 ∈ ℝ⁺ ∧ -2 ∈ ℤ) → (𝑘↑-2) ∈ ℝ⁺)
46	44, 20, 45	sylancl 588	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℝ⁺)
47		2cn 11713	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
48	47	negnegi 10956	. . . . . . . . . . 11 ⊢ --2 = 2
49	48	oveq2i 7167	. . . . . . . . . 10 ⊢ (𝑘↑--2) = (𝑘↑2)
50	25	nncnd 11654	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 𝑘 ∈ ℂ)
51	50, 27, 21	expnegd 13518	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑--2) = (1 / (𝑘↑-2)))
52	49, 51	syl5reqr 2871	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (𝑘↑-2)) = (𝑘↑2))
53	52	oveq1d 7171	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((1 / (𝑘↑-2)) · ((π / 𝑁)↑2)) = ((𝑘↑2) · ((π / 𝑁)↑2)))
54		nncn 11646	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
55		nnne0 11672	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0)
56	20	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → -2 ∈ ℤ)
57	54, 55, 56	expclzd 13516	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (𝑘↑-2) ∈ ℂ)
58	25, 57	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ∈ ℂ)
59	50, 27, 21	expne0d 13517	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≠ 0)
60	36, 58, 59	divrec2d 11420	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) = ((1 / (𝑘↑-2)) · ((π / 𝑁)↑2)))
61	2	recni 10655	. . . . . . . . . . . 12 ⊢ π ∈ ℂ
62	61	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → π ∈ ℂ)
63	8	nncnd 11654	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑁 ∈ ℂ)
64	8	nnne0d 11688	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑁 ≠ 0)
65	63, 64	jca 514	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
66	65	adantr 483	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
67		divass 11316	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℂ ∧ π ∈ ℂ ∧ (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0)) → ((𝑘 · π) / 𝑁) = (𝑘 · (π / 𝑁)))
68	50, 62, 66, 67	syl3anc 1367	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) = (𝑘 · (π / 𝑁)))
69	68	oveq1d 7171	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘 · (π / 𝑁))↑2))
70	34	adantr 483	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (π / 𝑁) ∈ ℂ)
71	50, 70	sqmuld 13523	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · (π / 𝑁))↑2) = ((𝑘↑2) · ((π / 𝑁)↑2)))
72	69, 71	eqtrd 2856	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) = ((𝑘↑2) · ((π / 𝑁)↑2)))
73	53, 60, 72	3eqtr4d 2866	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) = (((𝑘 · π) / 𝑁)↑2))
74		elioore 12769	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → ((𝑘 · π) / 𝑁) ∈ ℝ)
75	13, 74	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℝ)
76	75	resqcld 13612	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ∈ ℝ)
77		tangtx 25091	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → ((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)))
78	13, 77	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)))
79		eliooord 12797	. . . . . . . . . . . . . 14 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (0 < ((𝑘 · π) / 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π / 2)))
80	13, 79	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < ((𝑘 · π) / 𝑁) ∧ ((𝑘 · π) / 𝑁) < (π / 2)))
81	80	simpld 497	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < ((𝑘 · π) / 𝑁))
82	75, 81	elrpd 12429	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℝ⁺)
83	82	rpge0d 12436	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ ((𝑘 · π) / 𝑁))
84	15	rpge0d 12436	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (tan‘((𝑘 · π) / 𝑁)))
85	75, 16, 83, 84	lt2sqd 13620	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁) < (tan‘((𝑘 · π) / 𝑁)) ↔ (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2)))
86	78, 85	mpbid 234	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) < ((tan‘((𝑘 · π) / 𝑁))↑2))
87	76, 39, 86	ltled 10788	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘 · π) / 𝑁)↑2) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2))
88	73, 87	eqbrtrd 5088	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / (𝑘↑-2)) ≤ ((tan‘((𝑘 · π) / 𝑁))↑2))
89	12, 46, 38, 88	lediv23d 12500	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((tan‘((𝑘 · π) / 𝑁))↑2)) ≤ (𝑘↑-2))
90	43, 89	eqbrtrd 5088	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ≤ (𝑘↑-2))
91	1, 23, 28, 90	fsumle 15154	. . 3 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)) ≤ Σ𝑘 ∈ (1...𝑀)(𝑘↑-2))
92		oveq2 7164	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑀 → (2 · 𝑛) = (2 · 𝑀))
93	92	oveq1d 7171	. . . . . . . . . 10 ⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = ((2 · 𝑀) + 1))
94	93, 3	syl6eqr 2874	. . . . . . . . 9 ⊢ (𝑛 = 𝑀 → ((2 · 𝑛) + 1) = 𝑁)
95	94	oveq2d 7172	. . . . . . . 8 ⊢ (𝑛 = 𝑀 → (1 / ((2 · 𝑛) + 1)) = (1 / 𝑁))
96	95	oveq2d 7172	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / 𝑁)))
97	96	oveq2d 7172	. . . . . 6 ⊢ (𝑛 = 𝑀 → (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) = (((π↑2) / 6) · (1 − (1 / 𝑁))))
98	95	oveq2d 7172	. . . . . . 7 ⊢ (𝑛 = 𝑀 → (-2 · (1 / ((2 · 𝑛) + 1))) = (-2 · (1 / 𝑁)))
99	98	oveq2d 7172	. . . . . 6 ⊢ (𝑛 = 𝑀 → (1 + (-2 · (1 / ((2 · 𝑛) + 1)))) = (1 + (-2 · (1 / 𝑁))))
100	97, 99	oveq12d 7174	. . . . 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 11644	. . . . . . . . 9 ⊢ ℕ ∈ V
103	102	a1i 11	. . . . . . . 8 ⊢ (⊤ → ℕ ∈ V)
104		ovexd 7191	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V)
105		ovexd 7191	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 + (-2 · (1 / ((2 · 𝑛) + 1)))) ∈ V)
106		basel.h	. . . . . . . . 9 ⊢ 𝐻 = ((ℕ × {((π↑2) / 6)}) ∘_f · ((ℕ × {1}) ∘_f − 𝐺))
107	2	resqcli 13550	. . . . . . . . . . . 12 ⊢ (π↑2) ∈ ℝ
108		6re 11728	. . . . . . . . . . . 12 ⊢ 6 ∈ ℝ
109		6nn 11727	. . . . . . . . . . . . 13 ⊢ 6 ∈ ℕ
110	109	nnne0i 11678	. . . . . . . . . . . 12 ⊢ 6 ≠ 0
111	107, 108, 110	redivcli 11407	. . . . . . . . . . 11 ⊢ ((π↑2) / 6) ∈ ℝ
112	111	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → ((π↑2) / 6) ∈ ℝ)
113		ovexd 7191	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 − (1 / ((2 · 𝑛) + 1))) ∈ V)
114		fconstmpt 5614	. . . . . . . . . . 11 ⊢ (ℕ × {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) / 6))
115	114	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℕ × {((π↑2) / 6)}) = (𝑛 ∈ ℕ ↦ ((π↑2) / 6)))
116		1zzd 12014	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 1 ∈ ℤ)
117		ovexd 7191	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / ((2 · 𝑛) + 1)) ∈ V)
118		fconstmpt 5614	. . . . . . . . . . . 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 7426	. . . . . . . . . 10 ⊢ (⊤ → ((ℕ × {1}) ∘_f − 𝐺) = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
123	103, 112, 113, 115, 122	offval2 7426	. . . . . . . . 9 ⊢ (⊤ → ((ℕ × {((π↑2) / 6)}) ∘_f · ((ℕ × {1}) ∘_f − 𝐺)) = (𝑛 ∈ ℕ ↦ (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1))))))
124	106, 123	syl5eq 2868	. . . . . . . 8 ⊢ (⊤ → 𝐻 = (𝑛 ∈ ℕ ↦ (((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1))))))
125		ovexd 7191	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (-2 · (1 / ((2 · 𝑛) + 1))) ∈ V)
126	47	negcli 10954	. . . . . . . . . . 11 ⊢ -2 ∈ ℂ
127	126	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → -2 ∈ ℂ)
128		fconstmpt 5614	. . . . . . . . . . 11 ⊢ (ℕ × {-2}) = (𝑛 ∈ ℕ ↦ -2)
129	128	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℕ × {-2}) = (𝑛 ∈ ℕ ↦ -2))
130	103, 127, 117, 129, 121	offval2 7426	. . . . . . . . 9 ⊢ (⊤ → ((ℕ × {-2}) ∘_f · 𝐺) = (𝑛 ∈ ℕ ↦ (-2 · (1 / ((2 · 𝑛) + 1)))))
131	103, 116, 125, 119, 130	offval2 7426	. . . . . . . 8 ⊢ (⊤ → ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺)) = (𝑛 ∈ ℕ ↦ (1 + (-2 · (1 / ((2 · 𝑛) + 1))))))
132	103, 104, 105, 124, 131	offval2 7426	. . . . . . 7 ⊢ (⊤ → (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1)))))))
133	132	mptru 1544	. . . . . 6 ⊢ (𝐻 ∘_f · ((ℕ × {1}) ∘_f + ((ℕ × {-2}) ∘_f · 𝐺))) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1))))))
134	101, 133	eqtri 2844	. . . . 5 ⊢ 𝐽 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (-2 · (1 / ((2 · 𝑛) + 1))))))
135		ovex 7189	. . . . 5 ⊢ ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) ∈ V
136	100, 134, 135	fvmpt 6768	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))))
137	111	recni 10655	. . . . . . . 8 ⊢ ((π↑2) / 6) ∈ ℂ
138	137	a1i 11	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((π↑2) / 6) ∈ ℂ)
139	6	nncnd 11654	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (2 · 𝑀) ∈ ℂ)
140	139, 63, 64	divcld 11416	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) / 𝑁) ∈ ℂ)
141		ax-1cn 10595	. . . . . . . . 9 ⊢ 1 ∈ ℂ
142		subcl 10885	. . . . . . . . 9 ⊢ (((2 · 𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → ((2 · 𝑀) − 1) ∈ ℂ)
143	139, 141, 142	sylancl 588	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) − 1) ∈ ℂ)
144	143, 63, 64	divcld 11416	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) / 𝑁) ∈ ℂ)
145	138, 140, 144	mulassd 10664	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · (((2 · 𝑀) − 1) / 𝑁)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))))
146		1cnd 10636	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 1 ∈ ℂ)
147	63, 146, 63, 64	divsubdird 11455	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((𝑁 / 𝑁) − (1 / 𝑁)))
148	3	oveq1i 7166	. . . . . . . . . . 11 ⊢ (𝑁 − 1) = (((2 · 𝑀) + 1) − 1)
149		pncan 10892	. . . . . . . . . . . 12 ⊢ (((2 · 𝑀) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑀) + 1) − 1) = (2 · 𝑀))
150	139, 141, 149	sylancl 588	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) − 1) = (2 · 𝑀))
151	148, 150	syl5eq 2868	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 − 1) = (2 · 𝑀))
152	151	oveq1d 7171	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) / 𝑁) = ((2 · 𝑀) / 𝑁))
153	63, 64	dividd 11414	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 / 𝑁) = 1)
154	153	oveq1d 7171	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) − (1 / 𝑁)) = (1 − (1 / 𝑁)))
155	147, 152, 154	3eqtr3rd 2865	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (1 − (1 / 𝑁)) = ((2 · 𝑀) / 𝑁))
156	155	oveq2d 7172	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (1 − (1 / 𝑁))) = (((π↑2) / 6) · ((2 · 𝑀) / 𝑁)))
157	126	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → -2 ∈ ℂ)
158	63, 157, 63, 64	divdird 11454	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = ((𝑁 / 𝑁) + (-2 / 𝑁)))
159		negsub 10934	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑁 + -2) = (𝑁 − 2))
160	63, 47, 159	sylancl 588	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = (𝑁 − 2))
161		df-2 11701	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
162	3, 161	oveq12i 7168	. . . . . . . . . . 11 ⊢ (𝑁 − 2) = (((2 · 𝑀) + 1) − (1 + 1))
163	139, 146, 146	pnpcan2d 11035	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) − (1 + 1)) = ((2 · 𝑀) − 1))
164	162, 163	syl5eq 2868	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁 − 2) = ((2 · 𝑀) − 1))
165	160, 164	eqtrd 2856	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (𝑁 + -2) = ((2 · 𝑀) − 1))
166	165	oveq1d 7171	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 + -2) / 𝑁) = (((2 · 𝑀) − 1) / 𝑁))
167	157, 63, 64	divrecd 11419	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (-2 / 𝑁) = (-2 · (1 / 𝑁)))
168	153, 167	oveq12d 7174	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (-2 / 𝑁)) = (1 + (-2 · (1 / 𝑁))))
169	158, 166, 168	3eqtr3rd 2865	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (1 + (-2 · (1 / 𝑁))) = (((2 · 𝑀) − 1) / 𝑁))
170	156, 169	oveq12d 7174	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · (((2 · 𝑀) − 1) / 𝑁)))
171	8	nnsqcld 13606	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈ ℕ)
172	171	nncnd 11654	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ∈ ℂ)
173		6cn 11729	. . . . . . . . . 10 ⊢ 6 ∈ ℂ
174		mulcom 10623	. . . . . . . . . 10 ⊢ (((𝑁↑2) ∈ ℂ ∧ 6 ∈ ℂ) → ((𝑁↑2) · 6) = (6 · (𝑁↑2)))
175	172, 173, 174	sylancl 588	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁↑2) · 6) = (6 · (𝑁↑2)))
176	175	oveq2d 7172	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
177	107	recni 10655	. . . . . . . . . 10 ⊢ (π↑2) ∈ ℂ
178	177	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (π↑2) ∈ ℂ)
179	139, 143	mulcld 10661	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · ((2 · 𝑀) − 1)) ∈ ℂ)
180	171	nnne0d 11688	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) ≠ 0)
181	172, 180	jca 514	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((𝑁↑2) ∈ ℂ ∧ (𝑁↑2) ≠ 0))
182	173, 110	pm3.2i 473	. . . . . . . . . 10 ⊢ (6 ∈ ℂ ∧ 6 ≠ 0)
183	182	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (6 ∈ ℂ ∧ 6 ≠ 0))
184		divmuldiv 11340	. . . . . . . . 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 836	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / ((𝑁↑2) · 6)))
186		divmuldiv 11340	. . . . . . . . 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 836	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · ((2 · 𝑀) − 1))) / (6 · (𝑁↑2))))
188	176, 185, 187	3eqtr4d 2866	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))))
189	61	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → π ∈ ℂ)
190	189, 63, 64	sqdivd 13524	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((π / 𝑁)↑2) = ((π↑2) / (𝑁↑2)))
191	190	oveq1d 7171	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
192	139, 63, 143, 63, 64, 64	divmuldivd 11457	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁 · 𝑁)))
193	63	sqvald 13508	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (𝑁↑2) = (𝑁 · 𝑁))
194	193	oveq2d 7172	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁 · 𝑁)))
195	192, 194	eqtr4d 2859	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2)))
196	195	oveq2d 7172	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))) = (((π↑2) / 6) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / (𝑁↑2))))
197	188, 191, 196	3eqtr4d 2866	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · (((2 · 𝑀) − 1) / 𝑁))))
198	145, 170, 197	3eqtr4d 2866	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
199		eqid 2821	. . . . . . 7 ⊢ (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑥↑𝑗))) = (𝑥 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑀)(((𝑁C(2 · 𝑗)) · (-1↑(𝑀 − 𝑗))) · (𝑥↑𝑗)))
200		eqid 2821	. . . . . . 7 ⊢ (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2)) = (𝑛 ∈ (1...𝑀) ↦ ((tan‘((𝑛 · π) / 𝑁))↑-2))
201	3, 199, 200	basellem5 25662	. . . . . 6 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6))
202	201	oveq2d 7172	. . . . 5 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6)))
203	198, 202	eqtr4d 2859	. . . 4 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (-2 · (1 / 𝑁)))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)))
204	22	recnd 10669	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ)
205	1, 35, 204	fsummulc2 15139	. . . 4 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)))
206	136, 203, 205	3eqtrd 2860	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((tan‘((𝑘 · π) / 𝑁))↑-2)))
207		oveq1 7163	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑛↑-2) = (𝑘↑-2))
208		eqid 2821	. . . . . . 7 ⊢ (𝑛 ∈ ℕ ↦ (𝑛↑-2)) = (𝑛 ∈ ℕ ↦ (𝑛↑-2))
209		ovex 7189	. . . . . . 7 ⊢ (𝑘↑-2) ∈ V
210	207, 208, 209	fvmpt 6768	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2))
211	25, 210	syl 17	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ (𝑛↑-2))‘𝑘) = (𝑘↑-2))
212		id 22	. . . . . 6 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ)
213		nnuz 12282	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
214	212, 213	eleqtrdi 2923	. . . . 5 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (ℤ_≥‘1))
215	211, 214, 58	fsumser 15087	. . . 4 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(𝑘↑-2) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))‘𝑀))
216		basel.f	. . . . 5 ⊢ 𝐹 = seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))
217	216	fveq1i 6671	. . . 4 ⊢ (𝐹‘𝑀) = (seq1( + , (𝑛 ∈ ℕ ↦ (𝑛↑-2)))‘𝑀)
218	215, 217	syl6reqr 2875	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) = Σ𝑘 ∈ (1...𝑀)(𝑘↑-2))
219	91, 206, 218	3brtr4d 5098	. 2 ⊢ (𝑀 ∈ ℕ → (𝐽‘𝑀) ≤ (𝐹‘𝑀))
220	75	resincld 15496	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ)
221		sincosq1sgn 25084	. . . . . . . . 9 ⊢ (((𝑘 · π) / 𝑁) ∈ (0(,)(π / 2)) → (0 < (sin‘((𝑘 · π) / 𝑁)) ∧ 0 < (cos‘((𝑘 · π) / 𝑁))))
222	13, 221	syl 17	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) ∧ 0 < (cos‘((𝑘 · π) / 𝑁))))
223	222	simpld 497	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (sin‘((𝑘 · π) / 𝑁)))
224	223	gt0ne0d 11204	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≠ 0)
225	220, 224, 21	reexpclzd 13611	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) ∈ ℝ)
226	12, 225	remulcld 10671	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) ∈ ℝ)
227		sinltx 15542	. . . . . . . . . 10 ⊢ (((𝑘 · π) / 𝑁) ∈ ℝ⁺ → (sin‘((𝑘 · π) / 𝑁)) < ((𝑘 · π) / 𝑁))
228	82, 227	syl 17	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) < ((𝑘 · π) / 𝑁))
229	220, 75, 228	ltled 10788	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁))
230		0re 10643	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
231		ltle 10729	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ) → (0 < (sin‘((𝑘 · π) / 𝑁)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁))))
232	230, 220, 231	sylancr 589	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (0 < (sin‘((𝑘 · π) / 𝑁)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁))))
233	223, 232	mpd 15	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 ≤ (sin‘((𝑘 · π) / 𝑁)))
234	220, 75, 233, 83	le2sqd 13621	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁)) ≤ ((𝑘 · π) / 𝑁) ↔ ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2)))
235	229, 234	mpbid 234	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((𝑘 · π) / 𝑁)↑2))
236	235, 73	breqtrrd 5094	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2)))
237	220	resqcld 13612	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ)
238	237, 12, 46	lemuldiv2d 12482	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑-2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔ ((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2))))
239	220, 223	elrpd 12429	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺)
240		rpexpcl 13449	. . . . . . . . 9 ⊢ (((sin‘((𝑘 · π) / 𝑁)) ∈ ℝ⁺ ∧ 2 ∈ ℤ) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
241	239, 18, 240	sylancl 588	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℝ⁺)
242	28, 12, 241	lemuldivd 12481	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((𝑘↑-2) · ((sin‘((𝑘 · π) / 𝑁))↑2)) ≤ ((π / 𝑁)↑2) ↔ (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
243	238, 242	bitr3d 283	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) ≤ (((π / 𝑁)↑2) / (𝑘↑-2)) ↔ (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
244	236, 243	mpbid 234	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≤ (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
245	220	recnd 10669	. . . . . . . 8 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (sin‘((𝑘 · π) / 𝑁)) ∈ ℂ)
246		expneg 13438	. . . . . . . 8 ⊢ (((sin‘((𝑘 · π) / 𝑁)) ∈ ℂ ∧ 2 ∈ ℕ₀) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
247	245, 30, 246	sylancl 588	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
248	247	oveq2d 7172	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) · (1 / ((sin‘((𝑘 · π) / 𝑁))↑2))))
249	237	recnd 10669	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
250	241	rpne0d 12437	. . . . . . 7 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
251	36, 249, 250	divrecd 11419	. . . . . 6 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (((π / 𝑁)↑2) · (1 / ((sin‘((𝑘 · π) / 𝑁))↑2))))
252	248, 251	eqtr4d 2859	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π / 𝑁)↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
253	244, 252	breqtrrd 5094	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (𝑘↑-2) ≤ (((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
254	1, 28, 226, 253	fsumle 15154	. . 3 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(𝑘↑-2) ≤ Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
255	95	oveq2d 7172	. . . . . 6 ⊢ (𝑛 = 𝑀 → (1 + (1 / ((2 · 𝑛) + 1))) = (1 + (1 / 𝑁)))
256	97, 255	oveq12d 7174	. . . . 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 7191	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 + (1 / ((2 · 𝑛) + 1))) ∈ V)
259	103, 116, 117, 119, 121	offval2 7426	. . . . . . . 8 ⊢ (⊤ → ((ℕ × {1}) ∘_f + 𝐺) = (𝑛 ∈ ℕ ↦ (1 + (1 / ((2 · 𝑛) + 1)))))
260	103, 104, 258, 124, 259	offval2 7426	. . . . . . 7 ⊢ (⊤ → (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1))))))
261	260	mptru 1544	. . . . . 6 ⊢ (𝐻 ∘_f · ((ℕ × {1}) ∘_f + 𝐺)) = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))))
262	257, 261	eqtri 2844	. . . . 5 ⊢ 𝐾 = (𝑛 ∈ ℕ ↦ ((((π↑2) / 6) · (1 − (1 / ((2 · 𝑛) + 1)))) · (1 + (1 / ((2 · 𝑛) + 1)))))
263		ovex 7189	. . . . 5 ⊢ ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) ∈ V
264	256, 262, 263	fvmpt 6768	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))))
265		peano2cn 10812	. . . . . . . 8 ⊢ (𝑁 ∈ ℂ → (𝑁 + 1) ∈ ℂ)
266	63, 265	syl 17	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
267	266, 63, 64	divcld 11416	. . . . . 6 ⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
268	138, 140, 267	mulassd 10664	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))))
269	63, 146, 63, 64	divdird 11454	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((𝑁 + 1) / 𝑁) = ((𝑁 / 𝑁) + (1 / 𝑁)))
270	153	oveq1d 7171	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → ((𝑁 / 𝑁) + (1 / 𝑁)) = (1 + (1 / 𝑁)))
271	269, 270	eqtr2d 2857	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (1 + (1 / 𝑁)) = ((𝑁 + 1) / 𝑁))
272	156, 271	oveq12d 7174	. . . . 5 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = ((((π↑2) / 6) · ((2 · 𝑀) / 𝑁)) · ((𝑁 + 1) / 𝑁)))
273	175	oveq2d 7172	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
274	139, 266	mulcld 10661	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (𝑁 + 1)) ∈ ℂ)
275		divmuldiv 11340	. . . . . . . 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 836	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / ((𝑁↑2) · 6)))
277		divmuldiv 11340	. . . . . . . 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 836	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))) = (((π↑2) · ((2 · 𝑀) · (𝑁 + 1))) / (6 · (𝑁↑2))))
279	273, 276, 278	3eqtr4d 2866	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)) = (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))))
280	75	recoscld 15497	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℝ)
281	280	recnd 10669	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ∈ ℂ)
282	281	sqcld 13509	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ∈ ℂ)
283	249, 282, 249, 250	divdird 11454	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = ((((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) + (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))))
284	75	recnd 10669	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((𝑘 · π) / 𝑁) ∈ ℂ)
285		sincossq 15529	. . . . . . . . . . . . . 14 ⊢ (((𝑘 · π) / 𝑁) ∈ ℂ → (((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) = 1)
286	284, 285	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) = 1)
287	286	oveq1d 7171	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) + ((cos‘((𝑘 · π) / 𝑁))↑2)) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)))
288	249, 250	dividd 11414	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = 1)
289	222	simprd 498	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 0 < (cos‘((𝑘 · π) / 𝑁)))
290	289	gt0ne0d 11204	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (cos‘((𝑘 · π) / 𝑁)) ≠ 0)
291		tanval 15481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑘 · π) / 𝑁) ∈ ℂ ∧ (cos‘((𝑘 · π) / 𝑁)) ≠ 0) → (tan‘((𝑘 · π) / 𝑁)) = ((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁))))
292	284, 290, 291	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (tan‘((𝑘 · π) / 𝑁)) = ((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁))))
293	292	oveq1d 7171	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2))
294	245, 281, 290	sqdivd 13524	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((sin‘((𝑘 · π) / 𝑁)) / (cos‘((𝑘 · π) / 𝑁)))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2)))
295	293, 294	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((tan‘((𝑘 · π) / 𝑁))↑2) = (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2)))
296	295	oveq2d 7172	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((tan‘((𝑘 · π) / 𝑁))↑2)) = (1 / (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))))
297		sqne0 13490	. . . . . . . . . . . . . . . . 17 ⊢ ((cos‘((𝑘 · π) / 𝑁)) ∈ ℂ → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0))
298	281, 297	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0 ↔ (cos‘((𝑘 · π) / 𝑁)) ≠ 0))
299	290, 298	mpbird 259	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((cos‘((𝑘 · π) / 𝑁))↑2) ≠ 0)
300	249, 282, 250, 299	recdivd 11433	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / (((sin‘((𝑘 · π) / 𝑁))↑2) / ((cos‘((𝑘 · π) / 𝑁))↑2))) = (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)))
301	32, 296, 300	3eqtrrd 2861	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) = ((tan‘((𝑘 · π) / 𝑁))↑-2))
302	288, 301	oveq12d 7174	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((((sin‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2)) + (((cos‘((𝑘 · π) / 𝑁))↑2) / ((sin‘((𝑘 · π) / 𝑁))↑2))) = (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)))
303	283, 287, 302	3eqtr3d 2864	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 / ((sin‘((𝑘 · π) / 𝑁))↑2)) = (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)))
304		addcom 10826	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℂ ∧ ((tan‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ) → (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
305	141, 204, 304	sylancr 589	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → (1 + ((tan‘((𝑘 · π) / 𝑁))↑-2)) = (((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
306	247, 303, 305	3eqtrd 2860	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) = (((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
307	306	sumeq2dv 15060	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑-2) + 1))
308		1cnd 10636	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → 1 ∈ ℂ)
309	1, 204, 308	fsumadd 15096	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)(((tan‘((𝑘 · π) / 𝑁))↑-2) + 1) = (Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) + Σ𝑘 ∈ (1...𝑀)1))
310		fsumconst 15145	. . . . . . . . . . . 12 ⊢ (((1...𝑀) ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑘 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1))
311	1, 141, 310	sylancl 588	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1))
312		nnnn0 11905	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℕ₀)
313		hashfz1 13707	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ₀ → (♯‘(1...𝑀)) = 𝑀)
314	312, 313	syl 17	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (♯‘(1...𝑀)) = 𝑀)
315	314	oveq1d 7171	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((♯‘(1...𝑀)) · 1) = (𝑀 · 1))
316		nncn 11646	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℂ)
317	316	mulid1d 10658	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (𝑀 · 1) = 𝑀)
318	311, 315, 317	3eqtrd 2860	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)1 = 𝑀)
319	201, 318	oveq12d 7174	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (Σ𝑘 ∈ (1...𝑀)((tan‘((𝑘 · π) / 𝑁))↑-2) + Σ𝑘 ∈ (1...𝑀)1) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
320	307, 309, 319	3eqtrd 2860	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
321		3cn 11719	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℂ
322	321	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → 3 ∈ ℂ)
323	139, 143, 322	adddid 10665	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (((2 · 𝑀) − 1) + 3)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + ((2 · 𝑀) · 3)))
324		df-3 11702	. . . . . . . . . . . . . . . . 17 ⊢ 3 = (2 + 1)
325	324	oveq1i 7166	. . . . . . . . . . . . . . . 16 ⊢ (3 − 1) = ((2 + 1) − 1)
326	47, 141	pncan3oi 10902	. . . . . . . . . . . . . . . 16 ⊢ ((2 + 1) − 1) = 2
327	325, 326, 161	3eqtri 2848	. . . . . . . . . . . . . . 15 ⊢ (3 − 1) = (1 + 1)
328	327	oveq2i 7167	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑀) + (3 − 1)) = ((2 · 𝑀) + (1 + 1))
329	139, 146, 322	subadd23d 11019	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = ((2 · 𝑀) + (3 − 1)))
330	139, 146, 146	addassd 10663	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) + 1) + 1) = ((2 · 𝑀) + (1 + 1)))
331	328, 329, 330	3eqtr4a 2882	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = (((2 · 𝑀) + 1) + 1))
332	3	oveq1i 7166	. . . . . . . . . . . . 13 ⊢ (𝑁 + 1) = (((2 · 𝑀) + 1) + 1)
333	331, 332	syl6eqr 2874	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) − 1) + 3) = (𝑁 + 1))
334	333	oveq2d 7172	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (((2 · 𝑀) − 1) + 3)) = ((2 · 𝑀) · (𝑁 + 1)))
335		2cnd 11716	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ → 2 ∈ ℂ)
336	335, 316, 322	mul32d 10850	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · 3) = ((2 · 3) · 𝑀))
337		3t2e6 11804	. . . . . . . . . . . . . . 15 ⊢ (3 · 2) = 6
338	321, 47	mulcomi 10649	. . . . . . . . . . . . . . 15 ⊢ (3 · 2) = (2 · 3)
339	337, 338	eqtr3i 2846	. . . . . . . . . . . . . 14 ⊢ 6 = (2 · 3)
340	339	oveq1i 7166	. . . . . . . . . . . . 13 ⊢ (6 · 𝑀) = ((2 · 3) · 𝑀)
341	336, 340	syl6eqr 2874	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · 3) = (6 · 𝑀))
342	341	oveq2d 7172	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · ((2 · 𝑀) − 1)) + ((2 · 𝑀) · 3)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)))
343	323, 334, 342	3eqtr3d 2864	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → ((2 · 𝑀) · (𝑁 + 1)) = (((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)))
344	343	oveq1d 7171	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)) / 6))
345		mulcl 10621	. . . . . . . . . . 11 ⊢ ((6 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (6 · 𝑀) ∈ ℂ)
346	173, 316, 345	sylancr 589	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → (6 · 𝑀) ∈ ℂ)
347	173	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 6 ∈ ℂ)
348	110	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 6 ≠ 0)
349	179, 346, 347, 348	divdird 11454	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((((2 · 𝑀) · ((2 · 𝑀) − 1)) + (6 · 𝑀)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + ((6 · 𝑀) / 6)))
350	316, 347, 348	divcan3d 11421	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → ((6 · 𝑀) / 6) = 𝑀)
351	350	oveq2d 7172	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ → ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + ((6 · 𝑀) / 6)) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
352	344, 349, 351	3eqtrd 2860	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / 6) = ((((2 · 𝑀) · ((2 · 𝑀) − 1)) / 6) + 𝑀))
353	320, 352	eqtr4d 2859	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2) = (((2 · 𝑀) · (𝑁 + 1)) / 6))
354	190, 353	oveq12d 7174	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π↑2) / (𝑁↑2)) · (((2 · 𝑀) · (𝑁 + 1)) / 6)))
355	139, 63, 266, 63, 64, 64	divmuldivd 11457	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁)))
356	193	oveq2d 7172	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁 · 𝑁)))
357	355, 356	eqtr4d 2859	. . . . . . 7 ⊢ (𝑀 ∈ ℕ → (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁)) = (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2)))
358	357	oveq2d 7172	. . . . . 6 ⊢ (𝑀 ∈ ℕ → (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))) = (((π↑2) / 6) · (((2 · 𝑀) · (𝑁 + 1)) / (𝑁↑2))))
359	279, 354, 358	3eqtr4d 2866	. . . . 5 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = (((π↑2) / 6) · (((2 · 𝑀) / 𝑁) · ((𝑁 + 1) / 𝑁))))
360	268, 272, 359	3eqtr4d 2866	. . . 4 ⊢ (𝑀 ∈ ℕ → ((((π↑2) / 6) · (1 − (1 / 𝑁))) · (1 + (1 / 𝑁))) = (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)))
361	225	recnd 10669	. . . . 5 ⊢ ((𝑀 ∈ ℕ ∧ 𝑘 ∈ (1...𝑀)) → ((sin‘((𝑘 · π) / 𝑁))↑-2) ∈ ℂ)
362	1, 35, 361	fsummulc2 15139	. . . 4 ⊢ (𝑀 ∈ ℕ → (((π / 𝑁)↑2) · Σ𝑘 ∈ (1...𝑀)((sin‘((𝑘 · π) / 𝑁))↑-2)) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
363	264, 360, 362	3eqtrd 2860	. . 3 ⊢ (𝑀 ∈ ℕ → (𝐾‘𝑀) = Σ𝑘 ∈ (1...𝑀)(((π / 𝑁)↑2) · ((sin‘((𝑘 · π) / 𝑁))↑-2)))
364	254, 218, 363	3brtr4d 5098	. 2 ⊢ (𝑀 ∈ ℕ → (𝐹‘𝑀) ≤ (𝐾‘𝑀))
365	219, 364	jca 514	1 ⊢ (𝑀 ∈ ℕ → ((𝐽‘𝑀) ≤ (𝐹‘𝑀) ∧ (𝐹‘𝑀) ≤ (𝐾‘𝑀)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ⊤wtru 1538 ∈ wcel 2114 ≠ wne 3016 Vcvv 3494 {csn 4567 class class class wbr 5066 ↦ cmpt 5146 × cxp 5553 ‘cfv 6355 (class class class)co 7156 ∘_f cof 7407 Fincfn 8509 ℂcc 10535 ℝcr 10536 0cc0 10537 1c1 10538 + caddc 10540 · cmul 10542 < clt 10675 ≤ cle 10676 − cmin 10870 -cneg 10871 / cdiv 11297 ℕcn 11638 2c2 11693 3c3 11694 6c6 11697 ℕ₀cn0 11898 ℤcz 11982 ℤ_≥cuz 12244 ℝ⁺crp 12390 (,)cioo 12739 ...cfz 12893 seqcseq 13370 ↑cexp 13430 Ccbc 13663 ♯chash 13691 Σcsu 15042 sincsin 15417 cosccos 15418 tanctan 15419 πcpi 15420

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 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-inf2 9104 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615 ax-addf 10616 ax-mulf 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-iin 4922 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-se 5515 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-isom 6364 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7409 df-om 7581 df-1st 7689 df-2nd 7690 df-supp 7831 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-2o 8103 df-oadd 8106 df-er 8289 df-map 8408 df-pm 8409 df-ixp 8462 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-fsupp 8834 df-fi 8875 df-sup 8906 df-inf 8907 df-oi 8974 df-dju 9330 df-card 9368 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-7 11706 df-8 11707 df-9 11708 df-n0 11899 df-xnn0 11969 df-z 11983 df-dec 12100 df-uz 12245 df-q 12350 df-rp 12391 df-xneg 12508 df-xadd 12509 df-xmul 12510 df-ioo 12743 df-ioc 12744 df-ico 12745 df-icc 12746 df-fz 12894 df-fzo 13035 df-fl 13163 df-mod 13239 df-seq 13371 df-exp 13431 df-fac 13635 df-bc 13664 df-hash 13692 df-shft 14426 df-cj 14458 df-re 14459 df-im 14460 df-sqrt 14594 df-abs 14595 df-limsup 14828 df-clim 14845 df-rlim 14846 df-sum 15043 df-ef 15421 df-sin 15423 df-cos 15424 df-tan 15425 df-pi 15426 df-struct 16485 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-ress 16491 df-plusg 16578 df-mulr 16579 df-starv 16580 df-sca 16581 df-vsca 16582 df-ip 16583 df-tset 16584 df-ple 16585 df-ds 16587 df-unif 16588 df-hom 16589 df-cco 16590 df-rest 16696 df-topn 16697 df-0g 16715 df-gsum 16716 df-topgen 16717 df-pt 16718 df-prds 16721 df-xrs 16775 df-qtop 16780 df-imas 16781 df-xps 16783 df-mre 16857 df-mrc 16858 df-acs 16860 df-mgm 17852 df-sgrp 17901 df-mnd 17912 df-submnd 17957 df-mulg 18225 df-cntz 18447 df-cmn 18908 df-psmet 20537 df-xmet 20538 df-met 20539 df-bl 20540 df-mopn 20541 df-fbas 20542 df-fg 20543 df-cnfld 20546 df-top 21502 df-topon 21519 df-topsp 21541 df-bases 21554 df-cld 21627 df-ntr 21628 df-cls 21629 df-nei 21706 df-lp 21744 df-perf 21745 df-cn 21835 df-cnp 21836 df-haus 21923 df-tx 22170 df-hmeo 22363 df-fil 22454 df-fm 22546 df-flim 22547 df-flf 22548 df-xms 22930 df-ms 22931 df-tms 22932 df-cncf 23486 df-0p 24271 df-limc 24464 df-dv 24465 df-ply 24778 df-idp 24779 df-coe 24780 df-dgr 24781 df-quot 24880

This theorem is referenced by: basellem9 25666

W3C validator